Reasoning on an imperative object-based calculus in Higher Order Abstract Syntax

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 illustrate the benefits of using Natural Deduction in combination with weak Higher-Order Abstract Syntax for formalizing an object-based calculus with objects, cloning, method-update, types with subtyping, and side-effects, in inductive type theories such as the Calculus of Inductive Constructions. This setting suggests a clean and compact formalization of the syntax and semantics of the calculus, with an efficient management of method closures. Using our formalization and the Theory of Contexts, we can prove formally the Subject Reduction Theorem in the proof assistant Coq, with a relatively small overhead.
Type de document :
Communication dans un congrès
MERLIN '03. Proceedings of the 2003 ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, Aug 2003, Uppsala, Sweden. ACM SIGPLAN, pp.1-10, 〈10.1145/976571.976574〉
Liste complète des métadonnées

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

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

Fichier

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

Identifiants

Collections

Citation

Alberto Ciaffaglione, Luigi Liquori, Marino Miculan. Reasoning on an imperative object-based calculus in Higher Order Abstract Syntax. MERLIN '03. Proceedings of the 2003 ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, Aug 2003, Uppsala, Sweden. ACM SIGPLAN, pp.1-10, 〈10.1145/976571.976574〉. 〈hal-01149845〉

Partager

Métriques

Consultations de la notice

404

Téléchargements de fichiers

43