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

Soloviev, Sergei

On Isomorphism of Dependent Products in a Typed Logical Framework

pdf-format:
15.pdf (0.5 MB)

Abstract

A complete decision procedure for isomorphism of kinds that contain only dependent product, constant Type and variables is obtained. All proofs are done using Z. Luo's logical framework. They can be easily transferred to a large class of type theories with dependent product.

BibTeX - Entry

@InProceedings{soloviev:LIPIcs:2015:5501,
  author =	{Sergei Soloviev},
  title =	{{On Isomorphism of Dependent Products in a Typed Logical Framework}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{274--287},
  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/5501},
  URN =		{urn:nbn:de:0030-drops-55013},
  doi =		{10.4230/LIPIcs.TYPES.2014.274},
  annote =	{Keywords: Isomorphism of types, dependent product, logical framework}
}

Keywords: Isomorphism of types, dependent product, logical framework
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