Sunday 2nd August 2009

(at LFMTP)
Invited talk:
Gilles Dowek, Ecole Polytechnique:
How Can We Prove That a Proof Method is not an Instance of Another?

Monday 3rd August 2009

10:00-10:30 Coffee
10:30-11:30 Tutorial:
Wilmer Ricciotti, University of Bologna:
Proof-search in Matita

This tutorial presents some of the distinctive features of user interaction with the Matita interactive theorem prover. We place particular emphasis on automation and related tools, including an interactive graphical interface for inspecting the proof searching strategy on a step-by-step basis. Design and implementation issues will be discussed according to the audience's interests.

11:30-11:45 Mini-break
11:45-12:30 Adam Petcher and Aaron Stump,
Deciding Joinability Modulo Ground Equations in Operational Type Theory

Operational Type Theory (OpTT) is a theory of joinability of untyped functional terms including general recursion, pattern-matching and inductive datatypes, and higher-order functions. An algorithm is presented that can be used to automatically generate proofs of equality in OpTT. The algorithm will equate two supplied terms if and only if there exists an OpTT proof that can equate the two terms using only the proof rules related to evaluation under the operational semantics, symmetry, transitivity, and congruence with respect a set of supplied ground equations. The algorithm is proved sound, and under some natural assumptions about the termination behavior of the functions, also complete.

12:30-14:00 Lunch break
14:00-14:45 Noam Zeilberger,
Defunctionalizing focusing proofs

In previous work, the author gave a higher-order analysis of *focusing proofs* (in the sense of Andreoli's search strategy), with a role for infinitary rules very similar in structure to Buchholz's $\Omega$-rule. Among other benefits, this ``pattern-based'' description of focusing simplifies the cut-elimination procedure, allowing cuts to be eliminated in a connective-generic way. However, interpreted literally, it is problematic as a representation technique for proofs, because of the difficulty of inspecting and/or exhaustively searching over these infinite objects. In the spirit of infinitary proof theory, this paper explores a view of pattern-based focusing proofs as "facons de parler", describing how to compile them down to first-order derivations through defunctionalization, Reynolds' program transformation. Our main result is a representation of pattern-based focusing in the Twelf logical framework, whose core type theory is too weak to directly encode infinitary rules---although this weakness directly enables so-called ``higher-order abstract syntax'' encodings. By applying the systematic defunctionalization transform, not only do we retain the benefits of the higher-order focusing analysis, but we can also take advantage of HOAS within Twelf, ultimately arriving at a proof representation with surprisingly little bureaucracy.

14:45-15:30 Denis Cousineau,
Complete reducibility candidates

Deduction modulo is an extension of first-order predicate logic where axioms are replaced by a congruence relation on propositions and where many theories, such as arithmetic, simple type theory and some variants of set theory, can be expressed. An important question in deduction modulo is to find a condition of the theories that have the strong normalization property. Dowek and Werner have given a semantic sufficient condition for a theory to have the strong normalization property: they have proved a "soundness" theorem of the form: if a theory has a model (of a particular form) then it has the strong normalization property. In this paper, we refine their notion of model in a way allowing not only to prove soundness, but also completeness: if a theory has the strong normalization property, then it has a model of this form. The key idea of our model construction is a refinement of Girard's notion of reducibility candidates. By providing a sound and complete semantics for theories having the strong normalization property, this paper contributes to explore the idea that strong normalization is not only a proof-theoretic notion, but also a model-theoretic one.

12:30-14:00 Coffee
16:00-16:45 Carsten Schuermann
Linear Contextual Modal Type Theory

When one develops, implements, and studies type theories based on linear logic, for example, in the context of theorem proving, logic programming, and formal reasoning, one is immediately confronted with questions about their equational theory and how to deal with logic variables. In this paper, we propose linear contextual modal type the- ory that gives a mathematical account of the nature of logic variables. Our type theory is conservative over intuitionistic contextual modal type theory proposed by Nanevski, Pfenning, and Pientka. As a technical con- tribution we provide a proof of soundness, and, as a justification for its usefulness, we sketch how contextual modal type theory is used to state Cervesato's and Pfenning's linear pre-unification algorithm [CP97].

16:45-17:30 Discussion (theme and workshop)