Wybe - A CE-embedded proof checker
Watch this session
Topic
While functional, type-safe programming is a good starting point for the correctness of a program, it’s still far away from a safe bet. Formal proofs still shine here. But proof systems still often suffer from being disconnected from the original code.
Wouldn’t it be great to have a proof checker embedded in F#?
Hold your type and enter Wybe, a proof checker embedded in F#‘s computation expressions.
Champion
Links
-
Date:
- Session link: https://us06web.zoom.us/j/81598883956?pwd=bZUbJkqlsWvZZaB6tsbC9QTtQ67AdB.1
- Passcode: proof