SMT Solving for Functional Programming over Infinite Structures
Bartek Klin (University of Warsaw), Micha{\l} Szynwelski (University, of Warsaw)
TL;DR
This paper introduces a functional programming language that manipulates infinite structures using SMT solving, enabling reasoning about complex infinite sets within a Haskell implementation.
Contribution
It presents a novel language design that integrates SMT solving for infinite structures, expanding the capabilities of functional programming languages.
Findings
Successfully manipulates infinite structures using SMT
Implemented as a Haskell module for practical use
Enables reasoning about properties of infinite sets
Abstract
We develop a simple functional programming language aimed at manipulating infinite, but first-order definable structures, such as the countably infinite clique graph or the set of all intervals with rational endpoints. Internally, such sets are represented by logical formulas that define them, and an external satisfiability modulo theories (SMT) solver is regularly run by the interpreter to check their basic properties. The language is implemented as a Haskell module.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.