When the laws of logic meet the logic of laws

Abstract

This master thesis presents a brief introduction to type theory, starting at the simplest systems and building up to the Calculus of Inductive Constructions, the formal theory that lies behind some software tools called 'proof assistants'. We will then study a real-life problem based on an actual law (European Regulation 561 for Road Transport) and show that there exist ambiguous situations. Finally, we will use Coq, a proof assistant, to draft the correctness checking proof of our results on the law.