HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

On the Formalization of Imperative Object-based Calculiin (Co)Inductive Type Theories

Alberto Ciaffaglione 1, 2, 3 Luigi Liquori 4, 3 Marino Miculan 1
3 MIRHO - Objects, types and prototypes : semantics and validation
CRISAM - Inria Sophia Antipolis - Méditerranée , UHP - Université Henri Poincaré - Nancy 1, Université Nancy 2, INPL - Institut National Polytechnique de Lorraine, CNRS - Centre National de la Recherche Scientifique : UMR7503
Abstract : In this paper, we study the formalization of Abadi and Cardelli's impsigma, a representative object-based calculus with types and side effects, in interactive proof assistants based on (Co)Inductive Type Theories, Like Coq. In order to make the formal development of the theory of impsigma easier, we reformulate its static and dynamic semantics taking most advantage of the features provided by CC^(Co)Ind, the coinductive type theory underlying Coq. The new presentation is thus in the style of Natural Deduction Semantics (the counterpart in Natural Deduction style of Kahn's Natural semantics), using higher-order abstract syntax and hypothetical-general premises à la Martin-Löf. Interestingly, for a significant fragment of impsigma we can even use coinductive typing systems, thus avoiding "store types" and leading to a substantial simplification of the proofs of key metaproperties, such as Subject Reduction. The solutions we have devised in the encoding of and metareasoning on can be readily applied to other imperative calculi featuring similar issues.
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 6:44:17 PM
Last modification on : Friday, February 4, 2022 - 3:23:59 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:37:18 PM


  • HAL Id : inria-00071774, version 1


Alberto Ciaffaglione, Luigi Liquori, Marino Miculan. On the Formalization of Imperative Object-based Calculiin (Co)Inductive Type Theories. [Research Report] RR-4812, INRIA Nancy; LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy; INRIA. 2003, pp.37. ⟨inria-00071774⟩



Record views


Files downloads