Skip to Main content Skip to Navigation
Reports

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 metadatas

https://hal.inria.fr/inria-00071774
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 6:44:17 PM
Last modification on : Wednesday, June 24, 2020 - 4:19:29 PM
Long-term archiving on: : Sunday, April 4, 2010 - 10:37:18 PM

Identifiers

  • HAL Id : inria-00071774, version 1

Relations

Citation

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⟩

Share

Metrics

Record views

194

Files downloads

213