The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective) (Q2841232): Difference between revisions

@@ 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 / cites work @@
+The lambda calculus. Its syntax and semantics. Rev. ed.
+Normal rank
@@ Property / cites work @@
+Proving Properties of Programs by Structural Induction
+Normal rank
@@ Property / cites work @@
+Q5565113
@@ Property / cites work: Q5565113 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4850465
@@ Property / cites work: Q4850465 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5667469
@@ Property / cites work: Q5667469 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3024905
@@ Property / cites work: Q3024905 / rank @@
+Normal rank
@@ Property / cites work @@
+Residual theory in λ-calculus: a formal development
+Normal rank
@@ Property / cites work @@
+Q2723897
@@ Property / cites work: Q2723897 / rank @@
+Normal rank
@@ Property / cites work @@
+Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
+Normal rank
@@ Property / cites work @@
+Q3918095
@@ Property / cites work: Q3918095 / 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 @@
+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 @@
+Substitution revisited
@@ Property / cites work: Substitution revisited / 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 @@
+Q2778886
@@ Property / cites work: Q2778886 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4518890
@@ Property / cites work: Q4518890 / rank @@
+Normal rank