15 July 2007
Bremen, Germany
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