Normalization by Evaluation for Martin-Löf Type Theory with One Universe

DOI10.1016/J.ENTCS.2007.02.025MaRDI QIDQ5262927zbMATH OpenOpenAlexFDO

Authors Andreas Abel, Klaus Aehlig, Peter Dybjer

Publication date 10 July 2015

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2007.02.025

zbMATH Keywords

dependent typesnormalization by evaluationtype theoryuniversedomain semantics

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40) Semantics in the theory of computing (68Q55)

Recommendations

• Some normalization properties of Martin-Löf's type theory, and applications
• Normalization by evaluation for modal dependent type theory
• The simple type theory of normalisation by evaluation
• Normalisation by evaluation for type theory, in type theory
• Extending Martin-Löf type theory by one Mahlo-universe
• A type-checking algorithm for Martin-Löf type theory with subtyping based on normalisation by evaluation
• Normalization by Evaluation for Typed Weak lambda-Reduction
• Strong normalization in type systems: A model theoretical approach
• Foundations of Software Science and Computation Structures
• Normalising the associative law: An experiment with Martin-Löf's type theory

Cites work

• scientific article; zbMATH DE number 5173450 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 3780545 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 1302058 (Why is no real title available?)
• scientific article; zbMATH DE number 1302061 (Why is no real title available?)
• scientific article; zbMATH DE number 1487847 (Why is no real title available?)
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Constructive mathematics and computer programming
• Foundations of Software Science and Computation Structures
• Indexed induction-recursion
• Operational aspects of untyped Normalisation by Evaluation
• Term rewriting for normalization by evaluation.
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(9)

• scientific article; zbMATH DE number 65534 (Why is no real title available?)
• Extending Martin-Löf type theory by one Mahlo-universe
• Towards normalization by evaluation for the \(\beta \eta \)-calculus of constructions
• Normalization by Evaluation for Typed Weak lambda-Reduction
• A type-checking algorithm for Martin-Löf type theory with subtyping based on normalisation by evaluation
• Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
• Normalization by evaluation for modal dependent type theory
• Possible forms of evaluation or reduction in Martin-Löf type theory
• A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance

This page was built for publication: Normalization by Evaluation for Martin-Löf Type Theory with One Universe

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5262927)