On Isomorphism of Dependent Products in a Typed Logical Framework

Soloviev, Sergei On Isomorphism of Dependent Products in a Typed Logical Framework. (2015) In: 20th International Conference on Types for Proofs and Programs (TYPES 2014), 12 May 2014 - 15 May 2014 (Paris, France).

Preview

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
402kB

Official URL: https://doi.org/10.4230/LIPIcs.TYPES.2014.274

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.

Item Type:	Conference or Workshop Item (Paper)
Additional Information:	LIPIcs : Leibniz International Proceedings in Informatics Volume 39 Année 2015 ISBN: 978-3-939897-88-0 ISSN: 1868-8969 http://drops.dagstuhl.de/opus/volltexte/2015/5501/
HAL Id:	hal-01913983
Audience (conference):	International conference proceedings
Uncontrolled Keywords:	Isomorphism of types - Dependent types - Deciding algorithm
Institution:	French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE) Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE) Other partners > National Research University of Information Technologies, Mechanics and Optics of St- Petersburg - ITMO (RUSSIA) Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE) Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE) Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:	Institut de Recherche en Informatique de Toulouse - IRIT (Toulouse, France) - ACADIE
Funders:	Government of the Russian Federation Grant 074-U01
Statistics:	download
Deposited On:	26 Sep 2018 14:12

Repository Staff Only: item control page