LOIS
Looping Over Infinite Sets

Eryk Kopczyński, Szymon Toruńczyk

Papers and technical documentation

LOIS: technical documentation. PDF (Feb 1, 2016)
Abstract: LOIS is a C++ library allowing iterating through certain infinite sets, in finite time. The resulting language has an intuitive semantics, corresponding to execution of infinitely many threads in parallel. This allows to merge the power of abstract mathematical constructions into imperative programming. Infinite sets are internally represented using first order formulas over some underlying logical structure. To effectively handle such sets, we use and implement SMT solvers for various first order theories. LOIS has applications in education, and in verification of infinite state systems. This is a technical documentation of LOIS, describing how to write programs using it.

LOIS: syntax and semantics. PDF (Oct 6, 2016) (accepted to POPL 2017)
Abstract: We present the semantics of a programming language called LOIS, which allows iterating through certain infinite sets, in finite time. Our semantics intuitively correspond to execution of infinitely many threads in parallel. This allows to merge the power of abstract mathematical constructions into imperative programming. Infinite sets are internally represented using first order formulas over some underlying logical structure.

LOIS: an application of SMT solvers. PDF (Apr 25, 2016) (accepted to SMT 2016)
Abstract: We present an implemented programming language called LOIS, which allows iterating through certain infinite sets, in finite time. We demonstrate how this language offers a new application of SMT solvers to theoretical verification, by showing that many known problems concerning infinite-state systems can easily be implemented using LOIS, which in turn invokes SMT solvers for an underlying theory. In many applications, ω-categorical theories with quantifier elimination are of particular interest. Our tests indicate that state-of-the art solvers perform poorly on such theories, as they are outperformed by orders of magnitude by a simple quantifier-elimination procedure.

Public repository

NEW (since Oct 13, 2016): the ongoing development of LOIS is hosted on GitHub here.

Prototypes

LOIS is released under the MIT license. It has been tested under: