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

[1] Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In POPL '16 The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 2016. [ bib | http ]
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
[2] Matt Brown and Jens Palsberg. Breaking through the normalization barrier: A self-interpreter for f-omega. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 5--17. ACM, 2016. [ bib | DOI | .pdf ]
[3] Lawrence C Paulson. A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle. Journal of Automated Reasoning, 55(1):1--37, 2015. [ bib | .pdf ]
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.
[4] Brienne Yudkowsky. Lob's theorem cured my social anxiety, February 2014. [ bib | .html ]
[5] Herman Geuvers. The Church-Scott representation of inductive and coinductive data, 2014. [ bib | .pdf ]
[6] Mihaly Barasz, Paul Christiano, Benja Fallenstein, Marcello Herreshoff, Patrick LaVictoire, and Eliezer Yudkowsky. Robust cooperation in the prisoner's dilemma: Program equilibrium via provability logic. ArXiv e-prints, January 2014. [ bib | arXiv | .pdf ]
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.
[7] Robert J. Simmons and Bernardo Toninho. Constructive provability logic. CoRR, abs/1205.6402, May 2012. [ bib | arXiv | http ]
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.
[8] Oleg Kiselyov. Beyond church encoding: Boehm-berarducci isomorphism of algebraic data types and polymorphic lambda-terms, April 2012. [ bib | .html ]
[9] Conor McBride. Outrageous but meaningful coincidences: Dependent type-safe syntax and evaluation. In Proceedings of the 6th ACM SIGPLAN workshop on Generic programming, pages 1--12. ACM, 2010. [ bib | .pdf ]
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.
[10] James Chapman. Type theory should eat itself. Electronic Notes in Theoretical Computer Science, 228:21--36, 2009. Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008). [ bib | DOI | http ]
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
[11] Eliezer Yudkowsky. (the cartoon guide to) Löb's theorem, 2008. [ bib | http ]
[12] Nils Anders Danielsson. A formalisation of a dependently typed language as an inductive-recursive family. In Thorsten Altenkirch and Conor McBride, editors, Types for Proofs and Programs, volume 4502 of Lecture Notes in Computer Science, chapter A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family, pages 93--109. Springer Berlin Heidelberg, Berlin, Heidelberg, 2007. [ bib | DOI | http ]
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.

[13] Andrew W Appel, Paul-André Mellies, Christopher D Richards, and Jérôme Vouillon. A very modal model of a modern, major, general type system. ACM SIGPLAN Notices, 42(1):109--122, 2007. [ bib | .pdf ]
[14] Thorsten Altenkirch, Conor McBride, and Wouter Swierstra. Observational equality, now! In Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification, PLPV '07, pages 57--68, New York, NY, USA, 2007. ACM. [ bib | DOI | .pdf ]
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
[15] Dan Piponi. From löb's theorem to spreadsheet evaluation, November 2006. [ bib | .html ]
[16] Thorsten Altenkirch and Conor McBride. Towards observational type theory. Manuscript, available online, 2006. [ bib | .pdf ]
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.

[17] Russell O'Connor. Essential incompleteness of arithmetic verified by coq. CoRR, abs/cs/0505034, 2005. [ bib | http ]
[18] Rowan Davies and Frank Pfenning. A modal analysis of staged computation. J. ACM, 48(3):555--604, May 2001. [ bib | DOI | http ]
Keywords: binding times, run-time code generation, staged computation
[19] Torben Æ. Mogensen. An investigation of compact and efficient number representations in the pure lambda calculus. In Perspectives of System Informatics, 4th International Andrei Ershov Memorial Conference, PSI 2001, Akademgorodok, Novosibirsk, Russia, July 2-6, 2001, Revised Papers, pages 205--213, 2001. [ bib | DOI | http ]
[20] Geoffrey K. Pullum. Scooping the loop snooper, October 2000. [ bib | .html ]
[21] Natarajan Shankar. Metamathematics, Machines and Gödel's Proof. Cambridge University Press, 1997. [ bib ]
[22] Robert L Constable. Using reflection to explain and enhance type theory. In Proof and Computation, pages 109--144. Springer, 1995. [ bib | http ]
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.
[23] Frank Pfenning and Peter Lee. Metacircularity in the polymorphic λ-calculus. Theoretical Computer Science, 89(1):137--159, 1991. [ bib | DOI | http ]
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ω.
[24] Natarajan Shankar. Proof-checking Metamathematics (Theorem-proving). PhD thesis, The University of Texas at Austin, 1986. AAI8717580. [ bib ]
[25] Alessandro Berarducci and Corrado Böhm. Automatic synthesis of typed λ-programs on term algebras. Theoretical Computer Science, 39(820076097):135--154, 1985. [ bib | DOI | http ]
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.
[26] Douglas R. Hofstadter. Gödel, Escher, Bach: An Eternal Golden Braid. Vintage, 1979. [ bib ]
[27] Dana Scott. A system of functional abstraction. Unpublished manuscript, 1963. [ bib ]
[28] Stephen Cole Kleene. Introduction to Metamathematics. Wolters-Noordhoff, 1952. [ bib ]
[29] Alonzo Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5(2):56--68, 1940. [ bib | http ]
[30] Alfred Tarski. Der Wahrheitsbegriff in den formalisierten Sprachen. Studia Philosophica, 1:261--405, 1936. [ bib | .pdf ]
[31] Kurt Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für mathematik und physik, 38(1):173--198, 1931. [ bib | .pdf ]

This file was generated by bibtex2html 1.99.