Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda (Q2229159): Difference between revisions

@@ Property / cites work @@
+POPLMark reloaded: Mechanizing proofs by logical relations
+Normal rank
@@ Property / cites work @@
+Formal metatheory of the lambda calculus using Stoughton's substitution
+Normal rank
@@ Property / cites work @@
+Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory
+Normal rank
@@ Property / cites work @@
+Alpha-structural induction and recursion for the lambda calculus in constructive type theory
+Normal rank
@@ Property / cites work @@
+Q5565113
@@ Property / cites work: Q5565113 / rank @@
+Normal rank
@@ Property / cites work @@
+Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
+Normal rank
@@ Property / cites work @@
+Substitution revisited
@@ Property / cites work: Substitution revisited / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank