Imperative Object-Based Calculi in Co-inductive Type Theories

Alberto Ciaffaglione 1, 2 Luigi Liquori 2, 3 Marino Miculan 1
2 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 : We discuss the formalization of Abadi and Cardelli's impς, a para-digmatic 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 impς, 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 impς can be applied to other imperative calculi and proof environments with similar features.
Type de document :
Communication dans un congrès
Logic for Programming, Artificial Intelligence, and Reasoning, 10th International Conference, LPAR 2003, Almaty, Kazakhstan, September 22-26, 2003. Proceedings, Sep 2003, Almaty, Kazakhstan. Springer Verlag, 2850, pp.59-77, 2003, Lecture Notes in Computer Science. 〈10.1007/978-3-540-39813-4_4〉
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01149867
Contributeur : Luigi Liquori <>
Soumis le : jeudi 7 mai 2015 - 17:16:20
Dernière modification le : samedi 27 janvier 2018 - 01:31:34
Document(s) archivé(s) le : mercredi 19 avril 2017 - 19:20:14

Fichier

2003-lpar-03.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Relations

Citation

Alberto Ciaffaglione, Luigi Liquori, Marino Miculan. Imperative Object-Based Calculi in Co-inductive Type Theories. Logic for Programming, Artificial Intelligence, and Reasoning, 10th International Conference, LPAR 2003, Almaty, Kazakhstan, September 22-26, 2003. Proceedings, Sep 2003, Almaty, Kazakhstan. Springer Verlag, 2850, pp.59-77, 2003, Lecture Notes in Computer Science. 〈10.1007/978-3-540-39813-4_4〉. 〈hal-01149867〉

Partager

Métriques

Consultations de la notice

253

Téléchargements de fichiers

44