Haskell talks at Formation

Come hang out and watch some awesome Haskell talks at Formation! Formation will be providing food and drinks as well.

Schedule
6 Doors open
6:30 First talk starts
7:20 Second talk starts
8:15 Mingle time
9 Doors close

Abstracts for the talks

@fnowarn will be giving a talk.

----

Title: Proving theorems and certifying programs with Coq
by Stephan Boyer

Abstract:

Have you ever wanted to formally prove an algorithm correct or a theorem true? This talk will show you how! We'll cover the fundamentals of computer-assisted theorem proving using Coq, one of the most popular proof assistants. Coq is a functional programming language whose type system can encode essentially any mathematical proposition.

Most introductions to Coq survey the landscape from a bird's eye view. You start by building proof scripts using high-level "tactics", and later you're introduced to the actual proofs generated by these tactics. For some, this is a bit too magical. You learn to prove simple theorems, but lack intuition for what the tactics are actually doing. That conundrum was frustrating for me when I was learning Coq in graduate school. This talk, in contrast, will feature no magic.

Instead, we will approach Coq from the perspective of a functional programmer. We'll start with the syntax, which will be familiar to Haskell programmers. We'll learn how to encode propositional logic in data types, which can be done in any functional language. Then we'll see how to encode quantifiers using dependent types, which completes the foundation of higher-order logic. Finally, we'll learn how to automate our proofs using Coq's tactic language. The more you automate, the shorter and more robust your proofs become!