Löb's Theorem: A functional pearl of dependently typed quining: List of References

We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids referring to preterms or a typability relation but defines directly well typed objects by an inductive definition. We use the elimination principle to define the set-theoretic and logical predicate interpretation. The work has been formalized using the Agda system extended with QITs using postulates.

Keywords: Higher Inductive Types, Homotopy Type Theory, Logical Relations, Metaprogramming, Agda

An Isabelle/HOL formalisation of Gödel's two incompleteness theorems is presented. The work follows Świerczkowski's detailed proof of the theorems using hereditarily finite (HF) set theory (Dissertationes Mathematicae 422, 1--58, 2003). Avoiding the usual arithmetical encodings of syntax eliminates the necessity to formalise elementary number theory within an embedded logical calculus. The Isabelle formalisation uses two separate treatments of variable binding: the nominal package (Logical Methods in Computer Science 8(2:14), 1--35, 2012) is shown to scale to a development of this complexity, while de Bruijn indices (Indagationes Mathematicae 34, 381--392, 1972) turn out to be ideal for coding syntax. Critical details of the Isabelle proof are described, in particular gaps and errors found in the literature.

We consider the one-shot Prisoner's Dilemma between algorithms with read-access to one anothers' source codes, and we use the modal logic of provability to build agents that can achieve mutual cooperation in a manner that is robust, in that cooperation does not require exact equality of the agents' source code, and unexploitable, meaning that such an agent never cooperates when its opponent defects. We construct a general framework for such "modal agents", and study their properties.

We present constructive provability logic, an intuitionstic modal logic that validates the Löb rule of Gödel and Löb's provability logic by permitting logical reflection over provability. Two distinct variants of this logic, CPL and CPL*, are presented in natural deduction and sequent calculus forms which are then shown to be equivalent. In addition, we discuss the use of constructive provability logic to justify stratified negation in logic programming within an intuitionstic and structural proof theory.

Tagless interpreters for well-typed terms in some object language are a standard example of the power and benefit of precise indexing in types, whether with dependent types, or generalized algebraic datatypes. The key is to reflect object language types as indices (however they may be constituted) for the term datatype in the host language, so that host type coincidence ensures object type coincidence. Whilst this technique is widespread for simply typed object languages, dependent types have proved a tougher nut with nontrivial computation in type equality. In their type-safe representations, Danielsson [2006] and Chapman [2009] succeed in capturing the equality rules, but at the cost of representing equality derivations explicitly within terms. This article delivers a type-safe representation for a dependently typed object language, dubbed KIPLING, whose computational type equality just appropriates that of its host, Agda. The Kipling interpreter example is not merely de rigeur--- it is key to the construction. At the heart of the technique is that key component of generic programming, the universe.

In this paper I present a partial formalisation of a normaliser for type theory in Agda [Ulf Norell. Agda 2, 2007. http://www.cs.chalmers.se/ ulfn/]; extending previous work on big-step normalisation [Thorsten Altenkirch and James Chapman. Big-Step Normalisation. Journal of Functional Programming, 2008. Special Issue on Mathematically Structured Functional Programming. To appear, Thorsten Altenkirch and James Chapman. Tait in one big step. In Workshop on Mathematically Structured Functional Programming, {MSFP} 2006, Kuressaare, Estonia, July 2, 2006, electronic Workshop in Computing (eWiC), Kuressaare, Estonia, 2006. The British Computer Society (BCS)]. The normaliser in written as an environment machine. Only the computational behaviour of the normaliser is presented omitting details of termination.

Keywords: big-step normalisation

It is demonstrated how a dependently typed lambda calculus (a logical framework) can be formalised inside a language with inductive- recursive families. The formalisation does not use raw terms; the well- typed terms are defined directly. It is hence impossible to create ill-typed terms.

As an example of programming with strong invariants, and to show that the formalisation is usable, normalisation is proved. Moreover, this proof seems to be the first formal account of normalisation by evaluation for a dependently typed language.

This paper has something new and positive to say about propositional equality in programming and proof systems based on the Curry-Howard correspondence between propositions and types. We have found a way to present a propositional equality type

• which is substitutive, allowing us to reason by replacing equal for equal in propositions;
• which reflects the observable behaviour of values rather than their construction: in particular, we
• have extensionality-- functions are equal if they take equal inputs to equal outputs;
• which retains strong normalisation, decidable typechecking and canonicity--the property that closed normal forms inhabiting datatypes have canonical constructors;
• which allows inductive data structures to be expressed in terms of a standard characterisation of well-founded trees;
• which is presented syntactically--you can implement it directly, and we are doing so this approach stands at the core of Epigram 2;
• which you can play with now: we have simulated our system by a shallow embedding in Agda 2, shipping as part of the standard examples package for that system [21].

Until now, it has always been necessary to sacrifice some of these aspects. The closest attempt in the literature is Altenkirch's construction of a setoid-model for a system with canonicity and extensionality on top of an intensional type theory with proof-irrelevant propositions [4]. Our new proposal simplifies Altenkirch's construction by adopting McBride's heterogeneous approach to equality [19].

Keywords: equality, type theory

Observational Type Theory (OTT) combines benefi- cial aspects of Intensional and Extensional Type Theory (ITT/ETT). It separates definitional equality, decidable as in ITT, and a substitutive propositional equality, capturing extensional equality of functions, as in ETT. Moreover, canonicity holds: any closed term is definitionally reducible to a canonical value.

Building on previous work by each author, this article reports substantial progress in the form of a simplified theory with a straightforward syntactic presentation, which we have implemented.

As well as simplifying reasoning about functions, OTT offers potential foundational benefits, e.g. it gives rise to a closed type theory encoding inductive datatypes.

Keywords: binding times, run-time code generation, staged computation

The five lectures at Marktoberdorf on which these notes are based were about the architecture of problem solving environments which use theorem provers. Experience with these systems over the past two decades has shown that the prover must be extensible, yet it must be kept. We examine a way to safely add new decision procedures to the Nuprl prover. It relies on a reflection mechanism and is applicable to any tactic-oriented prover with sufficient reflection. The lectures explain reflection in the setting of constructive type theory, the core logic of Nuprl.

We consider the question of whether a useful notion of metacircularity exists for the polymorphic λ-calculus. Even though complete metacircularity seems to be impossible, we obtain a close approximation to a metacircular interpreter. We begin by presenting an encoding for the Girard-Reynolds second-order polymorphic λ-calculus in the third-order polymorphic λ-calculus. The encoding makes use of representations in which abstractions are represented by abstractions, thus eliminating the need for the explicit representation of environments. We then extend this construction to encompass all of the ω-order polymorphic λ-calculus (Fω). The representation has the property that evaluation is definable, and furthermore that only well-typed terms can be represented and thus type inference does not have to be explicitly defined. Unfortunately, this metacircularity result seems to fall short of providing a useful framework for typed metaprogramming. We speculate on the reasons for this failure and the prospects for overcoming it in the future. In addition, we briefly describe our efforts in designing a practical programming language based on Fω.

The notion of iteratively defined functions from and to heterogeneous term algebras is introduced as the solution of a finite set of equations of a special shape. Such a notion has remarkable consequences: (1) Choosing the second-order typed lambda- calculus (Lambsa for short) as a programming language enables one to represent algebra elements and iterative functions by automatic uniform synthesis paradigms, using neither conditional nor recursive constructs. (2) A completeness theorem for Lambda-terms with type of degree at most two and a companion corollary for Lambda-programs have been proved. (3) A new congruence relation for the last-mentioned Lambda-terms which is stronger than Lambda-convertibility is introduced and proved to have the meaning of a Lambda-program equivalence. Moreover, an extension of the paradigms to the synthesis of functions of higher complexity is considered and exemplified. All the concepts are explained and motivated by examples over integers, list- and tree-structures.