Thursday 15th July 2010

10:00-10:30 Coffee
10:30-11:10 Harley D. Eades III, Aaron Stump
Hereditary Substitution for Stratified System F

This paper proves normalization for Stratified System F, a type theory of predicative polymorphism studied by D. Leivant, by an extension of the method of hereditary substitution due to F. Pfenning. The advantage of normalization by hereditary substitution over normalization by reducibility is that the proof method is substantially less intricate, which promises to make it easier to apply to new theories.

11:10-11:50 Alexandre Viel and Dale Miller
Proof search when equality is a logical connective: Extended Abstract

We explore how one might do proof search in a simple, first-order classical logic where equality is treated as a logical connective. That is, equality over first-order terms has a left and right introduction rule. The formulation of the left-introduction rule involves unification of eigenvariables. The usual strategy for implementing proof search also involves unification, but this time for existential variables (not eigenvariables). In this paper, we show such unification over these two species of variables can at times be solved by a reduction to a particular subset of second-order unification problems. We also show that a given second-order unification problem in that subset can be encoded as a first-order formula in such a way that finding a proof of that formula solves the unification problem. We additionally argue that solving such second-order unifications problems is undecidable.

11:50-12:30 Arnaud Spiwack
An abstract type for constructing tactics in Coq

The Coq proof assistant is a large development, a lot of which happens to be more or less dependent on the type of tactics. To be able to perform tweaks in this type more easily in the future, we propose an API for building tactics which does not need to expose the type of tactics and yet has a fairly small amount of primitives. This API accompanies an entirely new implementation of the core tactic engine of Coq which aims at handling more gracefully existential variables (aka. metavariables) in proofs - like in more recent proof assistants like Matita and Agda2. We shall, then, leverage this newly acquired independence of the concrete type of tactics from the API to add backtracking abilities.

12:30-14:00 Lunch break
14:00-14:40 Zachary Snow, David Baelde and Gopalan Nadathur
Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search

Dependently typed lambda-calculi such as the Logical Framework (LF) are capable of representing relationships between terms through types. By exploiting the formulas-as-types notion, such calculi can also encode the correspondence between formulas and their proofs in typing judgments. As such, these calculi provide a natural yet powerful means for specifying varied formal systems. Such specifications can be transformed into a more direct form that uses predicate formulas over simply typed lambda-terms and that thereby provides the basis for their animation using conventional logic programming techniques. However, a naive use of this idea is fraught with inefficiencies arising from the fact that dependently typed expressions typically contain much redundant typing information. We investigate syntactic criteria for recognizing and, hence, eliminating such redundancies. In particular, we identify a property of bound variables in LF types called rigidity and formally show that checking that instantiations of such variables adhere to typing restrictions is unnecessary for the purpose of ensuring that the overall expression is well-formed. We show how to exploit this property in a translation based approach to executing specifications in the Twelf language. Recognizing redundancy is also relevant to devising compact representations of dependently typed expressions. We highlight this aspect of our work and discuss its connection with other approaches proposed in this context.

14:40-15:00 Discussion (theme and workshop)
15:00-15:30 Coffee
15:30-16:30 David Baelde
An overview of focusing for least and greatest fixed points in intuitionistic logic

Least and greatest fixed points, corresponding to inductive and coinductive definitions, are known to be difficult concepts in proof-theory. Recent advances, however, have brought some structure to these problems: The notion of focusing has been extended to support least and greatest fixed points, opening promising avenues. This has been done first in linear logic (\muMALL and \muLL) but also applies to the intuitionistic setting (\muLJ). In this paper, we fully review the current state of focusing in \muLJ, its successes in automated reasoning as well as its puzzles, on which we provide new insights by studying how our focusing mechanisms apply to related systems.

16:30-17:30 Invited talk:
Sean McLaughlin, Carnegie Mellon University
The Inverse Method for Intuitionistic Modal Logic

The inverse method has been shown to be a successful strategy for automated reasoning in some non-classical logics such as intuitionistic and linear logic. This talk describes a formulation of the inverse method for theorem proving in intuitionistic modal logic (IML). Applications of IML include distributed authentication logics such as Microsoft's DKAL and Garg's proof carrying file system (PCFS). In these applications, access control is reduced to theorem proving in IML, making the proof search problem critical for any implementation. In our formulation, the Kripke accessibility relation is captured by relativizing propositions to explicit worlds. Constraints mediate between worlds in sequents, and subsumption incorporates constraint entailment. In this talk we describe the general method, and highlight some strengths and weaknesses of this approach by describing experiments comparing existing systems with our implementation.