About Logic - Interview with Dana Scott

I'm sure this will be great Scott. Ask Bertrand Russell if you don't believe me.

See the centenary talk Scott gave on Strachey and also Scott, D. Some Reflections on Strachey and His Work. Higher-Order and Symbolic Computation 13, 103–114 (2000). https://doi.org/10.1023/A:1010018211714 and Toward a Mathematical Semantics for Computer Languages (1971) by Scott and Strachey.

2:03 From Scott's Strachey centenary talk:

Let us now return to λ-calculus and Strachey’s use of it. Christopher told me once that Roger Penrose (now Sir Roger!) suggested to him that he ought to look into using the λ-calculus for the kind of function definitions he wanted to do. At this moment I cannot track down or verify the story. (Perhaps people in Oxford might ask Penrose personally about this?)

See Curt Jaimungal Talking With Roger Penrose and the reference Penrose made to S. W. P. Steen's graduate course in Mathematical Logic. In 1973 Steen published a book Mathematical Logic with special reference to the natural numbers. See Emily Riehl on Univalent Foundations.

At the time of my discovery of the λ-calculus model in 1969, John Reynolds (1935-2013) was visiting England and attended my first lectures about the approach. He became an enthusiastic advocate, as he had been working himself on programming-language design. Over the years he subsequently made many major contributions to design and theory, as recounted in the Brookes-O’Hearn-Reddy Reynolds memorial paper in 2014. 

See The Essence of Reynolds by by Stephen Brookes, Peter W. O’Hearn, and Uday S. Reddy.

See the second edition of the book Boolean-valued Models and Independence Proofs in Set Theory by John L. Bell.

28:22 On predicative dependent type theory, see Martín Escardó's publications and preprints and some papers by Tom De Jong listed at nlab.

David Turner was another of Dana Scott's PhD students. See David Turner - Sixty Years of Functional Programming History and David Turner Obituary by Sarah Nicholas.

And whilst browsing around, I ran across this paper by Esther Dennis-Jones and David E. Rydeheard (1993): Categorical ML - Category-Theoretic Modular Programming and this 2005 paper Contextual equivalence for higher-order pi-calculus revisited by Alan Jeffrey and Julian Rathke. Also Principal typing schemes in a polyadic π-calculus (1993) by Vasco T. Vasconcelos & Kohei Honda and this 1998 paper by Gérard Boudol: 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.

Subscribe to About Logic.

Thorsten has a set of five really good talks about type theory on his YouTube:

More material at https://people.cs.nott.ac.uk/psztxa/mgs.2021/.

Subscribe to Thorsten Altenkirch.

I am wondering now whether that 2-torial David Jaz Myers did was all about trying to understand what's going in Girard, Lafont and Taylor's Proofs and Types. It seems to me that the deduction theorem (§5 on page 62) in Church's 1940 A Formalisation of the Simple Theory of Types is an induction on the Fundamental Theorem of Topos Theory (Logical Interpretation). One could start with this as an axiom, and then prove initial segments of the fundamental theorem constructively, introducing whatever syntax one needs within each iteration of the process. Then try to diagonalise that!