We report on work in progress devoted to the formalization of an Ordered Logical Framework (OLF) [16] based on a twolevels 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 metainterpreter 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.
A formalization of an Ordered Logical Framework in Hybrid with applications to continuation machines / A. Momigliano, J. Polakow - In: MERLIN '03: Proceedings[s.l] : ACM, 2003. - ISBN 1581138008. - pp. 1-9 (( convegno ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding, MERLIN tenutosi a Uppsala nel 2003 [10.1145/976571.976581].
A formalization of an Ordered Logical Framework in Hybrid with applications to continuation machines
A. Momigliano
Primo
;
2003
Abstract
We report on work in progress devoted to the formalization of an Ordered Logical Framework (OLF) [16] based on a twolevels 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 metainterpreter 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.
| File | Dimensione | Formato | |
|---|---|---|---|
|
p10-momigliano.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
250.28 kB
Formato
Adobe PDF
|
250.28 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
