带有类型Top的System I的形式化
A formalization of System I with type Top in Agda
Universidad Nacional de Rosario（罗萨里奥国立大学）；Universidad Nacional de Quilmes（基尔梅斯国立大学）；Instituto de Investigación en Ciencias de la Computación (ICC), CONICET / Universidad de Buenos Aires（计算机科学研究所（ICC），阿根廷国家科学研究委员会 / 布宜诺斯艾利斯大学）
AI总结：
本文提出带有类型Top的System I变种，并用Agda形式化了该算术，包含进度和强归约的证明。
摘要：
System I是一种最近引入的简单类型lambda演算，其中等价类型被视为相等。本文提出System I的一个变种，包含类型Top，并在Agda中完整形式化了该算术，包括进度和强归约的证明。
英文摘要：
System I is a recently introduced simply-typed lambda calculus with pairs where isomorphic types are considered equal. In this work we propose a variant of System I with the type Top, and present a complete formalization of this calculus in Agda, which includes the proofs of progress and strong normalization.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
