A formalization of System I with type Top in Agda
Agust\'in S\'ettimo, Cristian Sottile, Cecilia Manzino
TL;DR
This paper formalizes a variant of System I with the Top type in Agda, providing proofs of progress and strong normalization to enhance understanding of type isomorphisms in lambda calculus.
Contribution
It introduces a formalization of System I with the Top type in Agda, including proofs of progress and strong normalization, which was not previously established.
Findings
Formalization of System I with Top in Agda
Proofs of progress and strong normalization
Enhanced understanding of type isomorphisms
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Multi-Agent Systems and Negotiation