Applications of algebraic effect theoriesLukšič, Žiga (Avtor) Pretnar, Matija (Mentor) Algebraic effectseffect handlersfunctional programmingtheory of programming languagesdenotational semanticsAlgebraic effects are an established method of implementing effectful behaviour in functional programming languages. Computational effects are represented by operations and implemented through effect handlers. An effect theory consists of a type signature and a set of equations describing the behaviour of effect invocations. All effect handlers are required to adhere to the prescribed effect theory, meaning that they do not differentiate between two programs considered equal in the given theory. The standard approach to algebraic effects assumes a global effect theory, so all handlers need to respect the same set of equations. This often becomes very restricting in terms of suitable handlers and therefore most contemporary work focuses on theories that contain no equations. Discarding equations allows for a wider variety of viable handlers but drastically reduces the capabilities to reason about properties of effectful code. In the thesis we present the language EEFF that relaxes the single theory limitation by using local effect theories, allowing the use of different theories in different parts of the program, even when pertaining to effects with the same signature. This alleviates the issues of global effect theories while providing all benefits of equations. The type system is upgraded to track theory information, allowing for safe use of handlers and ensuring their correctness at the relevant theory. Proofs of handler correctness are done in a logic that is coupled with the type system. The type system can be coupled with different logics, granting the option to select a logic suitable for the problems at hand. The soundness of a logic is established with respect to a denotational semantics based on partial equivalence relations. The safety theorems of EEFF are formalised in the proof assistant Coq, and the implementation of EEFF is an extension of the language Eff. The formalisation also doubles as a reasoning tool for programs with algebraic effect theories and features two different logics to choose from, both of which are shown to be sound. Multiple examples throughout the thesis showcase the benefits of local algebraic theories.20202020-11-15 08:15:02Doktorsko delo/naloga122007UDK: 510.6VisID: 116307COBISS_ID: 43657475sl