Weak normalization implies strong normalization in a class of non-dependent pure type systems (Q5958619): Difference between revisions

@@ Property / cites work @@
+The lambda calculus. Its syntax and semantics. Rev. ed.
+Normal rank
@@ Property / cites work @@
+Q4023825
@@ Property / cites work: Q4023825 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3024819
@@ Property / cites work: Q3024819 / rank @@
+Normal rank
@@ Property / cites work @@
+CPS translations and applications: The cube and beyond
+Normal rank
@@ Property / cites work @@
+Q4376043
@@ Property / cites work: Q4376043 / rank @@
+Normal rank
@@ Property / cites work @@
+Some Properties of Conversion
@@ Property / cites work: Some Properties of Conversion / rank @@
+Normal rank
@@ Property / cites work @@
+A-translation and looping combinators in pure type systems
+Normal rank
@@ Property / cites work @@
+Q4281472
@@ Property / cites work: Q4281472 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4939698
@@ Property / cites work: Q4939698 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3707989
@@ Property / cites work: Q3707989 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3918095
@@ Property / cites work: Q3918095 / rank @@
+Normal rank
@@ Property / cites work @@
+Call-by-name, call-by-value and the \(\lambda\)-calculus
+Normal rank
@@ Property / cites work @@
+Strong normalization from weak normalization in typed \(\lambda\)-calculi
+Normal rank
@@ Property / cites work @@
+On the adequacy of representing higher order intuitionistic logic as a pure type system
+Normal rank