Zippy -- Generic White-Box Proof Search with Zippers
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866917968429973504 |
|---|---|
| author | Kappelmann, Kevin |
| author_facet | Kappelmann, Kevin |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_20413 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Zippy -- Generic White-Box Proof Search with Zippers Kappelmann, Kevin Logic in Computer Science Programming Languages 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. |
| title | Zippy -- Generic White-Box Proof Search with Zippers |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2503.20413 |