Reasoning on an imperative object-based calculus in higher order abstract syntax : dart-reports : Cia+Liq+Mic:merlin03

Alberto Ciaffaglione, Luigi Liquori, and Marino Miculan

Reasoning on an imperative object-based calculus in higher order abstract syntax

In Proc. 2nd MERlambdaIN, ACM Digital Library, Uppsala, Sweden, 2003 ACM

We illustrate the benefits of using Natural Deduction in combination with weak Higher-Order Abstract Syntax for formalizing an object-based calculus with objects, cloning, method-update, types with subtyping, and side-effects, in inductive type theories such as the Calculus of Inductive Constructions. This setting suggests a clean and compact formalization of the syntax and semantics of the calculus, with an efficient management of method closures. Using our formalization and the Theory of Contexts, we can prove formally the Subject Reduction Theorem in the proof assistant Coq, with a relatively small overhead.

[ bib | .pdf ]

Back

This file has been generated by bibtex2html 1.43