----------------------------------------------------------------------- International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'06) http://www.cs.mcgill.ca/~bpientka/lfmtp06/index.html Affiliated with LICS and IJCAR at FLOC'06 Seattle, Washington, 16 August, 2006. CALL FOR PAPERS Important Dates: Submission deadline: 15 May 2006 Author Notification: 15 June 2006 Final Version: 15 July 2006 ----------------------------------------------------------------------- LFMTP'06 merges the International workshop on Logical Frameworks and Meta-languages (LFM) and the MERLIN workshop on MEchanized Reasoning about Languages with variable BIndingIN). 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 one hand and their applications, for example, to 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 binding signatures. * Case studies of meta-programming, and the mechanization of the (meta)theory 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 * sub-structural frameworks * semantic foundations * methods for reasoning about logics * case studies. Invited Speaker: Gordon Plotkin (University of Edinburgh). Program Committee: Andrew Appel Princeton University Thierry Coquand Goteborg University Martin Hofmann LMU Munich Furio Honsell University of Udine Dale Miller Inria Futurs Brigitte Pientka McGill University Andrew Pitts Cambridge University Kevin Watkins Carnegie Mellon University Paper Submissions. Three categories of papers are solicited: * Category A: Detailed and technical accounts of new research: up to fifteen pages including bibliography. * Category B: Shorter accounts of work in progress and proposed further directions, including discussion papers: up to eight pages including bibliography. * 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. Submitted papers must conform to the ENTCS style, preferably using LaTeX2e. For further information and submission instructions, see the LFMTP web page: http://www.cs.mcgill.ca/~bpientka/lfmtp06/index.html 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. Organizers: Brigitte Pientka Alberto Momigliano bpientka@cs.mcgill.ca amomigl1@inf.ed.ac.uk School of Computer Science LFCS, School of Informatics McGill University University of Edinburgh