Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Soloviev, Sergei http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-55013
URL:

On Isomorphism of Dependent Products in a Typed Logical Framework

pdf-format:


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
Seminar: 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Issue date: 2015
Date of publication: 2015


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