scientific article; zbMATH DE number 7756109

DOI10.4230/lipics.types.2019.4MaRDI QIDQ6079230

Colin Geniet, Thorsten Altenkirch

Publication date: 27 October 2023

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

type theorynormalisationdependent typesAgdabig step normalisation

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Call-by-push-value: Decomposing call-by-value and call-by-name
• Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
• Quotient inductive-inductive types
• Type Theory Should Eat Itself
• Type theory in type theory using quotient inductive types
• Big-step normalisation
• A coherence theorem for Martin-Löf's type theory
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Internal type theory
• Categorical reconstruction of a reduction free normalization proof
• Normalisation by Evaluation for Dependent Types.
• Intensional interpretations of functionals of finite type I

This page was built for publication: