Alpha-structural induction and recursion for the lambda calculus in constructive type theory (Q1744410): Difference between revisions

@@ Property / cites work @@
+Q2871861
@@ Property / cites work: Q2871861 / rank @@
+Normal rank
@@ Property / cites work @@
+Engineering formal metatheory
@@ Property / cites work: Engineering formal metatheory / rank @@
+Normal rank
@@ Property / cites work @@
+The locally nameless representation
@@ Property / cites work: The locally nameless representation / rank @@
+Normal rank
@@ Property / cites work @@
+Q5667469
@@ Property / cites work: Q5667469 / rank @@
+Normal rank
@@ Property / cites work @@
+A new approach to abstract syntax with variable binding
+Normal rank
@@ Property / cites work @@
+Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus
+Normal rank
@@ Property / cites work @@
+Q3688389
@@ Property / cites work: Q3688389 / rank @@
+Normal rank
@@ Property / cites work @@
+Viewing \({\lambda}\)-terms through maps
@@ Property / cites work: Viewing \({\lambda}\)-terms through maps / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Nominal logic, a first order theory of names and binding
+Normal rank
@@ Property / cites work @@
+Alpha-structural recursion and induction
@@ Property / cites work: Alpha-structural recursion and induction / rank @@
+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