LFM'02 Program
Third International Workshop on
Logical Frameworks and Meta-Languages
(LFM'02)
A FLoC'02 affiliated workshop
Copenhagen, Denmark, July 26, 2002
|
| 9:00 |
Isolating Resource Consumption in Linear-Logic Proof Search |
| |
Pablo López, Universidad de Málaga,
Ernesto Pimentel, Universidad de Málaga,
Joshua S. Hodas, Harvey Mudd College,
Jeffrey Polakow, GNP Computers, and
Lubomira Stoilova, Harvey Mudd College
|
|
| 9:30 |
A Simplified Account of the Metatheory of Linear LF |
| |
Joseph C. Vanderwaart and Karl Crary, Carnegie Mellon University |
|
| 10:00 |
Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF |
| |
Aaron Stump and David L. Dill, Stanford University |
|
|
| 11:00 |
Eliminating Proofs from Programs |
| |
Femke van Raamsdonk, Vrije Universiteit Amsterdam, and
Paula Severi, Università degli Studi di Torino
|
|
| 11:30 |
A Hybrid Encoding of Howe's Method for Establishing Congruence of Bisimilarity |
| |
Alberto Momigliano, Simon J. Ambler, and Roy L. Crole, University of Leicester |
|
| 12:00 |
Ambient Calculus and its Logic in the Calculus of Inductive Constructions |
| |
Ivan Scagnetto and Marino Miculan, Università di Udine |
|
|
| 14:00 |
A Proof Dedicated Meta-Language |
| |
David Delahaye, Chalmers University of Technology |
|
| 14:30 |
Memoization-based Proof Search in LF: An Experimental Evaluation of a Prototype |
| |
Brigitte Pientka, Carnegie Mellon University |
|
| 15:00 |
Towards Proof Planning for M-omega+ |
| |
Carsten Schürmann, Yale University, and Serge Autexier, DKFI Saarbrücken |
|
|
| 16:00 |
System Demonstrations |
|
|
[ Home
| Program
| Proceedings
| Call for Papers
| FLoC'02
]
fp@cs
Frank Pfenning
|