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.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-01097444
Contributor : Raphaël Cauderlier <>
Submitted on : Saturday, June 13, 2015 - 3:38:33 PM
Last modification on : Tuesday, January 15, 2019 - 2:54:12 PM
Long-term archiving on : Tuesday, April 25, 2017 - 7:47:08 AM

File

article_types.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01097444, version 2

Collections

Citation

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

Share

Metrics

Record views

246

Files downloads

194