DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2014.27

A Calculus of Constructions with Explicit Subtyping

Authors: Ali Assaf

Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)

Abstract

The calculus of constructions can be extended with an infinite hierarchy of universes and cumulative subtyping. Subtyping is usually left implicit in the typing rules. We present an alternative version of the calculus of constructions where subtyping is explicit. We avoid problems related to coercions and dependent types by using the Tarski style of universes and by adding equations to reflect equality.

Cite as

Ali Assaf. A Calculus of Constructions with Explicit Subtyping. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 27-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{assaf:LIPIcs.TYPES.2014.27,
  author =	{Assaf, Ali},
  title =	{{A Calculus of Constructions with Explicit Subtyping}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{27--46},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.27},
  URN =		{urn:nbn:de:0030-drops-54904},
  doi =		{10.4230/LIPIcs.TYPES.2014.27},
  annote =	{Keywords: type theory, calculus of constructions, universes, cumulativity, subtyping}
}

Document

DOI: 10.4230/LIPIcs.TLCA.2015.31

Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting

Authors: Ali Assaf

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

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.

Cite as

Ali Assaf. Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 31-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{assaf:LIPIcs.TLCA.2015.31,
  author =	{Assaf, Ali},
  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 =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.31},
  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}
}

Search Results

Documents authored by Assaf, Ali

A Calculus of Constructions with Explicit Subtyping

Abstract

Cite as

Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting

Abstract

Cite as

Thanks for your feedback!

Could not send message