Original title: Combining effects with dependent types
Translated title: Combining effects with dependent types
Authors: Mückenschnabel, Maya ; Petříček, Tomáš (advisor) ; Šefl, Vít (referee)
Document type: Bachelor's theses
Year: 2024
Language: cze
Abstract: Dependent type systems provide a novel way of reasoning about program correctness, by embedding behavior of the program into the more expressive type system. Correctness is achieved by not allowing incorrect states to be representable. Languages like Idris show that dependent type systems are practically useful, not only for formal proofs, but also for creating fewer bugs in production. But the purity of computation poses a problem for composability of stateful computations and of side effects. Effect handlers provide one possible solution for this problem. In this thesis we propose an effect extension of depen- dent type systems. The resulting system not only makes it possible to provide guarantees about correctness of a program, but also make it easy to compose such guarantees using effects. We formalize the type system and present a prototype implementation.
Keywords: dependent types|effect handlers|type systems; dependent types|effect handlers|type systems

Institution: Charles University Faculties (theses) (web)
Document availability information: Available in the Charles University Digital Repository.
Original record: http://hdl.handle.net/20.500.11956/192041

Permalink: http://www.nusl.cz/ntk/nusl-622732


The record appears in these collections:
Universities and colleges > Public universities > Charles University > Charles University Faculties (theses)
Academic theses (ETDs) > Bachelor's theses