2026-07-31T14:23:53Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13068 2024-03-06T10:51:12Z ddc:004 open_access

Big Step Normalisation for Type Theory Altenkirch, Thorsten Geniet, Colin Normalisation big step normalisation type theory dependent types Agda 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Thorsten Altenkirch and Colin Geniet 2020 Is Part Of LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2019.4 urn:nbn:de:0030-drops-130682 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.4 eng https://creativecommons.org/licenses/by/3.0/legalcode