Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Thu 22 Aug 2019 15:20 - 15:50 at Aurora Borealis - Paper Session 3: SMT & Arity Chair(s): Eric Seidel

Satisfiability modulo theories (SMT) solvers give programmers a useful interface to solve challenging constraints at runtime. SMT solving has been used for a vast variety of different, useful applications, ranging from strengthening Haskell’s type system to verifying network protocols.

Unfortunately, interacting with SMT solvers directly from Haskell requires a great deal of manual effort. Data must be represented in and translated between two forms: that understood by Haskell, and that understood by the SMT solver. As such a translation is often done via printing and parsing text, any notion of type safety is lost. Furthermore, direct translations are rarely sufficient, as it typically takes many iterations on a design in order to get optimal – or even acceptable – performance from an SMT solver on large scale problems. This need for iteration complicates the translation issue: it is easy and frustrating to introduce a runtime bug.

To address these problems, we introduce a new library, G2Q. G2Q includes a quasiquoter that allows solving constraints written in Haskell itself, thus unifying data representation, ensuring correct typing, and simplifying iteration. We describe the API to our library and its backend, which is based on the G2 symbolic execution engine. Finally, we demonstrate the usability of G2Q via four example programs.

Thu 22 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:20 - 16:30
Paper Session 3: SMT & ArityHaskell at Aurora Borealis
Chair(s): Eric Seidel Bloomberg LP
Research paper
G2Q: Haskell Constraint Solving
William T. Hallahan Yale University, Anton Xue Yale University, Ruzica Piskac Yale University, USA
Making a Faster Curry with Extensional Types
Paul Downen University of Oregon, USA, Zachary Sullivan , Zena M. Ariola University of Oregon, USA, Simon Peyton Jones Microsoft, UK