[Prev][Next][Index][Thread]

LFM'02 Program and Call for Participation


		   Program and Call for Participation

		    Third International Workshop on
		 Logical Frameworks and Meta-Languages
				(LFM'02)

		     http://www.cs.cmu.edu/~lfm02/

		     A FLoC'02 affiliated workshop
		   Copenhagen, Denmark, July 26, 2002
			 http://floc02.diku.dk/


Logical frameworks and meta-languages form a common substrate for
representing, implementing, and reasoning about a wide variety of
deductive systems of interest in logic and computer science.  Their
design and implementation has been the focus of considerable research
over the last two decades, using competing and sometimes incompatible
basic principles.  This workshop will bring together designers,
implementors, and practitioners to discuss all aspects of logical
frameworks.

Informal proceedings will be published as a volume in the Electronic
Notes in Theoretical Computer Science (ENTCS) and will be available
at the workshop.

The workshop is open for any interested party.  If you are planning to
attend you are welcome to participate in the informal system
demonstration session.  Please send mail to the workshop chair (Frank
Pfenning <fp@cs.cmu.edu>) if you are interested in showing your
implementation.

==================================================
LFM'02 Program
July 26, 2002
==================================================
Session 1

9:00-9:30
Isolating Resource Comsumption in Linear-Logic Proof Search
Pablo Lopez, Universidad de Malaga,
Ernesto Pimentel, Universidad de Malaga,
Joshua S. Hodas, Harvey Mudd College,
Jeffrey Polakow, GNP Computers, and
Lubomira Stoilova, Harvey Mudd College

9:30-10:00
A Simplified Account of the Metatheory of Linear LF
Joseph C. Vanderwaart and Karl Crary, Carnegie Mellon University

10:00-10:30
Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF
Aaron Stump and David L. Dill, Stanford University
--------------------------------------------------
Coffee Break
10:30-11:00
--------------------------------------------------
Session 2

11:00-11:30
Eliminating Proofs from Programs
Femke van Raamsdonk, Vrije Universiteit Amsterdam, and
Paula Severi, Universidad de la Republica Montevideo

11:30-12:00
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-12:30
Ambient Calculus and its Logic in the Calculus of Inductive Constructions
Ivan Scagnetto and Marino Miculan, Universita di Udine
--------------------------------------------------
Lunch Break
12:30-14:00
--------------------------------------------------
Session 3

14:00-14:30
A Proof Dedicated Meta-Language
David Delahaye, Chalmers University of Technology

14:30-15:00
Memoization-Based Proof Search in LF: An Experimental Evaluation of a Prototype
Brigitte Pientka, Carnegie Mellon University

15:00-15:30
Towards Proof Planning for M-omega+
Carsten Schurmann, Yale University, and
Serge Autexier, DKFI Saarbrucken
--------------------------------------------------
Coffee Break
15:30-16:00
--------------------------------------------------
Session 4

16:00-17:30
System Demonstrations
==================================================


PROGRAM COMMITTEE:

    David Basin,            University of Freiburg
    Thierry Coquand,	    Goteborg University
    Amy Felty,		    University of Ottawa
    Didier Galmiche,	    LORIA Nancy
    Dale Miller,	    Penn State University
    Tobias Nipkow,	    Technical University Munich
    Frank Pfenning (chair), Carnegie Mellon University
    Benjamin Pierce,	    University of Pennsylvania
    Benjamin Werner	    INRIA Rocquencourt

CONTACT

    Frank Pfenning
    Department of Computer Science
    Carnegie Mellon University

    fp@cs.cmu.edu
    http://www.cs.cmu.edu/~lfm02