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.


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.






Variational Equation

The variational equation is a fundamental tool in engineering. It is the description of the sensitivity with respect to the initial conditions. A remarkable fact, often presented only in \(\mathbf{R}^n\), is that this is in fact the solution of another differential equation, sometimes called the variational equation. I would like to show that this is valid in general manifolds.