Monadic Warsaw #25

Hey everyone!

A new Monadic Warsaw is upon us. As always, if you want to add your talk to the pool, just contact the organizers.

Maciej Bielecki: Certified TodoMVC - writing web apps in Coq
Automated theorem provers are used to ensure correctness of critical applications like filesystems or compilers all over the world. Yet in the web development world, they remain an obscure curiosity. Can this situation be improved? In this talk we'll explore how can a web app be written in the Coq theorem prover, and how to prove facts about its behavior.