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