[Agda] Operational and Denotational, Typed and Untyped Lambda Calculus

[Martin Escardo]

> No favourites from anyone else? That doesn't seem much like this list!

(1) Of course, you can consider the type-theoretic incarnation of the 
"set-theoretic model" of Goedel's system T (simply typed lambda calculus 
with a base type for natural numbers, as you know).

http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue.pdf

This also considers a "dialogue" "forcing" model of system T, and then a 
logical relation between this and the set-theoretical model to prove (in 
Agda) that all system T definable functions (N->N)->N of the 
set-theoretical model are continuous.

The paper quoted above works with the SKI-combinatory version of system 
T, for simplicity of presentation. However, further accompanying Agda 
files consider the lambda-calculus version, and more: 
http://www.cs.bham.ac.uk/~mhe/dialogue/

(2) Again with system T, we can consider models in which all functions 
(of all types) are continuous (rather than just the definable ones of 
type (N->N)->N.)

This is done by my former PhD student Chuangjie Xu. https://cj-xu.github.io/

(3) Following from (2), this is actually a manifestation of the 
Kleene-Kreisel continuous functionals from the 1950's, used at that time 
(and to this day) to model computation with higher types. This is in the 
above Agda code (2) and also in the paper

http://www.cs.bham.ac.uk/~mhe/papers/kleene-kreisel.pdf

(4) This hasn't been implemented in Agda yet, but it should:
http://www.cs.bham.ac.uk/~mhe/papers/partial-elements-and-recursion.pdf

And actually it needs a univalent extension of type theory, such as 
cubical Agda: https://agda.readthedocs.io/en/latest/language/cubical.html

This last (4) is more in the vein of Dana Scott's ideas, but 
constructively performed (following the lead of many people, including 
Rosolini, Hyland, among others).

Best wishes,
Martin