[TYPES] Call for participation: LFM'04 - Logical Frameworks and Meta-languages

[Carsten Schuermann]

                    Fourth International Workshop on
                 Logical Frameworks and Meta-Languages
                                (LFM'04)

                 http://www.cs.yale.edu/~carsten/lfm04

                     A IJCAR'04 affiliated workshop
                   Cork, Ireland, July 04 - 08, 2004
                 http://4c.ucc.ie/ijcar/index.html


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

The workshop will be held on Monday, Jul 5 2004, as part of IJCAR'04.
The programme can be found on the workshop homepage

                 http://www.cs.yale.edu/~carsten/lfm04/prog.html

Invited speaker:

  Jose Meseguer: University of Illinois, Urbana Champaign
    Reflective Logics, Metalogical Frameworks, and Formal Interoperability

Accepted Papers:

  Andreas Abel, Chalmers University
    Weak Normalization for the Simply-Typed Lambda-Calculus in Twelf

  Jason Reed, Carnegie Mellon University
    Redundancy Elimination for LF

  Herman Geuvers, Freek Wiedijk, University of Nijmegen
    A Logical Framework with Explicit Conversions

  Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker,
      Carnegie Mellon University, ITT Industries, Princeton University
    Specifying Properties of Concurrent Computations in CLF,

  Reynald Affeld,  Naoki Kobayashi,
      University of Tokyo, Tokyo Institute of Technology
    A Coq Library for Verification of Concurrent Programs,

  Richard Bubel, Andreas Roth, Philipp Ruemmer, University of Karlsruhe
    Ensuring the Correctness of Lightweight Tactics for JavaCard Dynamic
Logic.

  Tim Sheard, Emir Pasalic, OGI
    Meta-Programming with Built-in Type Equality.

  Aaron Stump, Washington University of Saint-Louis
    Imperative LF Meta-Programming.

  Andrew McCreight, Carsten Schuermann, Yale University
    A Meta-Linear Logical Framework.


Hope to see you there,

Carsten Schuermann
Department of Computer Science
Yale University

carsten at cs.yale.edu
http://www.cs.yale.edu/~carsten/lfm04