Alberto Ciaffaglione, Luigi Liquori, and Marino Miculan
Imperative object-based calculi in
(co)inductive type theories
In Moshe Vardi and Andrei Voronkov, editors, Proc. 10th Int'l
Conf. Logic for Programming Artificial Intelligence & Reasoning, volume
2850 of LNCS, Almaty, Kazakhstan, September 2003 Springer
We discuss the formalization of Abadi and Cardelli's
impvarsigma, a
paradigmatic object-based calculus with types and side effects, in
Co-Inductive Type Theories, such as the Calculus of (Co)Inductive
Constructions (CC(Co)Ind). Instead of representing directly the
original system as it is, we reformulate its syntax and semantics
bearing in mind the proof-theoretical features provided by the target
metalanguage. On one hand, this methodology allows for a smoother
implementation and treatment of the calculus in the metalanguage. On
the other, it is possible to see the calculus from a new perspective,
thus having the occasion to suggest original and cleaner
presentations. We give hence a new presentation of impvarsigma,
exploiting natural deduction semantics, (weak) higher-order abstract
syntax, and, for a significant fragment of the calculus, coinductive
typing systems. This presentation is easier to use and implement than
the original one, and the proofs of key metaproperties, e.g. subject
reduction, are much simpler. Although all proof developments have
been carried out in the Coq system, the solutions we have devised in
the encoding of and metareasoning on impvarsigma can be applied to
other imperative calculi and proof environments with similar
features.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43