Volume 196, January 2008

Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2007)

• 
  Brigitte Pientka, Carsten Schürmann: Preface. 1
• 
  Julien Narboux, Christian Urban: Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking. 3-18
• 
  Murdoch Gabbay, Stéphane Lengrand: The lambda-context Calculus. 19-35
• 
  Anders Schack-Nielsen: Induction on Concurrent Terms. 37-51
• 
  Paul Callaghan: Coercive Subtyping via Mappings of Reduction Behaviour. 53-68
• 
  Fredrik Lindblad: Higher-Order Proof Construction Based on First-Order Narrowing. 69-84
• 
  Alberto Momigliano, Alan J. Martin, Amy P. Felty: Two-Level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax. 85-93
• 
  Brigitte Pientka, Xi Li, Florent Pompigne: Focusing the Inverse Method for LF: A Preliminary Report. 95-112
• 
  William Lovas, Frank Pfenning: A Bidirectional Refinement Type System for LF. 113-128
• 
  Michael Zeller, Aaron Stump, Morgan Deters: Signature Compilation for the Edinburgh Logical Framework. 129-135
• 
  Alexandre Buisse, Peter Dybjer: Towards Formalizing Categorical Models of Type Theory in Type Theory. 137-151