Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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 metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Raphaël Cauderlier Connect in order to contact the contributor
Submitted on : Saturday, June 13, 2015 - 3:38:33 PM
Last modification on : Monday, February 21, 2022 - 3:38:12 PM
Long-term archiving on: : Tuesday, April 25, 2017 - 7:47:08 AM


Files produced by the author(s)


  • HAL Id : hal-01097444, version 2



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



Record views


Files downloads