2026-07-20T05:47:10Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5491 2024-03-12T12:02:05Z ddc:004 open_access

Objects and Subtyping in the Lambda-Pi-Calculus Modulo Cauderlier, Raphaël Dubois, Catherine object calculus encoding dependent type rewrite system We present a shallow embedding of the Object Calculus of Abadi and Cardelli in the lambda-Pi-calculus modulo, an extension of the lambda-Pi-calculus with rewriting. This embedding may be used as an example of translation of subtyping. We prove this embedding correct with respect to the operational semantics and the type system of the Object Calculus. We implemented a translation tool from the Object Calculus to Dedukti, a type-checker for the lambda-Pi-calculus modulo. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Raphaël Cauderlier and Catherine Dubois 2015 Is Part Of LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2014.47 urn:nbn:de:0030-drops-54919 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.47 eng https://creativecommons.org/licenses/by/3.0/legalcode