[PVS] LFMTP-07: Call for participation

[Carsten Schuermann <carsten@xxxxxx>]

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

                  15 July, 2007
                             Bremen, Germany
               http://www.cs.mcgill.ca/~bpientka/lfmtp07/

                     A CADE-21 affiliated workshop
            http://www.cadeconference.org/meetings/cade21/


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 has been the focus of considerable research
over the last two decades, using competing and sometimes incompatible
basic principles.

This workshop will bring together designers, implementors, and
practitioners to discuss all aspects of logical frameworks.  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.
       Locally Nameless Representation and Nominal Isabelle

Accepted papers:

     Alberto Momigliano, Alan J. Martin and Amy P. Felty.
       Two-Level Hybrid: A System for Reasoning Using Higher-Order 
Abstract Syntax

     William Lovas and Frank Pfenning.
       A Bidirectional Refinement Type System for LF

     Paul Callaghan.
       Coercive Subtyping via Mappings of Reduction Behaviour

     Brigitte Pientka, Florent Pompigne and Xi Li.
       Focusing the Inverse Method for LF: a Preliminary Report

     Julien Narboux and Christian Urban.
       A Formalisation of the Logical Relation Proof given by Crary for
       Completeness of Equivalence Checking

     Alexandre Buisse and Peter Dybjer.
       Formalizing Categorical Models of Type Theory in Type Theory

     Michael Zeller, Aaron Stump and Morgan Deters.
       A Signature Compiler for the Edinburgh LF

     Anders Schack-Nielsen.
       Induction on Concurrent Terms

     Fredrik Lindblad.
       Higher-Order Proof Construction Based on First-Order Narrowing

     Murdoch Gabbay and Stephane Lengrand.
       The Lambda Context Calculus

Registration to the LFMTP workshop is independent from registration to
CADE-21.  http://www.cadeconference.org/meetings/cade21/registration.html


I hope to see you there,

Best regards,
Carsten Schuermann