Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A formalization of System I with type Top in Agda

Agustín Séttimo, Cristian Sottile, Cecilia Manzino

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.

A formalization of System I with type Top in Agda

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.
Paper Structure (16 sections, 14 equations, 2 figures, 3 tables)

This paper contains 16 sections, 14 equations, 2 figures, 3 tables.

Table of Contents

  1. Introduction
  2. STLC modulo isomorphisms
  3. Adding Top and transitioning to explicitness
  4. Formalization
  5. Types, contexts and variables
  6. Terms
  7. Substitutions and reduction
  8. Type isomorphisms
  9. Equivalence of terms
  10. Progress
  11. Strong normalization
  12. The adequacy function
  13. Evaluation
  14. Example
  15. Conclusions
  16. ...and 1 more sections

Figures (2)

  • Figure 1: Typing rules
  • Figure 2: Typing derivation of $\Omega$