A Formal Proof of the Strong Normalization Theorem for System T in Agda (Q6118750): Difference between revisions

@@ Property / cites work @@
+Normalization for the Simply-Typed Lambda-Calculus in Twelf
+Normal rank
@@ Property / cites work @@
+POPLMark reloaded: Mechanizing proofs by logical relations
+Normal rank
@@ Property / cites work @@
+Q3728878
@@ Property / cites work: Q3728878 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5667469
@@ Property / cites work: Q5667469 / rank @@
+Normal rank
@@ Property / cites work @@
+The locally nameless representation
@@ Property / cites work: The locally nameless representation / rank @@
+Normal rank
@@ Property / cites work @@
+Formal metatheory of the lambda calculus using Stoughton's substitution
+Normal rank
@@ Property / cites work @@
+Q2871864
@@ Property / cites work: Q2871864 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3994895
@@ Property / cites work: Q3994895 / rank @@
+Normal rank
@@ Property / cites work @@
+ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
+Normal rank
@@ Property / cites work @@
+Q3522248
@@ Property / cites work: Q3522248 / 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 @@
+Intensional interpretations of functionals of finite type I
+Normal rank
@@ Property / cites work @@
+Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus
+Normal rank
@@ Property / cites work @@
+Nominal unification
@@ Property / cites work: Nominal unification / rank @@
+Normal rank
@@ Property / cites work @@
+Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda
+Normal rank