Monday, August 27, 2012

An astonishing isomorphism

›
I just learned today that in classical linear logic, the following type isomorphism holds: $$ (!A \multimap R) \multimap R \qquad\simeq\qqu...
1 comment:
Thursday, August 23, 2012

A Computational Lambda Calculus for Applicative Functors

›
These days, most people are familiar with using monads to structure functional programs, and are also familiar with Haskell's do-notatio...
4 comments:
Wednesday, August 8, 2012

An ML implementation of match compilation

›
In this post, I'll give an OCaml implementation of the pattern match compiler from my previous post. Just for fun, it will also pattern...
2 comments:
Monday, August 6, 2012

Pattern compilation made easy

›
One of the most practically useful features of functional programming languages is pattern matching, and one of the most important quality-o...
2 comments:
Thursday, August 2, 2012

Category Theory for Computing Science now free for download!

›
Michael Barr and Charles Wells have kindly made their book Category Theory for Computing Science freely available for download. IMO, this...
Thursday, July 12, 2012

A Relationally Parametric Model of the Calculus of Constructions

›
Derek and I have a new paper out, on a new parametric model of the calculus of constructions. A Relationally Parametric Model of the Calc...
Wednesday, May 30, 2012

Superficially Substructural Types at ICFP 2012!

›
My paper with Aaron Turon, Derek Dreyer, and Deepak Garg, Superficially Substructural Types , was accepted for publication at ICFP 2012! We...