Håkon Gylterud: Quote operations on λ-calculus and type theory
Time: Wed 2019-04-10 10.00 - 11.45
Lecturer: Håkon Gylterud, University of Bergen
Location: Room 16, building 5, Kräftriket, Department of Mathematics, Stockholm University
Abstract: Going back to Gödel, we know that many formal languages have the ability to represent their own syntax. The operation which turns an expression into its internal representation is called quoting. For programming languages, one can also ask if they can internally represent their own evaluation function. Work by Brown and Palsberg shows that this is even possible to some extent for strongly normalizing languages.
Quoting is usually a meta-theoretical operation. However, some programming languages, such as LISP or Scheme, have this as an internal operation in the language. In this talk I will present extensions of λ-calculus and type theory with internal quoting operations. They differ from the LISP or Scheme equivalents by being confluent while allowing reductions under the quote.
The motivation for this work is to study how Church’s thesis, which states that every function is computable, can be seen as a quoting operation with extra properties. We will discuss how this statement can be internalised and demonstrated in an extension of intensional Martin-Löf type theory.
: Breaking through the Normalization Barrier: A Self-interpreter for F-omega, M. Brown and J. Palsberg, Proceedings of POPL'16.