Normalization of dependent types with subtyping
Event details
| Date | 01.09.2022 |
| Hour | 10:30 › 12:30 |
| Speaker | Matthieu Bovel |
| Location | |
| Category | Conferences - Seminars |
EDIC candidacy exam
Exam president: Prof. Rachid Guerraoui
Thesis advisor: Prof. Martin Odersky
Thesis co-advisor: Prof Viktor Kuncak
Co-examiner: Prof. Christoph Koch
Abstract
coming soon
Background papers
[1] T. Freeman and F. Pfenning, “Refinement types for ml,” SIGPLAN
Not., vol. 26, no. 6, p. 268–277, may 1991. [Online]. Available:
https://doi.org/10.1145/113446.113468
[2] D. Aspinall, “Subtyping with singleton types,” in Computer Science
Logic, L. Pacholski and J. Tiuryn, Eds. Berlin, Heidelberg:
Springer Berlin Heidelberg, 1995, pp. 1–15. [Online]. Available:
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.5.8740&rep=rep1&type=pdf
[3] O. Blanvillain, J. I. Brachth ̈auser, M. Kjaer, and M. Odersky, “Type-level
programming with match types,” Proc. ACM Program. Lang., vol. 6, no.
POPL, jan 2022. [Online]. Available: https://doi.org/10.1145/3498698
Exam president: Prof. Rachid Guerraoui
Thesis advisor: Prof. Martin Odersky
Thesis co-advisor: Prof Viktor Kuncak
Co-examiner: Prof. Christoph Koch
Abstract
coming soon
Background papers
[1] T. Freeman and F. Pfenning, “Refinement types for ml,” SIGPLAN
Not., vol. 26, no. 6, p. 268–277, may 1991. [Online]. Available:
https://doi.org/10.1145/113446.113468
[2] D. Aspinall, “Subtyping with singleton types,” in Computer Science
Logic, L. Pacholski and J. Tiuryn, Eds. Berlin, Heidelberg:
Springer Berlin Heidelberg, 1995, pp. 1–15. [Online]. Available:
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.5.8740&rep=rep1&type=pdf
[3] O. Blanvillain, J. I. Brachth ̈auser, M. Kjaer, and M. Odersky, “Type-level
programming with match types,” Proc. ACM Program. Lang., vol. 6, no.
POPL, jan 2022. [Online]. Available: https://doi.org/10.1145/3498698
Practical information
- General public
- Free