ETD

Archivio digitale delle tesi discusse presso l’Università di Pisa

Tesi etd-09062022-221843

Tipo di tesi

Tesi di laurea magistrale

URN

etd-09062022-221843

Titolo

Counterpart Semantics for Quantified Temporal Logics: Sets, Categories and Agda

Dipartimento

INFORMATICA

Corso di studi

INFORMATICA

Parole chiave

Agda
categorical logic
category theory
counterpart semantics
dependent types
formalization
temporal logics

Data inizio appello

07/10/2022

Consultabilità

Completa

Riassunto (Inglese)

Riassunto (Italiano)

The aim of this thesis is to provide a complete presentation of the semantics of first-order temporal logics based on the counterpart paradigm: we start by introducing a standard set-based semantics and then we define a categorical semantics based on relational presheaves. The constructions are formalized using the dependently typed programming language and proof assistant Agda, and we employ the agda-categories library to adequately capture the notions of category theory required in our setting.

File

Nome file	Dimensione
Andrea_L...hesis.pdf	557.30 Kb
Contatta l’autore