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

Affiliated with LICS and IJCAR at FLOC'06

Seattle, Washington, 16 August, 2006

LFMTP'06 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).

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'06 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 calculi. Papers focusing on experiences with encoding programming languages theory and instances of proof-carrying code or proof-carrying authorization 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

Invited talk:

Program (tentative):

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. Please use the following Submitted papers must conform to the ENTCS style preferrably using LaTeX2e and the ENTCS class files. We will post more detailled information about submission soon.

    Proceedings are to be published as a volume in the Electronic Notes in Theoretical Computer Science (ENTCS) series and will be available to participants at the workshop.

    Call for papers (txt, pdf, ps-letter, ps-a4)

    Submit a paper using easychair!

Important Dates:

    15 May 2006 Abstract Submission deadline
    22 May 2006 Paper Submission deadline
    15 June 2006 Notification of Authors
    15 July 2006 Final version
    16 August 2006 Workshop date

Program Committee:

Andrew Appel      Princeton University
Thierry Coquand Goteborg University
Martin Hofmann LMU Munich
Furio Honsell University Udine
Dale Miller Inria Futurs
Brigitte Pientka McGill University
Andrew Pitts Cambridge University
Kevin Watkins Carnegie Mellon University

Previous workshops

This workshop is continuing the series of logical frameworks and meta-languages, which started in 1999.

    LFM'99 was held in Paris, France, affiliated with LICS (IEEE Symposium on Logic in Computer Science), and organized by Amy Felty(now University of Ottawa).

    LFM'00 was held in Santa Barbara, USA, affiliated with LICS (IEEE Symposium on Logic in Computer Science), and organized by Joelle Despeyroux (INRIA). LFM'02 was held in Copenhagen, Denmark, affiliated with LICS (IEEE Symposium on Logic in Computer Science) and FLOC'02 and was organized by Frank Pfenning (Carnegie Mellon University).

    LFM'04 was held in Cork, Ireland, affiliated with IJCAR (International Joint Conference on Automated Reasoning) and organized by Carsten Schuermann (Yale University)

Previous MERλIN workshops were held in 2001, 2003, and 2005.
    MERλIN 2001 was held in Siena, Italy, June 18, 2001, in connection with IJCAR 2001 (International Joint Conference on Automated Reasoning). It was organized by Roy L. Crole, Simon J. Ambler, and Alberto Momigliano (then at University of Leicester, UK).

    MERλIN 2003 was held in Uppsala University, Sweden, August 26, 2003, and was associated with the federation meeting Principles, Logics and Implementations of high-level programming languages (PLI 2003), 25 to 29 August 2003. It was organized by Alberto Momigliano (then at University of Leicester, UK) and Marino Miculan (University of Udine, Italy).

    MERλIN 2005 was held in Talinn, Estonia, 30 September 2005, in connection with ICFP (International Conference on Functional Programming). It was organized by Alberto Momigliano (University of Edinburgh), Ivan Scagnetto (Universiy of Udine), and Alwen Tiu (INRIA Lorraine).


Brigitte Pientka      Alberto Momigliano
School of Computer Science School of Informatics
McGill University University of Edinburgh
bp at cs dot mcgill dot ca amomigl1 at inf dot ed dot ac dot uk

[ Home | News | Important Dates | Program | Program committee | Organizers | Previous workshops ]
Brigitte Pientka