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. (2020). Big Step Normalisation for Type Theory. LIPIcs, 2020, Article 4. https://doi.org/10.4230/LIPIcs.TYPES.2019.4

• Journal Article Type: Conference Paper
• Conference Name: 25th International Conference on Types for Proofs and Programs (TYPES 2019)
• Conference Location: Oslo, Norway
• 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
• 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