[isabelle] LFMTP-07: Call for participation
- To: lics-request at dcs.ed.ac.uk, bra-types at cs.chalmers.se, types-wg at durham.ac.uk, appsem at cs.chalmers.se, logic at theory.lcs.mit.edu, logic at CS.Cornell.EDU, types-list at lists.seas.upenn.edu, types at cs.indiana.edu, concurrency at cwi.nl, theorynt at listserv.nodak.edu, linear at cs.stanford.edu, rewriting at ens-lyon.fr, qed at mcs.anl.gov, coq-club at pauillac.inria.fr, info-hol at jaguar.cs.byu.edu, isabelle-users at cl.cam.ac.uk, pvs at csl.sri.com, theorem-provers at ai.mit.edu, lprolog at cs.umn.edu, carsten at itu.dk, types at lists.chalmers.se, prog-lang at diku.dk
- Subject: [isabelle] LFMTP-07: Call for participation
- From: Carsten Schuermann <carsten at itu.dk>
- Date: Tue, 12 Jun 2007 16:36:38 +0200
- User-agent: Thunderbird 22.214.171.124 (Macintosh/20070221)
Second International Workshop on
Logical Frameworks and Meta-Languages:
Theory and Practice
15 July, 2007
A CADE-21 affiliated workshop
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
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.
Locally Nameless Representation and Nominal Isabelle
Alberto Momigliano, Alan J. Martin and Amy P. Felty.
Two-Level Hybrid: A System for Reasoning Using Higher-Order
William Lovas and Frank Pfenning.
A Bidirectional Refinement Type System for LF
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
Induction on Concurrent Terms
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
I hope to see you there,
This archive was generated by a fusion of
Pipermail (Mailman edition) and