International Workshop on Logical Frameworks and Meta-Languages:
Theory and Practice (LFMTP'07)

Affiliated with CADE-21 at

Bremen, Germany, 15 July, 2007

LFMTP'07 continues the International Workshop on Logical Frameworks and Meta-languages (LFM) and merges it with the workshop on MEchanized Reasoning about Languages with variable BInding (MERλIN). A first version of LFMTP was held at FLOC'06..

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 on the one hand and their applications in for example proof-carrying code have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors, and practitioners to discuss all aspects of logical frameworks.

The broad subject areas of LFMTP'07 are

  • The automation and implementation of the meta-theory of programming languages and related calculi, particularly work which involves variable binding and fresh name generation.
  • The theoretical and practical issues concerning the encoding of variable binding and fresh name generation, especially the representation of, and reasoning about, datatypes defined from binding signatures.
  • Case studies of meta-programming, and the mechanization of the (meta)theory of descriptions of programming languages and other calculi. Papers focusing on logic translations and on experiences with encoding programming languages theory are particularly welcome.

Topics include, but are not limited to

  • logical framework design
  • meta-theoretic analysis
  • applications and comparative studies
  • implementation techniques
  • efficient proof representation and validation
  • proof-generating decision procedures and theorem provers
  • proof-carrying code
  • substructural frameworks
  • semantic foundations
  • methods for reasoning about logics
  • formal digital libraries

Paper submission:

  • Category A: Detailed and technical accounts of new research: up to fifteen pages including bibliography. An additional appendix which contains details of proofs may be attached.
  • Category B: Shorter accounts of work in progress and proposed further directions, including discussion papers: (up to eight pages) pages including bibliography and appendices.
  • Category C: System descriptions presenting an implemented tool and its novel features: (up to six pages). A demonstration is expected to accompany the presentation.

Submission is electronic in postscript or PDF format using easychair. Submitted papers must conform to the ENTCS style preferrably using LaTeX2e and the ENTCS class files.

To submit a paper, please use EasyChair!

Papers from program committee members are encouraged.

Authors of accepted papers are expected to present their paper at the workshop. Workshop proceedings with the papers presented at the workshop will be available to participants at the workshop and a final version of this proceeding will be most likely be published as a volume in the Electronic Notes in Theoretical Computer Science (ENTCS).

Important Dates (tentative):

    7 May 2007 Abstract Submission deadline
    13 May 2007 Paper Submission deadline
    3 June 2007 Notification of Authors
    17 June 2007 Final version
    15 July 2007 Workshop date

Program Committee:

Andreas Abel      LMU Munich
Peter Dybjer Chalmers University
Marino Miculan University of Udine
Dale Miller Inria Futurs
Brigitte Pientka McGill University
Benjamin Pierce University of Pennsylvania
Carsten Schürmann IT University of Copenhagen (Program Chair)
Christian Urban TU Munich


Brigitte Pientka      Carsten Schürmann
School of Computer Science Department of Theoretical Computer Science
McGill University IT University of Copenhagen
bp at cs dot mcgill dot ca carsten at itu dot dk

[ Home | CFP | Program | Program committee | Organizers | Previous workshops ]
Brigitte Pientka