2025/03/26 by Kevin Kappelmann, Kappelmann, Kevin
Computer Science · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2503.20413
openalex publication_date 2025/03/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We present a framework for tree-based proof search, called Zippy. Unlike existing proof search tools, Zippy is largely independent of concrete search tree representations, search-algorithms, states and effects. It is designed to create analysable and navigable proof searches that are open to customisation and extensions by users. Zippy is founded on concepts from functional programming theory, particularly zippers, arrows, monads, and lenses. We implemented the framework in Isabelle's metaprogramming language Isabelle/ML.