A proof-theoretic approach to abstract interpretation
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866918523649916928 |
|---|---|
| author | D'Silva, Vijay Palmigiano, Alessandra Tzimoulis, Apostolos Urban, Caterina |
| author_facet | D'Silva, Vijay Palmigiano, Alessandra Tzimoulis, Apostolos Urban, Caterina |
| contents | This paper develops a proof-theoretic framework for abstract interpretation by systematically associating logical systems with finite abstractions. Building on earlier work on the internal logics of abstractions, we propose a general procedure for generating a logic whose Lindenbaum-Tarski algebra is isomorphic to a given abstract lattice. The approach identifies logical connectives preserved by the concretization map and derives corresponding proof rules and axioms. The paper establishes soundness and completeness results under suitable conditions, extends the framework to Cartesian products and multi-variable settings, and investigates the logical structure of non-Cartesian abstractions such as octagons. These observations suggest new connections between abstract interpretation, proof theory, and algebraic logic, providing a foundation for a systematic logical analysis of program abstractions. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_26591 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A proof-theoretic approach to abstract interpretation D'Silva, Vijay Palmigiano, Alessandra Tzimoulis, Apostolos Urban, Caterina Logic in Computer Science Logic This paper develops a proof-theoretic framework for abstract interpretation by systematically associating logical systems with finite abstractions. Building on earlier work on the internal logics of abstractions, we propose a general procedure for generating a logic whose Lindenbaum-Tarski algebra is isomorphic to a given abstract lattice. The approach identifies logical connectives preserved by the concretization map and derives corresponding proof rules and axioms. The paper establishes soundness and completeness results under suitable conditions, extends the framework to Cartesian products and multi-variable settings, and investigates the logical structure of non-Cartesian abstractions such as octagons. These observations suggest new connections between abstract interpretation, proof theory, and algebraic logic, providing a foundation for a systematic logical analysis of program abstractions. |
| title | A proof-theoretic approach to abstract interpretation |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2605.26591 |