|10:30-12:30||Contributed Papers||Gilles Dowek|
Mechanizing Proofs about Mendler-style Recursion
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.
A Rewrite System for Proof Constructivization
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.
The Logic of Hereditary Harrop Formulas as a Specification Logic for Hybrid
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.
Implementing HOL in an Higher Order Logic Programming Language
12:30-14:00 Lunch break
|14:00-15:00||Invited Talk||(chair: Gilles Dowek)|
The Incredible Proof Machine
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.