LFM program

Friday July 26th, 2002

All sessions take place in auditorium 10.

LFM's program is also available with abstracts or side by side with other meetings.

09:00-10:30  Session 1

09:00  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; and Lubomira Stoilova, Harvey Mudd College, USA
Isolating resource comsumption in linear-logic proof search
09:30  Joseph C. Vanderwaart and Karl Crary, Carnegie Mellon U, USA
A simplified account of the metatheory of linear LF
10:00  Aaron Stump and David L. Dill, Stanford U, USA
Producing proofs from an arithmetic decision procedure in elliptical LF

10:30-11:00  Refreshments

11:00-12:30  Session 2

11:00  Femke van Raamsdonk, Vrije U of Amsterdam, The Netherlands and Paula Severi, U Turin, Italy
Eliminating proofs from programs
11:30  Alberto Momigliano, Simon J. Ambler, and Roy L. Crole; U Leicester, UK
A hybrid encoding of Howe's method for establishing congruence of bisimilarity
12:00  Ivan Scagnetto and Marino Miculan, U Udine, Italy
Ambient Calculus and its logic in the Calculus of Inductive Constructions

12:30-14:00  Lunch

14:00-15:30  Session 3

14:00  David Delahaye, Chalmers U of Techn., Sweden
A proof dedicated meta-language
14:30  Brigitte Pientka, Carnegie Mellon U, USA
Memoization-based proof search in LF: An experimental evaluation of a prototype
15:00  Carsten Schürmann, Yale U, USA and Serge Autexier, DFKI Saarbrücken, Germany
Towards proof planning for Mω+

15:30-16:00  Refreshments

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