Normalization by Evaluation for Martin-Löf Type Theory with One Universe (Q5262927): Difference between revisions

@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.entcs.2007.02.025
+Normal rank
@@ Property / OpenAlex ID @@
+W2148076999
@@ Property / OpenAlex ID: W2148076999 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3593498
@@ Property / cites work: Q3593498 / rank @@
+Normal rank
@@ Property / cites work @@
+Operational aspects of untyped Normalisation by Evaluation
+Normal rank
@@ Property / cites work @@
+The lambda calculus. Its syntax and semantics. Rev. ed.
+Normal rank
@@ Property / cites work @@
+Term rewriting for normalization by evaluation.
@@ Property / cites work: Term rewriting for normalization by evaluation. / rank @@
+Normal rank
@@ Property / cites work @@
+Q4247302
@@ Property / cites work: Q4247302 / rank @@
+Normal rank
@@ Property / cites work @@
+A general formulation of simultaneous inductive-recursive definitions in type theory
+Normal rank
@@ Property / cites work @@
+Indexed induction-recursion
@@ Property / cites work: Indexed induction-recursion / rank @@
+Normal rank
@@ Property / cites work @@
+Q4494371
@@ Property / cites work: Q4494371 / rank @@
+Normal rank
@@ Property / cites work @@
+Foundations of Software Science and Computation Structures
+Normal rank
@@ Property / cites work @@
+Constructive mathematics and computer programming
@@ Property / cites work: Constructive mathematics and computer programming / rank @@
+Normal rank
@@ Property / cites work @@
+Q3688389
@@ Property / cites work: Q3688389 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4247306
@@ Property / cites work: Q4247306 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3999860
@@ Property / cites work: Q3999860 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3959414
@@ Property / cites work: Q3959414 / rank @@
+Normal rank