Arnaud Spiwack
Arnaud Spiwack spend the first 10 years of his working life in Academia, between Chalmers university in Gothenburg, Sweden, and Ecole Polytechnique, Inria, and Mines ParisTech, in the Paris area. He spent this time researching dependent types, computer-verified proof, and sequent calculus. During his time in Academia, Arnaud got involved in the development of the Coq Proof Assistant, where he, in particular, re-engineered Coq's tactic engine and gave it an abstract interface. After leaving academia, he remained a member of the core development team of the Coq Proof Assistant. He is now a senior architect at Tweag I/O, and is working at making the world better typed.
Talks I've Given
-
Comparing Strict and Lazy
Featuring Arnaud Spiwack
Strict and lazy languages are often pitted against each other but rarely honestly compared. Let's take a step back from the slogans and examine the trade-offs between lazy and strict. Not which is best: how they compare.
haskell strict lazy -
Binding Types à la carte
Featuring Arnaud Spiwack
Imagine you want to write a data type for an abstract syntax tree with binders. You get started, write a function for substitution. Get lost in the renaming story.
haskell quantified-constraints category-theory algebraic-data-types binders abstract-syntax-trees -
Distributed Programming with Linear Types
Featuring Arnaud Spiwack
It is a very haskellian thing to do, to solve problems by applying types to them. In this talk, you will learn to do just that, to problems found in distributed programming. The interesting commonality of these problems is that they are not commonly recognised as having a solution in the space of...
haskellx haskell programming types