SMT solving for functional programming over infinite structures

MaRDI QIDQ5013828zbMATH OpenFDO

Authors Bartek Klin, Michał Szynwelski

Publication date 2 December 2021

Full work available at URL https://arxiv.org/abs/1604.01185, http://eptcs.web.cse.unsw.edu.au/paper.cgi?MSFP2016.3

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Scala to the Power of Z3: Integrating SMT and Programming
• LOIS: syntax and semantics
• CoCaml: functional programming with regular coinductive types
• scientific article; zbMATH DE number 1487843
• scientific article; zbMATH DE number 4009812

Cites work

• Algebraic properties of valued constraint satisfaction problem
• Applying Linear Quantifier Elimination
• Automata theory in nominal sets
• Handbook of constraint programming.
• scientific article; zbMATH DE number 3976287 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 53151 (Why is no real title available?)
• Linear Quantifier Elimination
• Locally finite constraint satisfaction problems
• Nominal sets. Names and symmetry in computer science
• Parallel reductions in \(\lambda\)-calculus
• Towards nominal computation
• Universal partial order represented by means of oriented trees and other simple graphs

Cited in

(10)

• Completeness and incompleteness in nominal Kleene algebra
• scientific article; zbMATH DE number 7136664 (Why is no real title available?)
• Residuality and learning for nondeterministic nominal automata
• scientific article; zbMATH DE number 7559500 (Why is no real title available?)
• scientific article; zbMATH DE number 7147443 (Why is no real title available?)
• LOIS: syntax and semantics
• Infinite structures in Scratchpad II
• Fast computations on ordered nominal sets
• On-the-fly bisimilarity checking for fresh-register automata
• Karp's NP-complete problems over first-order definable structures

Describes a project that uses

Uses Software

• Haskell
• z3
• NLambda
• SETL

This page was built for publication: SMT solving for functional programming over infinite structures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5013828)