A Haskell Implementation for a Dependent Type Theory with Definitions

Examensarbete för masterexamen

Använd denna länk för att citera eller länka till detta dokument: https://hdl.handle.net/20.500.12380/304406
Ladda ner:
Fil Beskrivning StorlekFormat 
CSE 21-161 Qufei.pdf1.4 MBAdobe PDFVisa
Bibliografiska detaljer
Typ: Examensarbete för masterexamen
Titel: A Haskell Implementation for a Dependent Type Theory with Definitions
Författare: Wang, Qufei
Sammanfattning: 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.
Nyckelord: computer science;dependent type theory;functional programming;type checker
Utgivningsdatum: 2021
Utgivare: Chalmers tekniska högskola / Institutionen för data och informationsteknik
URI: https://hdl.handle.net/20.500.12380/304406
Samling:Examensarbeten för masterexamen // Master Theses

Materialet i Chalmers öppna arkiv är upphovsrättsligt skyddat och får ej användas i kommersiellt syfte!