Big Step Normalisation for Type Theory

Altenkirch, Thorsten; Geniet, Colin

Abstract

Big step normalisation is a normalisation method for typed lambda-calculi which relies on a purely syntactic recursive evaluator. Termination of that evaluator is proven using a predicate called strong computability, similar to the techniques used to prove strong normalisation of β-reduction for typed lambda-calculi. We generalise big step normalisation to a minimalist dependent type theory. Compared to previous presentations of big step normalisation for e.g. the simply-typed lambda-calculus, we use a quotiented syntax of type theory, which crucially reduces the syntactic complexity introduced by dependent types. Most of the proof has been formalised using Agda.

Citation

Altenkirch, T., & Geniet, C. Big Step Normalisation for Type Theory. Presented at 25th International Conference on Types for Proofs and Programs (TYPES 2019), Oslo, Norway

• Presentation Conference Type: Conference Paper (published)
• Conference Name: 25th International Conference on Types for Proofs and Programs (TYPES 2019)
• Acceptance Date: Mar 26, 2020
• Online Publication Date: Sep 24, 2020
• Publication Date: Sep 24, 2020
• Deposit Date: May 20, 2020
• Publicly Available Date: May 27, 2020
• Journal: LIPIcs
• Electronic ISSN: 1868-8969
• Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
• Peer Reviewed: Peer Reviewed
• Volume: 2020
• Article Number: 4
• Series Title: Leibniz International Proceedings in Informatics
• DOI: https://doi.org/10.4230/LIPIcs.TYPES.2019.4
• Keywords: Normalisation; big step normalisation; type theory; dependent types; Agda
• Public URL: https://nottingham-repository.worktribe.com/output/4475693
• Publisher URL: https://drops.dagstuhl.de/opus/volltexte/2020/13068/
• Related Public URLs: https://cas.oslo.no/types2019/; ; https://www.dagstuhl.de/en/publications/lipics