[TYPES/announce] LFMTP-07: Call for participation

[Carsten Schuermann]

                   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