LIPIcs.TYPES.2014.274.pdf
- Filesize: 0.48 MB
- 14 pages
Document
On Isomorphism of Dependent Products in a Typed Logical Framework
Author
-
Part of:
Volume:
20th International Conference on Types for Proofs and Programs (TYPES 2014)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Types for Proofs and Programs (TYPES) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2015-10-12
Cite AsGet BibTex
Sergei Soloviev. On Isomorphism of Dependent Products in a Typed Logical Framework. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 274-287, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.TYPES.2014.274
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.
Keywords
- Isomorphism of types
- dependent product
- logical framework
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads