[isabelle] CFP: LFMTP'07

      International Workshop on Logical Frameworks and Meta-Languages:
      Theory and Practice (LFMTP'07)

              Affiliated with CADE-21
              Bremen, Germany, 15 July, 2007

               FINAL CALL FOR PAPERS


Important Dates:

Abstract Submission      7 May    2007
Submission deadline:    13 May    2007
Author Notification:     3 June   2007
Final Version:          17 June   2007
Workshop day            15 July   2007


LFMTP'07 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.

The broad subject areas of LFMTP'07 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
* 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: Randy Pollack, University of Edinburgh

Program Committee:

Andreas Abel	       (LMU Munich)
Peter Dybjer	       (Chalmers University)
Marino Miculan	       (University Udine)
Dale Miller	       (INRIA Futurs)
Brigitte Pientka       (McGill University)
Benjamin Pierce	       (University of Pennsylvania)
Carsten Schuermann     (IT University of Copenhagen, PC Chair)
Christian Urban        (TU Munich)

   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:

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.


Brigitte Pientka              Carsten Schuermann
bpientka at cs.mcgill.ca         carsten at itu.dk
School of Computer Science    Department of Theoretical Computer Science
McGill University             IT University of Copenhagen

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.