LFM'02 Program

Third International Workshop on
Logical Frameworks and Meta-Languages
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 ]

Frank Pfenning