Type Theory and Mathematical Logic

The author works on a project in the area of Mathematical Logic and Applied Type Theory, involving heavy use of the Coq proof assisant.