LFM on Friday

Detailed program
Friday July 26th, 2002
See also the unified by-slot program

All sessions take place in auditorium 10.

Session 1

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.

Session 2

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.

Session 3

14:00-14:30  David Delahaye, Chalmers U of Techn., Sweden
A proof dedicated meta-language
We describe a proof dedicated meta-language, called Ltac, in the context of the Coq proof assistant. This new layer of meta-language is quite appropriate to write small and local automations. Ltac is essentially a small functional core with recursors and powerful pattern-matching operators for Coq terms but also for proof contexts. As Ltac is not complete, we describe an interface between Ltac 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 Ltac's syntax in ML files, and where it is possible to insert ML code in Ltac 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.

16:00-17:30  Session 4: System Demonstrations