文章基本信息

标题：On Isomorphism of Dependent Products in a Typed Logical Framework
本地全文：下载
作者：Sergei Soloviev
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：39
页码：274-287
DOI：10.4230/LIPIcs.TYPES.2014.274
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Isomorphism of types; dependent product; logical framework