Electronic Notes in Theoretical Computer Science, Volume 199

Volume 199, February 2008

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages (LFM 2004)

Carsten Schürmann:
Preface. 1-2
Andreas Abel:
Normalization for the Simply-Typed Lambda-Calculus in Twelf. 3-16
Reynald Affeldt, Naoki Kobayashi:
A Coq Library for Verification of Concurrent Programs. 17-32
Herman Geuvers, Freek Wiedijk:
A Logical Framework with Explicit Conversions. 33-47
Tim Sheard, Emir Pasalic:
Meta-programming With Built-in Type Equality. 49-65
Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker:
Specifying Properties of Concurrent Computations in CLF. 67-87
Jason Reed:
Redundancy Elimination for LF. 89-106
Richard Bubel, Andreas Roth, Philipp Rümmer:
Ensuring the Correctness of Lightweight Tactics for JavaCard Dynamic Logic. 107-128
Andrew McCreight, Carsten Schürmann:
A Meta Linear Logical Framework. 129-147
Aaron Stump:
Imperative LF Meta-Programming. 149-159

Last update Fri May 17 20:02:59 2013 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page