A formalization of an Ordered Logical Framework in Hybrid with applications to continuation machines
Alberto Momigliano, Jeff Polakow · 2003
We report on work in progress devoted to the formalization of an Ordered Logical Framework (OLF) [16] based on a two-levels architecture [10] in the Hybrid system [2]. 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 roughly 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.