Update: - invited speaker: Dale Miller - submission server now open (abstract deadline: 14 April) International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08) http://www4.in.tum.de/~lfmtp Pittsburgh, PA, USA, 23 June 2008 Affiliated with Logic in Computer Science (LICS 2008) 2nd CALL FOR PAPERS Important dates: --------------------------------------------------------------------- Abstract submission: 14 April 2008 Paper submission: 21 April 2008 Author notification: 19 May 2008 Final version: 2 June 2008 Workshop day: 23 June 2008 --------------------------------------------------------------------- The LFMTP workshop continues 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 the one hand and their applications in for example 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 and variable binding. The broad subject areas of LFMTP'08 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 descriptions of programming languages and other calculi. Papers focusing on logic translations and on experiences with encoding programming languages theory 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 * substructural frameworks * semantic foundations * methods for reasoning about logics * formal digital libraries Invited Speaker: Dale Miller (Laboratoire d'Informatique, INRIA Saclay) Program Committee: Andreas Abel (LMU Munich) Peter Dybjer (Chalmers University of Technology) Alberto Momigliano (University of Edinburgh) Brigitte Pientka (McGill University) Randy Pollack (University of Edinburgh) Carsten Schuermann (IT University of Copenhagen) Peter Sewell (University of Cambridge) Aaron Stump (Washington University) Christian Urban (TU Munich) 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 and appendices. * 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. Authors are required to submit a paper title and a short abstract of about 100 words before submitting the paper. Papers are to be submitted in postscript or PDF format and must conform to the ENTCS style preferably using LaTeX2e. For further information and submission instructions, see the LFMTP web page: http://www4.in.tum.de/~lfmtp 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. Authors of accepted papers are expected to present their paper at the workshop. The organizers: Andreas Abel Christian Urban Theoretical Computer Science Institute for Computer Science Ludwig-Maximilians-University Munich Technical University of Munich Email: andreas.abel@ifi.lmu.de Email: urbanc@in.tum.de -- Andreas Abel <>< Du bist der geliebte Mensch. Theoretical Computer Science, University of Munich http://www.tcs.informatik.uni-muenchen.de/~abel/