External and internal syntax of the \(\lambda \)-calculus (Q968531): Difference between revisions

@@ Property / describes a project that uses @@
+Nominal Isabelle
@@ Property / describes a project that uses: Nominal Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / 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.jsc.2010.01.010
+Normal rank
@@ Property / OpenAlex ID @@
+W2033368611
@@ Property / OpenAlex ID: W2033368611 / rank @@
+Normal rank
@@ Property / cites work @@
+Engineering formal metatheory
@@ Property / cites work: Engineering formal metatheory / rank @@
+Normal rank
@@ Property / cites work @@
+The lambda calculus. Its syntax and semantics. Rev. ed.
+Normal rank
@@ Property / cites work @@
+Q5565097
@@ Property / cites work: Q5565097 / rank @@
+Normal rank
@@ Property / cites work @@
+Automating inversion of inductive predicates in Coq
+Normal rank
@@ Property / cites work @@
+Q5565113
@@ Property / cites work: Q5565113 / 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 @@
+Untersuchungen über das logische Schliessen. II
@@ Property / cites work: Untersuchungen über das logische Schliessen. II / rank @@
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+Recursive functions of symbolic expressions and their computation by machine, Part I
+Normal rank
@@ Property / cites work @@
+Q5601829
@@ Property / cites work: Q5601829 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4281480
@@ Property / cites work: Q4281480 / rank @@
+Normal rank
@@ Property / cites work @@
+Some lambda calculus and type theory formalized
@@ Property / cites work: Some lambda calculus and type theory formalized / rank @@
+Normal rank
@@ Property / cites work @@
+Q3999860
@@ Property / cites work: Q3999860 / 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 @@
+A canonical locally named representation of binding
+Normal rank
@@ Property / cites work @@
+Q5807658
@@ Property / cites work: Q5807658 / rank @@
+Normal rank
@@ Property / cites work @@
+Theory of symbolic expressions. I
@@ Property / cites work: Theory of symbolic expressions. I / rank @@
+Normal rank
@@ Property / cites work @@
+Theory of symbolic expressions. II
@@ Property / cites work: Theory of symbolic expressions. II / rank @@
+Normal rank
@@ Property / cites work @@
+Q4016562
@@ Property / cites work: Q4016562 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3044486
@@ Property / cites work: Q3044486 / rank @@
+Normal rank
@@ Property / cites work @@
+Substitution revisited
@@ Property / cites work: Substitution revisited / rank @@
+Normal rank
@@ Property / cites work @@
+Q5610986
@@ Property / cites work: Q5610986 / rank @@
+Normal rank
@@ Property / cites work @@
+Nominal techniques in Isabelle/HOL
@@ Property / cites work: Nominal techniques in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Barendregt’s Variable Convention in Rule Inductions
+Normal rank