Sebastián Urciuoli, Álvaro Tasistro, Nora Szasz. Strong Normalization for the Simply-Typed Lambda Calculus in Constructive Type Theory Using Agda. In Cláudia Nalon, editor, Proceedings of the 15th International Workshop on Logical and Semantic Frameworks with Applications, LSFA 2020, Online, September 15, 2019. Volume 351 of Electronic Notes in Theoretical Computer Science, pages 187-203, Elsevier, 2020. [doi]
Abstract is missing.