curry-howard

Slides of a (very) informal lecture of mine on the Curry-Howard correspondence

typechecking.c (163B)

 1 unsigned int f(unsigned int n)
 2 {
 3   if (n == 0) return 1;
 4   else return n * f(n - 1);
 5 }
 6 
 7 // error: implicit conversion from 'float' to 
 8 // 'unsigned int'
 9 f(0.5f);