MERLIN 2005 Proceedings

• Towards a type theory of contexts
  Frank Pfenning

• A computational approach to reflective meta-reasoning about languages with bindings
  Aleksey Nogin, Alexei Kopylov, Xin Yu, Jason Hickey
• A unified category-theoretic formulation of typed binding signatures
  Miki Tanaka, John Power
• A formal treatment of the barendregt variable convention in rule inductions
  Christian Urban, Michael Norrish
• Toward a general theory of names: binding and scope
  James Cheney
• Translating specifications from nominal logic to CIC with the theory of contexts
  Marino Miculan, Ivan Scagnetto, Furio Honsell
• Types with semantics: soundness proof assistant
  Olha Shkaravska
• Combining higher-order abstract syntax with first-order abstract syntax in ATS
  Kevin Donnelly, Hongwei Xi