Logical Frameworks and Meta-Languages
(LFM'04)
Affiliated with IJCAR'04
Cork, Ireland, July 05, 2004
|
|
Home |
|
|
Program |
|
|
Venue |
|
|
CFP |
Programme
| 9:30-10:30 |
Invited talk (Chair: Carsten Schürmann) |
|
Jose Meseguer University of Illinois, Urbana Champaign Reflective Logics, Metalogical Frameworks, and Formal Interoperability. |
|
| 11:00-12:30 |
Logical Frameworks (Chair: Frank Pfenning) |
|
Andreas Abel Chalmers University Weak Normalization for the Simply-Typed Lambda-Calculus in Twelf, pdf. |
|
|
Jason Reed Carnegie Mellon University Redundancy Elimination for LF, pdf. |
|
|
Herman Geuvers, Freek Wiedijk University of Nijmegen A Logical Framework with Explicit Conversions, pdf. |
|
| 14:00-15:30 |
Concurrency (Chair: TBA) |
|
Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker Carnegie Mellon University, ITT Industries, Princeton University Specifying Properties of Concurrent Computations in CLF, pdf. |
|
|
Reynald Affeld, Naoki Kobayashi University of Tokyo, Tokyo Institute of Technology A Coq Library for Verification of Concurrent Programs, pdf. |
|
|
Richard Bubel, Andreas Roth, Philipp Rümmer University of Karlsruhe Ensuring the Correctness of Lightweight Tactics for JavaCard Dynamic Logic, pdf. |
|
| 16:00-17:30 |
Meta-Logical Frameworks (Chair: Jose Meseguer) |
|
Tim Sheard, Emir Pasalic OGI Meta-Programming with Built-in Type Equality, pdf. |
|
|
Aaron Stump Washington University of Saint-Louis Imperative LF Meta-Programming, pdf. |
|
|
Andrew McCreight, Carsten Schürmann Yale University A Meta-Linear Logical Framework, pdf. |