EPTCS 71
Proceedings Sixth International Workshop on
Logical Frameworks and Meta-languages: Theory and Practice
Nijmegen, The Netherlands, August 26, 2011
Edited by: Herman Geuvers and Gopalan Nadathur
This volume constitutes the proceedings of the Sixth International
Workshop on Logical Frameworks and Meta-languages: Theory and
Practice, LFMTP 2011. 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 use
in reasoning tasks ranging from the correctness of software to the
properties of formal computational systems on the other hand have been
the focus of considerable research over the last two decades. The
LFMTP workshop series, which resulted from the amalgamation of the
Logical Frameworks and Meta-languages (LFM) and the Mechanized
Reasoning about Languages with Variable Binding (MERλIN)
workshop series, is intended to bring together designers,
implementors, and practitioners to discuss various aspects impinging
on the structure and utility of logical frameworks. The topics that
have been covered in the various editions of this workshop and its
precursors have included the following:
- Encoding and reasoning about the meta-theory of programming
languages and related formally specified systems.
- Theoretical and practical issues concerning the treatment of
variable binding, especially the representation of, and reasoning
about, datatypes defined from binding signatures.
- Logical treatments of inductive and co-inductive definitions and
associated reasoning techniques.
- Case studies of meta-programming, and the mechanization of the
(meta)theory of descriptions of programming languages and other
calculi, especially ones focusing on logic translations and on
experiences with encoding programming languages theory.
LFMTP 2011 was held on August 26, 2011 in Nijmegen, Netherlands, as a
workshop associated with ITP 2011, the Second International Conference
on Interactive Theorem Proving. In addition to presentations of the
contributed papers contained in this proceedings, the program included
invited talks by Henk Barendregt (Radboud University, Netherlands) and
Michael Norrish (NICTA, Australia). Further, its program was
integrated with that of the MLPA 11, the Third Workshop on Modules and
Libraries for Proof Assistants.The full program can be found at the
web site for LFMTP 2011.
LFMTP is a refereed workshop series. In 2011, papers were invited with
May 23 as a deadline for submission. Each contributed papers was
reviewed by three members of the program committee that consisted of
the following individuals:
- Claudio Sacerdoti Coen (University of Bologna)
- Herman Geuvers (Program Co-Chair, Radboud University
Nijmegen)
- James McKinna (Radboud University Nijmegen)
- Gopalan Nadathur (Program Co-Chair, University of Minnesota)
- Frank Pfenning (Carnegie Mellon University)
- Alwen Tiu (Australian National University)
- Christian Urban (TU Munich)
Acceptance decisions were made by consensus, based on the
reviews. Authors of accepted papers were given an opportunity to
revise their manuscripts prior to their presentation to take
cognizance of the reviews. A further such opportunity was provided to
take account of the feedback obtained at the workshop. The papers
contained in these proceedings are the end result of this process.
Herman Geuvers
Gopalan Nadathur