Name: One-off meetup: Joachim Breitner visit
Start: 2017-05-03T19:00:00+02:00
End: 2017-05-03T22:00:00+02:00
Location: talent.io

Nous avons la chance d'avoir Joachim Breitner à Paris; let's meet and get inspired!

Le meetup aura lieu le 03 Mai à 19h à talent.io (http://talent.io/) , qui nous ouvrira ses portes, mais il faudra qu'on amène nos boissons -> je compte sur vous.

Who needs theorem provers when we have compilers?

After decades of work on functional programming and on interactive theorem proving, a Haskell programmer who wants to include simple equational proofs in his programs, e.g. that some Monad laws hold, is still most likely to simply do the derivation as comments in the file, as all the advanced powerful proving tools are inconvenient.

But one powerful tool capable of doing (some of) these proofs is hidden in plain sight: GHC, the Haskell compiler! Its optimization machinery, in particular the simplifier, can prove many simple equations all by himself, simply by compiling both sides and noting that the result is the same. Furthermore, and crucially to make this approach applicable to more complicated equations, the compiler can be instructed to do almost arbitrary symbolic term rewritings by using Rewrite Rules.

In this hands-on talk I will show a small GHC plugin that I can use to prove the monad laws for a non-trivial functor. I am looking forward to a discussion of the merits, limits and capabilities of this approach.

Speaker bio

Joachim Breitner has obtained a PhD in computer science from the
Karlsruhe Institute of Technology for a thesis about the Call Arity
compiler transformation that he introduced to GHC. He is currently a
postdoctoral researcher at the University of Pennsylvania in
Philadelphia. He is a member of the Debian project, the Haskell Core
Library Committee and the GHC Steering Committee, and he blogs about
his project on http://www.joachim-breitner.de/blog

lucasdicioccio

haskell-paris

Technology

Haskell

Functional Programming

Computer Programming

Programming Languages

New Technology

Web Technology

Web Programming

User Group

One-off meetup: Joachim Breitner visit

talent.io

Partager

haskell-paris

One-off meetup: Joachim Breitner visit

haskell-paris

Détails

Les membres s'intéressent également à