Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '09, McGill University, Montreal, Canada, August 2, 2009

James Cheney (Editor), Amy P. Felty (Editor)

Research output: Contribution to conferencePaperpeer-review

Abstract

This volume contains the papers presented at the 4th International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2009), held in Montreal, Canada, August 2, 2009. This workshop is the fourth in this series of international meetings, which combines two earlier series: the LFM workshop series on "Logical Frameworks and Meta-Languages" and the MERλIN workshop series on "MEchanized Reasoning about Languages and variable bINding." The previous meetings were held in Pittsburgh, USA in 2008, Bremen, Germany in 2007, and Seattle, USA in 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 on the other have been the focus of considerable research over the last two decades, using competing and sometimes incompatible basic principles. In recent years, there has also been a tremendous amount of work around the POPLMARK challenge, which focuses on mechanizing languages involving binders. This workshop brings together designers, implementers, and practitioners working on these areas. The broad subject areas of LFMTP 2009 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 design of proof assistants, automated theorem provers, and formal digital libraries building upon logical framework technology;

•theoretical and practical issues concerning the encoding of variable binding, 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 other calculi. Papers focusing on logic translations and on experiences with encoding programming languages theory were particularly encouraged.

A total of 14 submissions were received in response to the call for papers. Each paper was reviewed by at least three referees and 9 papers were accepted for publication in these proceedings. In addition to the accepted papers, the scientific program included an invited talk given by Gilles Dowek (Ecole Polytechnique and INRIA), and an invited tutorial given by Wilmer Ricciotti (University of Bologna), both joint with the International Workshop on Proof-Search in Type Theories (PSTT).
Original languageEnglish
Publication statusPublished - 2009

Fingerprint Dive into the research topics of 'Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '09, McGill University, Montreal, Canada, August 2, 2009'. Together they form a unique fingerprint.

Cite this