2026-08-17T04:51:22Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5501 2024-03-06T10:36:14Z ddc:004 open_access

On Isomorphism of Dependent Products in a Typed Logical Framework Soloviev, Sergei Isomorphism of types dependent product logical framework 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Sergei Soloviev 2015 Is Part Of LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2014.274 urn:nbn:de:0030-drops-55013 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.274 eng https://creativecommons.org/licenses/by/3.0/legalcode