Please use this identifier to cite or link to this item:
Title: When the laws of logic meet the logic of laws
Author: del Castillo Tierz, Jorge del
Keywords: Lògica
Teoria de tipus
Tesis de màster
Type theory
Masters theses
Issue Date: 2018
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.
Note: Treballs Finals del Màster de Lògica Pura i Aplicada, Facultat de Filosofia, Universitat de Barcelona, Curs: 2017-2018, Tutor: Joost J. Joosten
Appears in Collections:Màster Oficial - Pure and Applied Logic / Lògica Pura i aplicada

Files in This Item:
File Description SizeFormat 
When_the_laws_of_logic_meet_the_logic_of_laws.pdf981.78 kBAdobe PDFView/Open

This item is licensed under a Creative Commons License Creative Commons