31 citations · 47 across the 16 of their papers we have counts for
5 papers · 2 filters
Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell)
Niki Vazou, Joachim Breitner, Will Kunkel +2
Equational reasoning is one of the key features of pure functional languages such as Haskell. To date, however, such reasoning always took place externally to Haskell, either manua…
Type variables in patterns
Richard A. Eisenberg, Joachim Breitner, Simon Peyton Jones
For many years, GHC has implemented an extension to Haskell that allows type variables to be bound in type signatures and patterns, and to scope over terms. This extension was neve…
The sufficiently smart compiler is a theorem prover
Joachim Breitner
That the Haskell Compiler GHC is capable of proving non-trivial equalities between Haskell code, by virtue of its aggressive optimizer, in particular the term rewriting engine in t…
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code
Joachim Breitner, Antal Spector-Zabusky, Yao Li +3
Good tools can bring mechanical verification to programs written in mainstream functional languages. We use hs-to-coq to translate significant portions of Haskell's containers libr…
A promise checked is a promise kept: Inspection Testing
Joachim Breitner
Occasionally, developers need to ensure that the compiler treats their code in a specific way that is only visible by inspecting intermediate or final compilation artifacts. This i…