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
Bibliographical item details
FieldValue
Type: Examensarbete för masterexamen
Title: A Haskell Implementation for a Dependent Type Theory with Definitions
Authors: Wang, Qufei
Abstract: We 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.
Keywords: computer science;dependent type theory;functional programming;type checker
Issue Date: 2021
Publisher: Chalmers tekniska högskola / Institutionen för data och informationsteknik
URI: https://hdl.handle.net/20.500.12380/304406
Collection:Examensarbeten för masterexamen // Master Theses



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