<div dir="ltr">Thank you for the further replies. I'm looking into them! Cheers, -- P</div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 30 March 2018 at 16:35, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
No favourites from anyone else? That doesn't seem much like this list!<br>
</blockquote>
<br></span>
(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).<br>
<br>
<a href="http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue.pdf" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe/<wbr>dialogue/dialogue.pdf</a><br>
<br>
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.<br>
<br>
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: <a href="http://www.cs.bham.ac.uk/~mhe/dialogue/" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe/<wbr>dialogue/</a><br>
<br>
(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.)<br>
<br>
This is done by my former PhD student Chuangjie Xu. <a href="https://cj-xu.github.io/" rel="noreferrer" target="_blank">https://cj-xu.github.io/</a><br>
<br>
(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<br>
<br>
<a href="http://www.cs.bham.ac.uk/~mhe/papers/kleene-kreisel.pdf" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe/<wbr>papers/kleene-kreisel.pdf</a><br>
<br>
(4) This hasn't been implemented in Agda yet, but it should:<br>
<a href="http://www.cs.bham.ac.uk/~mhe/papers/partial-elements-and-recursion.pdf" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe/<wbr>papers/partial-elements-and-re<wbr>cursion.pdf</a><br>
<br>
And actually it needs a univalent extension of type theory, such as cubical Agda: <a href="https://agda.readthedocs.io/en/latest/language/cubical.html" rel="noreferrer" target="_blank">https://agda.readthedocs.io/en<wbr>/latest/language/cubical.html</a><br>
<br>
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).<br>
<br>
Best wishes,<br>
Martin<br>
<br>
<br>
</blockquote></div><br></div>