u/mightybytein r/haskell • Recommends
Compose Conference: Augmenting GHC's type system with the power of the Z3 theorem prover
0:00 / 0:00
#haskell#z3#type-checkerplugins
'There and Back Again' and What Happened After
Compose Conference
2.9K subscribers • 28 videos on Hallway
- Recommended by 1 person: 1 in engineering communities.
- Presented by Kenneth Foner
Advanced. Deep dive for people who know the field.
1.4K views10 years ago1 recommendation
Programming languagesComputer scienceHaskellFormal methods and verificationAlgorithms
Kenneth Foner explains how to reconstruct the 'There and Back Again' pattern in modern Haskell using GHC type-checker plugins and the Z3 theorem prover.
Kenneth Foner C◦mp◦se :: Conference composeconference.org/ February 4, 2016 Reconstructing ‘There and Back Again’ in modern Haskell requires us to elucidate some subtle arithmetic invariants of the pattern, both to ourselves and to the type system. To automatically verify the tricky arithmetic latent in the pearl, we use GHC’s brand new type-checker plugin interface to augment our type system with the power of the Z3 theorem prover.Why it's here
1 person recommends thisWhat people say. Recommended for its deep dive into augmenting Haskell's type system with Z3.