Combining effects with dependent types

• Název práce v češtině: Combining effects with dependent types
• Název v anglickém jazyce: Combining effects with dependent types
• Klíčová slova: dependent types|effect handlers|type systems
• Klíčová slova anglicky: dependent types|effect handlers|type systems
• Akademický rok vypsání: 2023/2024
• Typ práce: bakalářská práce
• Ústav: Katedra distribuovaných a spolehlivých systémů (32-KDSS)
• Vedoucí / školitel: Mgr. Tomáš Petříček, Ph.D.
• Řešitel: skrytý - zadáno a potvrzeno stud. odd.
• Datum přihlášení: 26.03.2024
• Datum zadání: 26.03.2024
• Datum potvrzení stud. oddělením: 04.04.2024

Zásady pro vypracování

There are multiple directions in the development of advanced and more expressive type systems for programming languages. On the one hand, algebraic effect handlers [6] are used to control how programs affect the world. On the other hand, dependent types [4, 7] make it possible to express richer properties using types. There is some work on combining those [8], but the design space for programming languages that combine multiple advanced type system features remains largely unexplored.

The aim of this thesis is to design a programming language that combines multiple of the recent research directions on advanced type system. The developed programming language may support a form of effect system inspired by Koka, Eff or Effekt [1, 2, 3] alongside with a form of dependent types [4] and may utilize bidirectional type checking [5] in the implementation. The thesis will focus on formally specifying the type system of the dependently typed core language with an extension for tracking effects.

Seznam odborné literatury

[1] Brachthäuser, J. I., Schuster, P., & Ostermann, K. (2020). Effekt: Lightweight effect polymorphism for handlers. Technical Report. University of Tübingen, Germany.
[2] Leijen, D. (2014). Koka: Programming with row polymorphic effect types. arXiv preprint arXiv:1406.2061.
[3] Bauer, A., & Pretnar, M. (2014). An effect system for algebraic effects and handlers. Logical methods in computer science, 10.
[4] Löh, A., McBride, C., & Swierstra, W. (2010). A tutorial implementation of a dependently typed lambda calculus. Fundamenta informaticae, 102(2), 177-207.
[5] Christiansen, D. R. (2013). Bidirectional typing rules: A tutorial. Available at: https://davidchristiansen.dk/tutorials/bidirectional.pdf
[6] Plotkin, G., & Pretnar, M. (2009). Handlers of algebraic effects. In European Symposium on Programming (pp. 80-94). Berlin, Heidelberg: Springer Berlin Heidelberg.
[7] Bove, A., Dybjer, P., & Norell, U. (2009). A brief overview of Agda–a functional language with dependent types. In Theorem Proving in Higher Order Logics: 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings 22 (pp. 73-78). Springer Berlin Heidelberg.
[8] Brady, E. (2013). Programming and reasoning with algebraic effects and dependent types. In Proceedings of the 18th ACM SIGPLAN international conference on Functional programming (pp. 133-144).