10:0010:30 
Coffee 
10:3011:10 
Harley D. Eades III, Aaron Stump
Hereditary Substitution for Stratified System F
Abstract:
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:1011:50 
Alexandre Viel and Dale Miller
Proof search when equality is a logical connective: Extended Abstract
Abstract:
We explore how one might do proof search in a simple, firstorder
classical logic where equality is treated as a logical connective.
That is, equality over firstorder terms has a left and right
introduction rule. The formulation of the leftintroduction 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 secondorder
unification problems. We also show that a given secondorder
unification problem in that subset can be encoded as a firstorder
formula in such a way that finding a proof of that formula solves the
unification problem. We additionally argue that solving such
secondorder unifications problems is undecidable.

11:5012:30 
Arnaud Spiwack
An abstract type for constructing tactics in Coq
Abstract:
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:3014:00 
Lunch break 
14:0014:40 
Zachary Snow, David Baelde and Gopalan Nadathur
Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search
Abstract:
Dependently typed lambdacalculi such as the Logical Framework (LF)
are capable of representing relationships between terms through
types. By exploiting the formulasastypes 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 lambdaterms 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 wellformed. 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:4015:00 
Discussion (theme and workshop) 
15:0015:30 
Coffee 
15:3016:30 
David Baelde
An overview of focusing for
least and greatest fixed points in intuitionistic logic
Abstract:
Least and greatest fixed points, corresponding to inductive and coinductive
definitions, are known to be difficult concepts in prooftheory. 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:3017:30 
Invited talk: Sean McLaughlin, Carnegie Mellon University
The Inverse Method for Intuitionistic Modal Logic
Abstract:
The inverse method has been shown to be a successful strategy for
automated reasoning in some nonclassical 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.
