This is a cool effort. Since agda : haskell :: coq : ocaml, I'm curious why agda wasn't used. Does it not not support extraction in the same way?<p>I would liked to have seen the talk itself since there are a few places in the slides where more detail would be nice. For example, I saw no reason why focusLeft on slide 40 wouldn't be total---it's not recursive, so why wouldn't it terminate? (given that reverse is total)<p>I also wonder whether most functions in functional programs can be rewritten so that termination is evident due to structural recursion (like the transformation described on slide 41).