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

DOI10.1016/j.entcs.2007.02.025zbMath1316.68038OpenAlexW2148076999MaRDI QIDQ5262927

Peter Dybjer, Klaus Aehlig, Andreas Abel

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

universetype theorydependent typesnormalization by evaluationdomain semantics

Mathematics Subject Classification ID

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

Related Items

A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance ⋮ Normalization by Evaluation for Typed Weak lambda-Reduction

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• Term rewriting for normalization by evaluation.
• Indexed induction-recursion
• Constructive mathematics and computer programming
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Operational aspects of untyped Normalisation by Evaluation
• Foundations of Software Science and Computation Structures
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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