| 10:00-10:30 |
Coffee |
| 10:30-11:30 |
Tutorial:
Wilmer Ricciotti, University of Bologna:
Proof-search 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 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
Abstract:
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
Abstract:
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
Abstract:
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
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 pre-unification algorithm [CP97].
|
| 16:45-17:30 |
Discussion (theme and workshop) |