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

Visa enkel post
dc.contributor.authorBrilakis, Konstantinos
dc.contributor.departmentChalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)sv
dc.contributor.departmentChalmers University of Technology / Department of Computer Science and Engineering (Chalmers)en
dc.date.accessioned2019-07-03T14:43:05Z
dc.date.available2019-07-03T14:43:05Z
dc.date.issued2018
dc.description.abstractThis 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.
dc.identifier.urihttps://hdl.handle.net/20.500.12380/255039
dc.language.isoeng
dc.setspec.uppsokTechnology
dc.subjectData- och informationsvetenskap
dc.subjectComputer and Information Science
dc.titleOn Initial Categories with Families Formalization of unityped and simply typed CwFs in Agda
dc.type.degreeExamensarbete för masterexamensv
dc.type.degreeMaster Thesisen
dc.type.uppsokH
local.programmeComputer science – algorithms, languages and logic (MPALG), MSc
Ladda ner
Original bundle
Visar 1 - 1 av 1
Bild (thumbnail)
Namn:
255039.pdf
Storlek:
2.28 MB
Format:
Adobe Portable Document Format
Beskrivning:
Fulltext
Ladda ner
Samling
Examensarbeten för masterexamen