2026-07-23T22:21:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23353 2025-06-25T13:23:37Z ddc:004 open_access

The Algebra of Patterns - Rocq Proofs (Artifact) Binder, David Ermantraut, Lean functional programming pattern matching algebraic data types equational reasoning This artifact provides Rocq proofs for all the theorems of section 3 of the paper The Algebra of Patterns. Concretely, these are theorems 3, 4, 7, 8, 9, 10, 11, 12, 13 and 15. Schloss Dagstuhl – Leibniz-Zentrum für Informatik David Binder and Lean Ermantraut 2025 Is Part Of DARTS, Volume 11, Issue 2, Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025) Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DARTS.11.2.10 urn:nbn:de:0030-drops-233531 https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.10 eng https://creativecommons.org/licenses/by/4.0/legalcode