31 citations · 31 across the 2 of their papers we have counts for
3 papers · 1 filter
Structural Operational Semantics for Control Flow Graph Machines
Dmitri Garbuzov, William Mansky, Christine Rizkallah +1
Compilers use control flow graph (CFG) representations of low-level programs because they are suited to program analysis and optimizations. However, formalizing the behavior and me…
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…
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…