MERLIN (ICFP 2003 Workshop): Uppsala, Sweden

• S. J. Ambler, Roy L. Crole, Alberto Momigliano:
  A definitional approach to primitivexs recursion over higher order abstract syntax.
  
• Michael Norrish:
  Mechanising Hankin and Barendregt using the Gordon-Melham axioms.
  
• Alberto Momigliano, Jeff Polakow:
  A formalization of an Ordered Logical Framework in Hybrid with applications to continuation machines.
  
• Alberto Ciaffaglione, Luigi Liquori, Marino Miculan:
  Reasoning on an imperative object-based calculus in Higher Order Abstract Syntax.
  
• Ralph-Johan Back, Viorel Preoteasa:
  Reasoning about recursive procedures with parameters.
  
• Jason Hickey, Aleksey Nogin, Adam Granicz:
  Compiler implementation in a formal logical framework.
  
• Yasuhiko Minamide, Koji Okuma:
  Verifying CPS transformations in Isabelle/HOL.
  
• John Power:
  A unified category theoretic approach to variable binding.
  
• Carsten Schürmann, Jatin Shah:
  Representing reductions of NP-complete problems in logical frameworks: a case study.
  
• Neil Ghani, Tarmo Uustalu:
  Explicit substitutions and higher-order syntax.
  
• Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning:
  A modal foundation for meta-variables.