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

[Philip Wadler]

Thank you for the further replies. I'm looking into them! Cheers, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On 30 March 2018 at 16:35, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:

> 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
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180403/78b5936a/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180403/78b5936a/attachment.ksh>