MERλIN 2003
Second ACM SIGPLAN Workshop on
MEchanized Reasoning about Languages with varIable biNding
|
MERλIN 2003
|
|
| 8:45 Welcome |
| 9:00--10:00 |
| Scope, binding, and inlining in the
Glasgow Haskell Compiler (Invited Talk) |
| Simon Peyton-Jones (Microsoft Research, UK) |
| 10:00--10:30 Coffee Break |
| 10:30--12:30 |
| 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 |
| 14:15--15:45 |
| 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 |
| 16:15--18:00 |
| 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 |