Proof Pearl: Abella Formalization of λ-Calculus Cube Property (Q4916060): Difference between revisions

@@ Property / describes a project that uses @@
+Abella
@@ Property / describes a project that uses: Abella / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Beluga
@@ Property / describes a project that uses: Beluga / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Twelf
@@ Property / describes a project that uses: Twelf / 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.1007/978-3-642-35308-6_15
+Normal rank
@@ Property / OpenAlex ID @@
+W2110359479
@@ Property / OpenAlex ID: W2110359479 / rank @@
+Normal rank
@@ Property / cites work @@
+On the Expressivity of Minimal Generic Quantification
+Normal rank
@@ Property / cites work @@
+The lambda calculus. Its syntax and semantics. Rev. ed.
+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 @@
+Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
+Normal rank
@@ Property / cites work @@
+The Abella Interactive Theorem Prover (System Description)
+Normal rank
@@ Property / cites work @@
+Reasoning in Abella about Structural Operational Semantics Specifications
+Normal rank
@@ Property / cites work @@
+Nominal abstraction
@@ Property / cites work: Nominal abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+A two-level logic approach to reasoning about computations
+Normal rank
@@ Property / cites work @@
+Relating conflict-free stable transition and event models via redex families
+Normal rank
@@ Property / cites work @@
+Residual theory in λ-calculus: a formal development
+Normal rank
@@ Property / cites work @@
+Q4281480
@@ Property / cites work: Q4281480 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4808736
@@ Property / cites work: Q4808736 / rank @@
+Normal rank
@@ Property / cites work @@
+A proof theory for generic judgments
@@ Property / cites work: A proof theory for generic judgments / rank @@
+Normal rank
@@ Property / cites work @@
+Proof search specifications of bisimulation and modal logics for the π-calculus
+Normal rank
@@ Property / cites work @@
+More Church-Rosser proofs (in Isabelle/HOL)
@@ Property / cites work: More Church-Rosser proofs (in Isabelle/HOL) / rank @@
+Normal rank
@@ Property / cites work @@
+A mechanical proof of the Church-Rosser theorem
@@ Property / cites work: A mechanical proof of the Church-Rosser theorem / rank @@
+Normal rank
@@ Property / cites work @@
+Parallel reductions in \(\lambda\)-calculus
@@ Property / cites work: Parallel reductions in \(\lambda\)-calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Q4799892
@@ Property / cites work: Q4799892 / rank @@
+Normal rank