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.TLCA.2015.31
URN: urn:nbn:de:0030-drops-51535
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5153/
Go to the corresponding LIPIcs Volume Portal

Assaf, Ali

Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting

pdf-format:
8.pdf (0.4 MB)

Abstract

The lambda Pi calculus can be extended with rewrite rules to embed
any functional pure type system. In this paper, we show that the embedding is conservative by proving a relative form of normalization, thus justifying the use of the lambda Pi calculus modulo rewriting as a logical framework for logics based on pure type systems. This result was previously only proved under the condition that the target system is normalizing. Our approach does not depend on this condition and therefore also works when the source system is not normalizing.

BibTeX - Entry

@InProceedings{assaf:LIPIcs:2015:5153,
  author =	{Ali Assaf},
  title =	{{Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{31--44},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Thorsten Altenkirch},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5153},
  URN =		{urn:nbn:de:0030-drops-51535},
  doi =		{10.4230/LIPIcs.TLCA.2015.31},
  annote =	{Keywords: lambda Pi calculus modulo rewriting, pure type systems, logical framework, normalization, conservativit}
}

Keywords: lambda Pi calculus modulo rewriting, pure type systems, logical framework, normalization, conservativit
Collection: 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Issue Date: 2015
Date of publication: 15.06.2015

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