Workshop Program

We consider the normalization proof for a simply-typed lambda calculus with Mendler-style recursion using logical relations. This language is powerful enough to encode total recursive functions using recursive types. A key feature of our proof is the semantic interpretation of recursive types, which requires higher-kinded polymorphism in the reasoning language. We have implemented the proof in Coq due to this requirement. However, we believe this proof can serve as a challenge problem for other proof environments, especially those supporting binders, since our mechanization in Coq requires proofs of several substitution properties.

Proof constructivization is the problem of automatically extracting constructive proofs out of classical proofs. It is required to integrate classical theorem provers in intuitionistic proof assistants. We use the ability of rewrite systems to represent partial functions to implement heuristics for proof constructivization in Dedukti, a logical framework based on rewriting in which proofs are first-class objects which can be the subject of computation. We benchmark these heuristics on the proofs outputted by the automated theorem prover Zenon on the TPTP library of problems.

Hybrid is a logical framework that supports the use of higher-order abstract syntax (HOAS) in representing formal systems or “object logics” (OLs). It is implemented in Coq and follows a two-level approach, where a specification logic (SL) is implemented as an inductive type and used to concisely and elegantly encode the inference rules of the formal systems of interest. In this paper, we develop a new higher-order specification logic for Hybrid. By increasing the expressive power of the SL beyond what was considered previously, we increase the flexibility of encoding OLs and thus extend the class of formal systems for which we can reason about efficiently. We focus on formalizing the meta-theory of the SL. We develop an abstract way in which to present an important class of meta-theorems. This class includes properties such as weakening, contraction, exchange, and the admissibility of the cut rule. The cut admissibility theorem establishes consistency and also provides justification for substituting a formula for an assumption in a context of assumptions. It can greatly simplify reasoning about OLs in systems that provide HOAS. We present the abstraction and show how it is used to prove all of these theorems.

We present a proof-of-concept prototype of a (constructive variant of an) HOL interactive theorem prover written in a Higher Order Logic Programming (HOLP) language, namely an extension of LambdaProlog. The prototype is meant to support the claim, that we reinforce, that HOLP is the class of languages that provides the right abstraction level and programming primitives to obtain concise implementations of theorem provers. We identify and advocate for a programming technique, that we call semi-shallow embedding, while at the same time identifying the reasons why pure LambdaProlog is not sufficient to support that technique, and it needs to be extended.

Bringing the joy and excitement of interactive theorem provers to high school students is a challenge, because having to learn the rules of the syntax, and manually checking hand-written proofs is just not fun. Thus I created the Incredible Proof Machine, which allows students to conduct proofs by dragging blocks and wiring up them up to “proof graphs”, all using just the mouse. The result is a surprisingly addictive game-like experience that lures students (and non-students) to prove statements of propositional and predicate logic; or any other natural-deduction based calculus their instructor wants to teach. In this talk, I will explain the motivation behind the Proof Machine and its design decisions, demonstrate the user interface and its various features, show how to define your own tasks and even logics and outline the correspondence between these proof graphs and conventional natural deduction derivation trees.