LOIS: syntax and semantics. We present the semantics of an imperative programming language called LOIS (Looping Over Infinite Sets), 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, and SMT solvers are employed to evaluate programs.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Keshvardoost, Khadijeh; Klin, Bartek; Lasota, Sławomir; Ochremiak, Joanna; Toruńczyk, Szymon: Definable isomorphism problem (2019)
- Klin, Bartek; Łełyk, Mateusz: Scalar and vectorial (\mu)-calculus with atoms (2019)
- Kopczyński, Eryk; Toruńczyk, Szymon: LOIS: syntax and semantics (2017)
- Kozen, Dexter; Mamouras, Konstantinos; Silva, Alexandra: Completeness and incompleteness in nominal Kleene algebra (2017)
- Moerman, Joshua; Sammartino, Matteo; Silva, Alexandra; Klin, Bartek; Szynwelski, Michał: Learning nominal automata (2017)