-----------------------------------------------------------------------
   
    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 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. 

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 descriptions 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
    * substructural 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 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 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 in postscript or PDF format. Submitted papers
must conform to the ENTCS style preferrably 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    Scholl of Informatics
McGill University             University of Edinburgh