Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations (Q853738): Difference between revisions

@@ Property / DOI @@
-.1007/s10990-006-8745-7
@@ Property / DOI: 10.1007/s10990-006-8745-7 / rank @@
-Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10990-006-8745-7
+Normal rank
@@ Property / OpenAlex ID @@
+W1981019433
@@ Property / OpenAlex ID: W1981019433 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4484329
@@ Property / cites work: Q4484329 / rank @@
+Normal rank
@@ Property / cites work @@
+The lambda calculus. Its syntax and semantics. Rev. ed.
+Normal rank
@@ Property / cites work @@
+Q2703747
@@ Property / cites work: Q2703747 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4843179
@@ Property / cites work: Q4843179 / 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 @@
+Residual theory in λ-calculus: a formal development
+Normal rank
@@ Property / cites work @@
+Theorem proving in higher order logics. 18th international conference, TPHOLs 2005, Oxford, UK, August 22--25, 2005. Proceedings.
+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 @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Defining functions on equivalence classes
@@ Property / cites work: Defining functions on equivalence classes / rank @@
+Normal rank
@@ Property / cites work @@
+Nominal logic, a first order theory of names and binding
+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 @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
+Normal rank
@@ Property / cites work @@
+Q2778886
@@ Property / cites work: Q2778886 / rank @@
+Normal rank
@@ Property / cites work @@
+The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective)
+Normal rank
@@ Property / DOI @@
+.1007/S10990-006-8745-7
@@ Property / DOI: 10.1007/S10990-006-8745-7 / rank @@
+Normal rank