On Initial Categories with Families Formalization of unityped and simply typed CwFs in Agda

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/255039
Download file(s):
File Description SizeFormat 
255039.pdfFulltext2.33 MBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: On Initial Categories with Families Formalization of unityped and simply typed CwFs in Agda
Authors: Brilakis, Konstantinos
Abstract: 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.
Keywords: Data- och informationsvetenskap;Computer and Information Science
Issue Date: 2018
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
URI: https://hdl.handle.net/20.500.12380/255039
Collection:Examensarbeten för masterexamen // Master Theses



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.