Normalization by Evaluation for Martin-Löf Type Theory with One Universe
DOI10.1016/J.ENTCS.2007.02.025zbMATH Open1316.68038OpenAlexW2148076999MaRDI QIDQ5262927FDOQ5262927
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
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
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)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Title not available (Why is that?)
- Operational aspects of untyped Normalisation by Evaluation
- A general formulation of simultaneous inductive-recursive definitions in type theory
- Foundations of Software Science and Computation Structures
- Title not available (Why is that?)
- Constructive mathematics and computer programming
- Term rewriting for normalization by evaluation.
- Title not available (Why is that?)
- Indexed induction-recursion
- Title not available (Why is that?)
Cited In (8)
- 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
- 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
- Title not available (Why is that?)
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)
