Objects and subtyping in the λΠ-calculus moduloReportar como inadecuado

Objects and subtyping in the λΠ-calculus modulo - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique Inria Paris-Rocquencourt 2 CNAM Paris - Conservatoire National des Arts et Métiers - Paris 3 ENSIIE - Ecole Nationale Supérieure d-Informatique pour l-Industrie et l-Entreprise

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.

Autor: Raphaël Cauderlier - Catherine Dubois -

Fuente: https://hal.archives-ouvertes.fr/


Documentos relacionados