Programming with atoms (tool demonstration)

A demo presentation of two simple programming languages designed to manipulate infinite, but first-order definable structures, such as the set of all intervals with rational endpoints. One of the languages is implemented as a C++ library, LOIS, by Eryk Kopczyński and Szymon Toruńczyk, while the other as a Haskell module, NLambda, by Bartek Klin and Michał Szynwelski. Internally, infinite sets are represented by logical formulas that define them, whereas an external SMT solver is invoked to check their basic properties.

Authors

• Eryk Kopczyński
• Michał Szynwelski

Keywords

No keywords are indexed for this paper.