Companion Operator

A companion matrix is a matrix with a prescribed characteristic polynomial. I would like to show them from a broader perspective: companion matrices are the matrix version of a shift operator.

Read more

Type logic in Haskell

Type logic is the logic directly associated to types. It turns out that one can go quite far with regards to proving statements with Haskell. I show how to do that, and even how to prove statements in classical logic with Haskell.

Read more