A formalization of an Ordered Logical Framework in Hybrid with applications to continuation machines

We report on work in progress devoted to the formalization of an Ordered Logical Framework (OLF) based on a two-level architecture [8] in the Hybrid system. OLF here is a second-order version of ordered linear logic to be used as a meta-language for the verification of the (meta)theory of deductive systems. It is implemented as a meta-interpreter on top of the Hybrid system, which provides the full HOAS language. We apply the framework to the formal verification of type preservation of a simple continuation machine for Mini-ML.

• Type: Conference
• Year: 2003
• Where: ICFP
• Authors: Alberto Momigliano, Jeff Polakow
• Keywords: Formal Verification, Hybrid System, ICFP 2003, Programming Languages, Simple Continuation Machine