On Initial Categories with Families Formalization of unityped and simply typed CwFs in Agda
Ladda ner
Typ
Examensarbete för masterexamen
Master Thesis
Master Thesis
Program
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2018
Författare
Brilakis, Konstantinos
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
This thesis explores a categorical model of type theory, namely, categories with families who provide a model for a basic framework of dependent type theory. The notion of a category with families is formalized as a generalized algebraic theory with extra structure with the purpose of modelling different lambda calculi. The work revolves around implementing in the Agda proof assistant categories with families at three levels: (i) untyped, (ii) simply typed, and (iii) dependently typed calculi. The formalization primarily consists of constructing initial objects in the category of categories with families and isomorphisms between them. The work investigates each notion from its core and proceeds by adding extra structure. Complete formalizations of untyped and simply typed categories with families are presented along with an incomplete picture for dependent types.
Beskrivning
Ämne/nyckelord
Data- och informationsvetenskap , Computer and Information Science