A formalization of System I with type Top in Agda
Logic in Computer Science
2026-03-26 v1 Programming Languages
Abstract
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.
Cite
@article{arxiv.2603.23652,
title = {A formalization of System I with type Top in Agda},
author = {Agustín Séttimo and Cristian Sottile and Cecilia Manzino},
journal= {arXiv preprint arXiv:2603.23652},
year = {2026}
}