10:0010:30 
Coffee 
10:3011:30 
Tutorial:
Wilmer Ricciotti, University of Bologna:
Proofsearch in Matita
Abstract:
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 stepbystep basis. Design and implementation issues will be discussed according to the audience's interests.

11:3011:45 
Minibreak 
11:4512:30 
Adam Petcher and Aaron Stump,
Deciding Joinability Modulo Ground Equations in Operational Type Theory
Abstract:
Operational Type Theory (OpTT) is a theory of joinability of untyped
functional terms including general recursion, patternmatching and
inductive datatypes, and higherorder 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:3014:00 
Lunch break 
14:0014:45 
Noam Zeilberger,
Defunctionalizing focusing proofs
Abstract:
In previous work, the author gave a higherorder 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 ``patternbased'' description of focusing simplifies the cutelimination procedure,
allowing cuts to be eliminated in a connectivegeneric 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 patternbased focusing proofs as "facons de parler", describing how to compile them down to firstorder derivations through defunctionalization, Reynolds' program transformation. Our main result is a representation of patternbased focusing
in the Twelf logical framework, whose core type theory is too weak to
directly encode infinitary rulesalthough this weakness directly enables socalled ``higherorder abstract syntax'' encodings. By applying the systematic
defunctionalization transform, not only do we retain the benefits of the higherorder focusing analysis, but we can also take advantage of HOAS within Twelf, ultimately arriving at a proof representation with surprisingly little
bureaucracy.

14:4515:30 
Denis Cousineau,
Complete reducibility candidates
Abstract:
Deduction modulo is an extension of firstorder 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 prooftheoretic notion, but also a modeltheoretic one.

12:3014:00 
Coffee 
16:0016:45 
Carsten Schuermann
Linear Contextual Modal Type Theory
Abstract:
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 preunification algorithm [CP97].

16:4517:30 
Discussion (theme and workshop) 