Workshop Program
10:3012:30  Contributed Papers  Gilles Dowek 
10:30 
Mechanizing Proofs about Mendlerstyle Recursion
We consider the normalization proof for a simplytyped lambda
calculus with Mendlerstyle 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 higherkinded 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.

11:00 
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
firstclass 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.

11:30 
The Logic of Hereditary Harrop Formulas as a Specification Logic for Hybrid
Hybrid is a logical framework that supports the use of higherorder
abstract syntax (HOAS) in representing formal systems or “object
logics” (OLs). It is implemented in Coq and follows a twolevel
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 higherorder 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 metatheory of the
SL. We develop an abstract way in which to present an important
class of metatheorems. 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.

12:00 
Implementing HOL in an Higher Order Logic Programming Language

12:3014:00
Lunch break
14:0015:00  Invited Talk  (chair: Gilles Dowek) 
14:00 
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 handwritten 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 gamelike experience that lures students (and nonstudents)
to prove statements of propositional and predicate logic; or any other
naturaldeduction 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.
