International Workshop on Logical Frameworks and Meta-Languages:
Theory and Practice (LFMTP'07)
Affiliated with CADE-21 at
Bremen, Germany, 15 July, 2007
LFMTP'07 continues the International Workshop on Logical Frameworks and Meta-languages (LFM) and merges it with the workshop on
MEchanized Reasoning about Languages with variable
BInding (MERλIN). A first version of LFMTP was held at FLOC'06..
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
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
Randy Pollack, University of Edinburgh
The full program of the day can be found here.
The final proceeding will be published in ENTCS (Electronic Notes in Theoretical Computer Science). A preliminary version of the proceeding can be found here.
| Brigitte Pientka
|| Carsten Schürmann
| School of Computer Science
|| Department of Theoretical Computer Science
| McGill University
|| IT University of Copenhagen
| bp at cs dot mcgill dot ca
|| carsten at itu dot dk
| Previous workshops