Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts

Alberto Ciaffaglione 1, 2 Luigi Liquori 3, 1 Marino Miculan 2
1 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 illustrate a methodology for formalizing and reasoning about Abadi and Cardelli's object-based calculi, in (co)inductive type theory, such as the Calculus of (Co)Inductive Constructions, by taking advantage of Natural Deduction Semantics and coinduction in combination with weak Higher-Order Abstract Syntax and the Theory of Contexts. Our methodology allows to implement smoothly the calculi in the target metalanguage; moreover, it suggests novel presentations of the calculi themselves. In detail, we present a compact formalization of the syntax and semantics for the functional and the imperative variants of the ς-calculus. Our approach simplifies the proof of Subject Reduction theorems, which are proved formally in the proof assistant Coq with a relatively small overhead.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2007, Journal of Automated Reasoning, 39 (1), pp.1-47. 〈Kluwer Academic Publishers〉. 〈10.1007/s10817-006-9061-y〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01148347
Contributeur : Luigi Liquori <>
Soumis le : mercredi 13 mai 2015 - 13:16:32
Dernière modification le : samedi 27 janvier 2018 - 01:30:41
Document(s) archivé(s) le : mercredi 19 avril 2017 - 14:42:26

Fichier

2007-jar-07.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Alberto Ciaffaglione, Luigi Liquori, Marino Miculan. Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts. Journal of Automated Reasoning, Springer Verlag, 2007, Journal of Automated Reasoning, 39 (1), pp.1-47. 〈Kluwer Academic Publishers〉. 〈10.1007/s10817-006-9061-y〉. 〈hal-01148347〉

Partager

Métriques

Consultations de la notice

377

Téléchargements de fichiers

49