Sciweavers

Share
ICFP
2003
ACM

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

10 years 2 months ago
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.
Alberto Momigliano, Jeff Polakow
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2003
Where ICFP
Authors Alberto Momigliano, Jeff Polakow
Comments (0)
books