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.
Topics & Concepts
ExtensionalityType theoryAxiomConstructive set theoryType (biology)Interpretation (philosophy)MathematicsConstructiveExtension (predicate logic)Pure mathematicsAlgebra over a fieldDiscrete mathematicsAxiom of choiceSet theorySet (abstract data type)Computer scienceProgramming languageProcess (computing)BiologyEcologyGeometryLogic, programming, and type systemsAdvanced Database Systems and QueriesConstraint Satisfaction and Optimization