A Haskell Implementation for a Dependent Type Theory with Definitions
Ladda ner
Typ
Examensarbete för masterexamen
Program
Publicerad
2021
Författare
Wang, Qufei
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
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.
Beskrivning
Ämne/nyckelord
computer science , dependent type theory , functional programming , type checker