Electronic Notes in Theoretical Computer Science, Volume 196

Volume 196, January 2008

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