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
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
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
- 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
- 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!
| 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
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).
Previous MERλIN workshops were held in 2001, 2003, and 2005.
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)
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
| Important Dates
| Program committee
| Previous workshops