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 <>
Submitted on : Saturday, June 13, 2015 - 3:38:33 PM
Last modification on : Saturday, February 8, 2020 - 12:10:04 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