LFM 2000

Workshop on Logical Frameworks and Meta-languages
Sunday, June 25, 2000
Santa Barbara, California

Held as part of the International Conference on Logic in Computer Science (LICS'2000).

Proceedings

• foreword
  
• contents
  
• TinkerType: A Language for Playing with Formal Systems
  Benjamin C. Pierce
• A Meta Logical Framework Based On Realizability
  Carsten Schuermann
• Properties of Terms in Continuation-Passing Style in an Ordered Logical Framework
  Jeffrey Polakow and Frank Pfenning
• PAL+: A Lambda-free Logical Framework
  Zhaohui Luo
• Modularity in Meta-languages
  Peter D. Mosses
• Termination of Rewriting in the Calculus of Constructions
  Daria Walukiewicz
• ELAN for Equational Reasoning in Coq
  Cuihltlauac Alvarado and Quang-Huy Nguyen