Electronic Notes in Theoretical Computer Science, Volume 199

Volume 199, February 2008

• 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