MERλIN 2003
Second ACM SIGPLAN Workshop on
MEchanized Reasoning about Languages with varIable biNding


8:45 Welcome
Scope, binding, and inlining in the Glasgow Haskell Compiler (Invited Talk)
Simon Peyton-Jones (Microsoft Research, UK)

10:00--10:30 Coffee Break
Compiler Implementation in a Formal Logical Framework
Jason Hickey, Aleksey Nogin, Adam Granicz, and Brian Aydemir
Verifying CPS transformations in Isabelle/HOL
Yasuhiko Minamide and Koji Okuma

Mechanising Hankin and Barendregt using the Gordon-Melham axioms

Michael Norrish
Reasoning on an Imperative Object-based Calculus in Higher Order Abstract Syntax
Alberto Ciaffaglione, Luigi Liquori and Marino Miculan
12:30--14:15 Lunch
A unified category-theoretic approach to variable binding
John Powers
A Definitional Approach to Primitive Recursion over Higher Order Abstract Syntax
S. Ambler, R. Crole and A. Momigliano
Representing Reductions of NP-Complete Problems in Logical Frameworks - A Case Study
Jatin Shah and Carsten Schürmann

15:45--16:15 Tea Break
A Formalization of an Ordered Logical Framework in Hybrid with Applications to Continuation Machines (20 min)
Alberto Momigliano and Jeff Polakow
Towards a Dependent Modal Type Theory (20 min)
Aleksandar Nanevski, Brigitte Pientka and Frank Pfenning
Explicit Substitutions and Higher Order Syntax (20 min)
Neil Ghani and Tarmo Uustalu

Swapping the Atom: Programming with Binders in Fresh O'Caml (10 min)

Mark R. Shinwell
Reasoning about Recursive Procedures with Parameters
Ralph-Johan Back and Viorel Preoteasa

Created by Alberto Momigliano. Last modified: Jul 29, 2003