Paper Info
Title
Imperative Object-Based Calculi in Co-inductive Type Theories
Abstract
We discuss the formalization of Abadi and Cardelli's imps, 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 anew presentation of imps, 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 imps can be applied to other imperative calculi and proof environments with similar features.
Year
DOI
Venue
2003
10.1007/978-3-540-39813-4_4
LECTURE NOTES IN ARTIFICIAL INTELLIGENCE
Keywords
Field
DocType
object-based calculi with side eects,program and system verification,. interactive theorem proving,logical foundations of programming,type system,interactive theorem proving,side effect,type theory,natural deduction
Discrete mathematics,Inductive type,Object-oriented programming,Natural deduction,Object type,Type theory,Pure mathematics,Algorithm,Metalanguage,Process calculus,Mathematics
Conference
Volume
ISSN
Citations 
2850
0302-9743
7
PageRank 
References 
Authors
0.46
17
3
Name
Order
Citations
PageRank
Alberto Ciaffaglione1589.97
Luigi Liquori239838.85
Marino Miculan350243.24