Electronic Notes in Theoretical Computer Science, Volume 196

Volume 196, January 2008

• 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