31 citations · 47 across the 16 of their papers we have counts for
11 papers · 1 filter
Embracing a mechanized formalization gap
Antal Spector-Zabusky, Joachim Breitner, Yao Li +1
If a code base is so big and complicated that complete mechanical verification is intractable, can we still apply and benefit from verification methods? We show that by allowing a…
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…
Total Haskell is Reasonable Coq
Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah +1
We would like to use the Coq proof assistant to mechanically verify properties of Haskell programs. To that end, we present a tool, named hs-to-coq, that translates total Haskell p…
Lock-step simulation is child's play
Joachim Breitner, Chris Smith
Implementing multi-player networked games by broadcasting the player's input and letting each client calculate the game state - a scheme known as lock-step simulation - is an estab…
The Correctness of Launchbury's Natural Semantics for Lazy Evaluation
Joachim Breitner
In his seminal paper "A Natural Semantics for Lazy Evaluation", John Launchbury proves his semantics correct with respect to a denotational semantics. We machine-checked the proof…
dup -- Explicit un-sharing in Haskell
Joachim Breitner
We propose two operations to prevent sharing in Haskell that do not require modifying the data generating code, demonstrate their use and usefulness, and compare them to other appr…
Conditional Elimination through Code Duplication
Joachim Breitner
We propose an optimizing transformation which reduces program runtime at the expense of program size by eliminating conditional jumps.