# name
When the laws of logic meet the logic of laws

# metadata.dc.description[].value
Treballs Finals del Màster de Lògica Pura i Aplicada, Facultat de Filosofia, Universitat de Barcelona, Curs: 2017-2018, Tutor: Joost J. Joosten

# metadata.dc.description.abstract[].value
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.

# metadata.dc.source[].value
Màster Oficial - Pure and Applied Logic / Lògica Pura i aplicada

# metadata.dc.title[].value
When the laws of logic meet the logic of laws