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.

My goal is to derive Maxwell's equations of electromagnetism with almost no effort at all. As often in mathematics, things look simpler when there is less structure. Here, as in mechanics, we do not assume any prior metric, so the geometry of the space at hand is very simple.

I would like to explain how I carry out testing when I write code for scientific computing. It's partly using techniques that are common to the general philosophy of testing, and partly techniques that are specific to scientific computing.

Another Haskell version of Peter Norvig's spelling corrector, illustrating list monads, type classes and polymorphic programming.

The Reader and Writer monad are well known, but I would like to present their comonadic counterpart.

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.

A little JavaScript application to demonstrate two ideas:

• Equivariance

• Modified vector field

LaTeX has undergone incredible changes during the last decade. Unfortunately, many LaTeX users still use it as if we were still in the 90's! Here are some tips to use LaTeX to its maximum.