| | All
sessions take place in auditorium 10.09:00- | 09:30
| Pablo López, U Málaga,
Spain Ernesto
Pimentel, U Málaga, Spain Joshua
S. Hodas, Harvey Mudd College, USA Jeffrey
Polakow, GNP Computers, USA Lubomira
Stoilova, Harvey Mudd College, USA
**Isolating
resource comsumption in linear-logic proof search** This
work presents an extension of the Tag-Frame resource
management system previously developed by the authors. The extended system
is able to isolate the consumption of a given goal/clause without incurring
extra runtime costs. We believe this feature may help in debugging linear
logic programs and specifications in a proof-theoretic setting. |
09:30- | 10:00
| Joseph C. Vanderwaart, Carnegie Mellon U,
USA Karl
Crary, Carnegie Mellon U, USA
**A
simplified account of the metatheory of linear LF** We
present a variant of the linear logical framework LLF that
avoids the restriction that well-typed terms be in pre-canonical form and
adds *λ*-abstraction at the level
of families. We abandon the use of *β*-conversion as definitional
equality in favor of a set
of typed definitional equality judgments that include rules for parallel
conversion and extensionality. We show type-checking is decidable by giving
an algorithm to decide definitional equality for well-typed terms and
showing the algorithm is sound and complete. The algorithm and the proof of
its correctness are simplified by the fact that they apply only to
well-typed terms and may therefore ignore the distinction between
intuitionistic and linear hypotheses. |
10:00- | 10:30
| Aaron Stump, Stanford U, USA David
L. Dill, Stanford U, USA
**Producing
proofs from an arithmetic decision procedure in elliptical
LF** Software
that can produce independently checkable evidence for
the correctness of its output has received recent attention for use in
certifying compilers and proof-carrying code. CVC ("a
Cooperating Validity Checker) is a proof-producing validity checker for a
decidable fragment of first-order logic enriched with background theories.
This paper describes how proofs of valid formulas are produced from the
decision procedure for linear real arithmetic implemented in CVC. It is
shown how extensions to LF which support proof rules schematic in an arity
("elliptical" rules) are very
convenient for this purpose. |
11:00- | 11:30
| Femke van Raamsdonk, Vrije U of Amsterdam,
The Netherlands Paula
Severi, U Turin, Italy
**Eliminating
proofs from programs** This
paper presents a step in the development of an operational
approach to program extraction in type theory. In order to get a program
from a lambda term, the logical parts need to be removed. This is done by a
reduction relation →_{ε}. We study the combination
of *β*-reduction and *ε*-reduction, both in the setting
of simply typed
lambda calculus and for pure type systems. In the general setting the
properties confluence, subject reduction, and strong normalization are
studied. |
11:30- | 12:00
| Alberto Momigliano, U Leicester, UK Simon
J. Ambler, U Leicester, UK Roy
L. Crole, U Leicester, UK
**A
hybrid encoding of Howe's method for establishing congruence of
bisimilarity** We
give a short description of Hybrid, a new tool for automated
theorem proving, which was recently introduced by the authors. It provides
a form of Higher Order Abstract Syntax (HOAS) combined consistently with
induction and coinduction. We present a case study illustrating the use of
Hybrid for reasoning about the lazy *λ*-calculus. In particular,
we prove that the standard
notion of simulation is a precongruence. Although such a proof is not new,
the development is non-trivial, and we attempt to illustrate the advantages
of using Hybrid, as well as some issues which will be addressed as further
work. |
12:00- | 12:30
| Ivan Scagnetto, U Udine, Italy Marino
Miculan, U Udine, Italy
**Ambient
Calculus and its logic in the Calculus of Inductive
Constructions** The
Ambient Calculus has been recently proposed as a model of
mobility of agents in a dynamically changing hierarchy of domains. In this
paper, we describe the implementation of the theory and metatheory of
Ambient Calculus and its modal logic in the Calculus of Inductive
Constructions. We take full advantage of Higher-Order Abstract Syntax,
using the *Theory of Contexts* as a fundamental tool for
developing formally the metatheory of the object system. Among others, we
have successfully proved a set of *fresh renamings*
properties, and formalized the connection between the Theory of Contexts
and Gabbay-Pitts' "new"
quantifier. As a feedback, we introduce a new definition of satisfaction
for the Ambients logic and derive some of the properties originally assumed
as axioms in the Theory of Contexts. |
14:00- | 14:30
| David Delahaye, Chalmers U of Techn., Sweden
**A
proof dedicated meta-language** We
describe a proof dedicated meta-language, called *L*_{tac}, in the
context of the **Coq** proof assistant. This new layer of
meta-language is quite appropriate to write small and local automations.
*L*_{tac} is
essentially a small functional core with recursors and powerful
pattern-matching operators for **Coq** terms but also for
proof contexts. As *L*_{tac} is not complete, we describe
an
interface between *L*_{tac} and the full programmable
meta-language of the system (**Objective Caml**), which is also the
implementation language. This
interface is based on a quotation system where we can use *L*_{tac}'s syntax in **ML** files, and where it is possible to insert
**ML** code in *L*_{tac} scripts by means of
antiquotations. In
that way, the two meta-languages are not opposed and we give an example
where they fairly cooperate. Thus, this shows that a **LCF**-like system
with a two-level meta-language is completely
realistic. |
14:30- | 15:00
| Brigitte Pientka, Carnegie Mellon U, USA
**Memoization-based
proof search in LF: An experimental evaluation of
a prototype**
*Elf*
is a general meta-language for the
specification and implementation of logical systems in the style of the
logical framework LF. Proof search in this framework is based on the
operational semantics of logic programming. In this paper, we discuss
experiments with a prototype for memoization-based proof search for *Elf*
programs. We compare the performance of memoization-based
proof search, depth-first search and iterative deepening search using two
applications: 1) Bi-directional type-checker with subtyping and
intersection types, and 2) parsing of formulas into higher-order abstract
syntax. These experiments indicate that memoization-based proof search is a
practical and overall more efficient alternative to depth-first and
iterative deepening search. |
15:00- | 15:30
| Carsten Schürmann, Yale U, USA Serge
Autexier, DFKI Saarbrücken, Germany
**Towards
proof planning for ***M*_{ω}^{+} This
paper describes the proof planning system *P*_{ω}^{+} for the meta theorem
prover for LF implemented in Twelf. The main contributions include a formal
system that approximates the flow of information between assumptions and
goals within a meta proof, a set of inference rules to reason about those
approximations, and a soundness proof that guarantees that the proof
planner does not reject promising proof states. |
| |