System Fω and Total Functional Programming

See Breaking through the normalization barrier: a self-interpreter for f-omega (POPL 2016) by Matt Brown and Jens Palsberg.

Here's his earlier video about System-F. 

Subscribe to Computable Secrets.

Jeremy Gibbons on his book Functional Programming Patterns

 

See his piece How Design Co-programs. 

Why is so hard to get anyone to talk about the dual notion which is data representation by processes? If data determines algorithms, then algorithms can equally well determine data. And if those algorithms are distributed computations then it makes the data they represent very hard to alter. If you ask a computer scientists they might just say "Well, that's because they're not isomorphic." But that doesn't matter: it just means that codata can represent so-called uncomputable functions, which can actually be used in practical applications such as forward key-generation.

Some physicists also don't seem to want to think about what data actually is. See Jetbundle - Groups, Monoids, Homomorphisms and Vibes, ... and Why is Physics So Difficult?

Subscribe to Topos Institute.

See Boudol's 1998 paper The π-Calculus in Direct Style:

We introduce a calculus which is a direct extension of both the λ and the π calculi. We give a simple type system for it, that encompasses both Curry‘s type inference for the λ-calculus, and Milner‘s sorting for the π-calculus as particular cases of typing. We observe that the various continuation passing style transformations for λ-terms, written in our calculus, actually correspond to encodings already given by Milner and others for evaluation strategies of λ-terms into the π-calculus. Furthermore, the associated sortings correspond to well-known double negation translations on types. Finally we provide an adequate CPS transform from our calculus to the π-calculus. This shows that the latter may be regarded as an “assembly language”, while our calculus seems to provide a better programming notation for higher-order concurrency. We conclude by discussing some alternative design decisions. 

See also Contextual equivalence for higher-order pi-calculus revisited by Alan Jeffrey and Julian Rathke.

The higher-order pi-calculus is an extension of the pi-calculus to allow communication of abstractions of processes rather than names alone. It has been studied intensively by Sangiorgi in his thesis where a characterisation of a contextual equivalence for higher-order pi-calculus is provided using labelled transition systems and normal bisimulations. Unfortunately the proof technique used there requires a restriction of the language to only allow finite types. We revisit this calculus and offer an alternative presentation of the labelled transition system and a novel proof technique which allows us to provide a fully abstract characterisation of contextual equivalence using labelled transitions and bisimulations for higher-order pi-calculus with recursive types also.

Representations such as this one would also allow zero-knowledge verification of personal data such as age/physical location/financial solvency etc. Is that the real problem?  It's just too damned difficult to stay alive long enough to get the message across? See Alan Jeffrey, 1967–2024.

Subscribe to Olive Badger.