research
∙
10/25/2019
Embracing a mechanized formalization gap
If a code base is so big and complicated that complete mechanical verifi...
share
research
∙
06/09/2018
Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell)
Equational reasoning is one of the key features of pure functional langu...
research
∙
06/09/2018
Type variables in patterns
For many years, GHC has implemented an extension to Haskell that allows ...
research
∙
05/21/2018
The sufficiently smart compiler is a theorem prover
That the Haskell Compiler GHC is capable of proving non-trivial equaliti...
research
∙
03/19/2018
A promise checked is a promise kept: Inspection Testing
Occasionally, developers need to ensure that the compiler treats their c...
research
∙
03/19/2018
Beyond correct and fast: Inspection Testing
Occasionally, developers need to ensure that the compiler treats their c...
research
∙
03/19/2018
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code
Good tools can bring mechanical verification to programs written in main...
research
∙
11/25/2017
Total Haskell is Reasonable Coq
We would like to use the Coq proof assistant to mechanically verify prop...
research
∙
05/26/2017