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:

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):

Accepted Work in Progress Report:


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.


Program Committee

Questions: Send email to Brigitte Pientka (bpientka at cs.mcgill.ca)