Coq for Haskell programmers

### The Subject ###

I’d like to tell you a story about the Coq proof assistant — a fascinating tool that has turned my hobby into my job.

Some people would say Haskell makes programming feel like maths, and Coq does so to a greater degree.

In fact, Coq allows one to do math on their computer or prove correctness of your programs!

I’ll present the basics of software verification using theorem provers, dependently-types programming and show how Coq can be useful to the working Haskell programmer through a number of tools.

### Beware! Coq is like video-gaming — very addictive. ###

### Introducing Anton Trunov ###

I’m a research programmer at IMDEA Software Institute, Madrid.
I have worked both in industry (embedded systems mostly) and in academia (high performance computing) for more than a decade.
And I have been enjoying my stay in the absolutely marvellous city of Madrid for a bit more than a year.

These days I’m doing formal verification in the area of concurrency as a member of the group developing a fine-grained concurrent separation logic framework.

You can find me on Twitter as @Anton_A_Trunov or on Stackoverflow as anton-trunov mostly answering Coq & Idris questions.

Presentation will be given in English.

### Your attention please !! ###
HaskellMAD will raffle a free ticket to participate in the Haskell eXchange 2018 conference, at CodeNode London City - from Thursday 11 to Friday 12 October. +info: https://skillsmatter.com/conferences/10237-haskell-exchange-2018#overview