FLoC '02 - LFM program

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