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

@@ Property / DOI @@
-.1016/j.entcs.2016.06.008
@@ Property / DOI: 10.1016/j.entcs.2016.06.008 / rank @@
-Normal rank
@@ Property / Wikidata QID @@
+Q113317681
@@ Property / Wikidata QID: Q113317681 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Nominal Isabelle
@@ Property / describes a project that uses: Nominal Isabelle / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.entcs.2016.06.008
+Normal rank
@@ Property / OpenAlex ID @@
+W2461095491
@@ Property / OpenAlex ID: W2461095491 / rank @@
+Normal rank
@@ 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
@@ Property / DOI @@
+.1016/J.ENTCS.2016.06.008
@@ Property / DOI: 10.1016/J.ENTCS.2016.06.008 / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:1744410