Objects and subtyping in the λΠ-calculus modulo

Abstract : We present a shallow embedding of the Object Calculus of Abadi and Cardelli in the λΠ-calculus modulo, an extension of the λΠ-calculus in which conversion is considered modulo a rewrite system. This embedding may be used as an example of translation of subtyping, a feature also present in some proof assistants like Coq and PVS. This embedding is proved correct with respect to the operational semantics and the type system of the Object Calculus. It has been implemented as a translation tool from the Object Calculus to Dedukti, a type-checker for the λΠ-calculus modulo.
Type de document :
Pré-publication, Document de travail
2015
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01097444
Contributeur : Raphaël Cauderlier <>
Soumis le : samedi 13 juin 2015 - 15:38:33
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : mardi 25 avril 2017 - 07:47:08

Fichier

article_types.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01097444, version 2

Collections

Citation

Raphaël Cauderlier, Catherine Dubois. Objects and subtyping in the λΠ-calculus modulo. 2015. 〈hal-01097444v2〉

Partager

Métriques

Consultations de la notice

213

Téléchargements de fichiers

119