License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2014.47
URN: urn:nbn:de:0030-drops-54919
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5491/
Go to the corresponding LIPIcs Volume Portal

Cauderlier, Raphaël ; Dubois, Catherine

Objects and Subtyping in the Lambda-Pi-Calculus Modulo

pdf-format:
5.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{cauderlier_et_al:LIPIcs:2015:5491,
  author =	{Rapha{\"e}l Cauderlier and Catherine Dubois},
  title =	{{Objects and Subtyping in the Lambda-Pi-Calculus Modulo}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{47--71},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Hugo Herbelin and Pierre Letouzey and Matthieu Sozeau},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5491},
  URN =		{urn:nbn:de:0030-drops-54919},
  doi =		{10.4230/LIPIcs.TYPES.2014.47},
  annote =	{Keywords: object, calculus, encoding, dependent type, rewrite system}
}

Keywords: object, calculus, encoding, dependent type, rewrite system
Collection: 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Issue Date: 2015
Date of publication: 12.10.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI