Categorical semantics of dependent type theory
After a brief historical note on type theory and its semantics, we give the syntax of a basic dependent type theory in the style of Martin-Löf's Type Theory. We then discuss set-theoretic and categorical models, their uses and weaknesses. We describe the construction of a model of dependent typ...
| Κύριοι συγγραφείς: | , |
|---|---|
| Άλλοι συγγραφείς: | |
| Μορφή: | bachelorThesis |
| Γλώσσα: | Greek |
| Έκδοση: |
Εθνικό Μετσόβιο Πολυτεχνείο. Σχολή Εφαρμοσμένων Μαθηματικών και Φυσικών Επιστημών
2018
|
| Θέματα: | |
| Διαθέσιμο Online: | http://dspace.lib.ntua.gr/handle/123456789/47896 |