Superhero monads, and more equational reasoning

This month, Katie returns to give us a sneak preview of the talk she has been invited to give at Codemania NZ, and Dave Laing gives his first talk at BFPG, going deeper into laws and equational reasoning in Haskell and Coq.

Space might be limited, so get your RSVP in now!

Monads to the Rescue

Katie Miller

Monads are sometimes spoken of like villains with an evil plan to turn programmers' brains to mush. This talk will reveal that monads are actually superheroes and show how they can save your Hello World and beyond from great perils. The presentation will cover some of the basics of the functional programming paradigm before focusing on a select squad of monadic heroes. There will be examples shown in Java 8 as well as Haskell.

Katie Miller is a Java developer at Red Hat and a BFPG organiser. The former journalist can write copy, code, and copy that looks like code, churning out shorthand notes at up to 120 words per minute. Producing code that reads like copy is among her ongoing endeavours.

Laws and Equations and Coq! Oh, My!

David Laing

Haskell isn't able to determine whether Monoid and Functor instances satisfy the appropriate laws, but that doesn't mean it can't be done. This talk will walk step by step through the process of using equational reasoning to prove that the Monoid and Functor laws hold for their list instances. We'll then look at how to verify these laws using Coq, and at the Haskell code extracted from the Coq proof.

Dave wrote code for a few years, did a PhD in theoretical computer science, then continued to write code. Most recently he's been feeding his bank account by coding in C++ and feeding his mind by coding in Haskell.