About
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. This workshop will bring together designers, implementors, and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressivity and lucidity of the reasoning process.
LFMTP 2013 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as 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.
- New theory contributions: canonical frameworks, contextual frameworks, functional programming over logical frameworks.
This year's invited speaker are Dale Miller (Inria), Furio Honsell, (University of Udine), and Robert W. Harper (CMU). For information about title and abstract, see Invited Talks.
In addition, this year LFMTP will celebrate the twenty years anniversary of the publication of:
Robert Harper, Furio Honsell and Gordon Plotkin. A Framework For Defining Logics. Journal of the Association for Computing Machinery, 40(1):143-184, 1993
Accepted regular papers (alphabetical order):
- Andrew Cave and Brigitte Pientka. First-class substitutions in contextual type theory
- Floris van Doorn, Herman Geuvers and Freek Wiedijk. Explicit Convertibility Proofs in Pure Type Systems
- Mahfuza Farooque, Stéphane Graham-Lengrand and Assia Mahboubi. A bisimulation between DPLL(T) and a proof-search
- Ulrik Terp Rasmussen and Andrzej Olaf Filinski. Structural Logical Relations with Case Analysis and Equality Reasoning
- Yuting Wang and Gopalan Nadathur. Towards Extracting Explicit Proofs from Totality Checking in Twelf
Accepted Work in Progress Report:
- Vivek Nigam and Elaine Pimentel. Relating Focused Proofs with Different Polarity Assignments
Proceedings:
Accepted regular papers will be included in the ACM Digital Library. Authors are encouraged to publish auxiliary material with their paper (technical appendixes, source code, scripts, test data, etc.).
Travel Support:
Student attendees with accepted papers can apply for a SIGPLAN PAC grant to help cover travel expenses. PAC also offers other support, such as for child-care expenses during the meeting or for travel costs for companions of SIGPLAN members with physical disabilities, as well as for travel from locations outside of North America and Europe. For details on the PAC programme see here.
Organizers
- Alberto Momigliano, University of Milan
- Brigitte Pientka, McGill University
- Randy Pollack, Harvard University
Program Committee
- David Baelde, ENS
- James Cheney, Edinburgh
- Adam Chlipala, MIT
- Dan Licata, CMU/IAS
- Alberto Momigliano, Milano
- Brigitte Pientka, McGill
- Nicolas Pouillard ITU
- Randy Pollack, Harvard
- Andrei Popescu, TUM
- Florian Rabe, Bremen
- Stephanie Weirich, UPenn
Questions: Send email to Brigitte Pientka (bpientka at cs.mcgill.ca)