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 • 30 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.
u/sclvin r/haskell • Mentions
On “Help with type-level naturals”
Not a full answer, since I can't conceptualize exactly the problem you're trying to solve, but I thought this talk from /u/kwef at Compose was a very nice overview of the travails of using type level nats currently, as well as some future work that may simplify things: link to this video