Strong Normalization for the Simply-Typed Lambda Calculus in Constructive Type Theory Using Agda. - Sebastián Urciuoli; Álvaro Tasistro; Nora Szasz (LSFA, 2020)

A Formal Proof of the Strong Normalization Theorem for System T in Agda. - Sebastián Urciuoli (LSFA, 2022)