Normalization by Evaluation for Martin-Löf Type Theory with One Universe
Authors:
Open Access
- 1 April 2007
- journal article
- Published by Elsevier in Electronic Notes in Theoretical Computer Science
- Vol. 173, 17-39
Abstract
No abstract availableKeywords
This publication has 7 references indexed in Scilit:
- Indexed induction–recursionThe Journal of Logic and Algebraic Programming, 2006
- Operational aspects of untyped Normalisation by EvaluationMathematical Structures in Computer Science, 2004
- Term rewriting for normalization by evaluationInformation and Computation, 2003
- A general formulation of simultaneous inductive-recursive definitions in type theoryThe Journal of Symbolic Logic, 2000
- Domains for denotational semantics1982
- An Intuitionistic Theory of Types: Predicative Part1975
- About Models for Intuitionistic Type Theories and the Notion of Definitional Equality1975