A Haskell Implementation for a Dependent Type Theory with Definitions

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/304406
Download file(s):
File Description SizeFormat 
CSE 21-161 Qufei.pdf1.4 MBAdobe PDFView/Open
Full metadata record
DC FieldValueLanguage
dc.contributor.authorWang, Qufei-
dc.contributor.departmentChalmers tekniska högskola / Institutionen för data och informationstekniksv
dc.description.abstractWe present in this paper a simple dependently typed language. This language could be viewed as a pure -calculus extended with dependent types and definitions. The focus of this project is on the study of a definition mechanism where the definitions of constants could be handled efficiently during the type checking process. We later enrich the language with a module system to study how the definition mechanism should be adjusted for the introduction of the concept namespace on variables. The outcome of our work is a REPL(read-evaluate-print-loop) program through which a source file of our language could be loaded and type checked. The program also provides auxiliary functions for users to experiment with and observe the effect of the definition mechanism. The syntax of our language is specified by the BNF converter and the program is implemented in Haskell. We hold the expectation that our work could contribute to the development of proof assistant systems based on the dependent type theory.sv
dc.subjectcomputer sciencesv
dc.subjectdependent type theorysv
dc.subjectfunctional programmingsv
dc.subjecttype checkersv
dc.titleA Haskell Implementation for a Dependent Type Theory with Definitionssv
dc.type.degreeExamensarbete för masterexamensv
dc.contributor.examinerBove, Ana-
dc.contributor.supervisorCoquand, Thierry-
Collection:Examensarbeten för masterexamen // Master Theses

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