Matija Pretnar
Fakulteta za matematiko in fizikoJadranska 21, SI-1000 Ljubljana
tel: +386 1 4766 668
matija.pretnar@fmf.uni-lj.si
GitHub
I study formalization, implementation, and semantics of programming languages. My current research is focused on algebraic effects and their handlers.
Zaposlen sem na Fakulteti za matematiko in fiziko, kjer poučujem večinoma računalniške predmete.
In the standard algebraic approach to effects, once an operation is called, the evaluation of the continuation stalls until it gets a result (either from a built-in primitive effect or through a handler). But we often desire asynchronous behaviour, when the continuation may proceed with the evaluation and suitably incorporates the result once it arrives. I will describe a small calculus with primitives for sending and receiving such signals.
Joint work with Danel Ahman
Projekt Tomo is a web service for teaching programming that works by providing students immediate and low-overhead automated feedback on the correctness of the submitted solutions. In the talk, I will describe the basic principles of the service, its history and how its eponym helped shape it.
The main premise of algebraic effects is that effects can be described with an equational theory consisting of a set of operations and equations between them. However, many computationally interesting algebraic effect handlers do not respect these equations, which most approaches nowadays reconcile by assuming a trivial equational theory. I will present an approach in which the expected equations may be encoded in computation types.
Joint work with Žiga Lukšič
Algebraic effects are computational effects that can be described with a set of basic operations and equations between them. As many interesting effect handlers do not respect these equations, most approaches assume a trivial theory, sacrificing both reasoning power and safety. I will present an alternative approach where the effect system tracks equations that are observed in subparts of the program, yielding a sound and flexible logic, and paving a way for practical optimizations and reasoning tools.
Joint work with Žiga Lukšič
Algebraic effects are computational effects that can be described with a set of basic operations and equations between them. As many interesting effect handlers do not respect these equations, most approaches assume a trivial theory, sacrificing both reasoning power and safety.
We present an alternative approach where the type system tracks equations thar are observed in subparts of the program, yielding a sound and flexible logic, and paving a way for practical optimizations and reasoning tools.
Joint work with Žiga Lukšič
To inform the programmer about the effects of a given program, a bottom up inference algorithm that Eff provides is sufficient. However, for an optimizing compiler, we need access to effects of all subterms. It turned out that adapting the current algorithm is overly error-prone as the core language is implicitly typed and subtyping-based.
In hope of remedying the situation, we present an explicitly-typed polymorphic core calculus, which reifies appeals to subtyping in explicit casts with coercions that witness the subtyping proof. We provide a constraint-based inference algorithm that turns an implicitly-typed term into our calculus, and effect erasure, which allows us to targets an ML-like language with or without support for algebraic effects.
The talk will include a brief introduction to algebraic effect handlers.
Joint work with Amr Hany Saleh, George Karachalias and Tom Schrijvers
Recimo, da so učenci 3. b razreda pri testu iz matematike dosegli povprečno 63%, učenci 3. c razreda pa 70%. Ali so učenci 3. c res bolj razumeli snov ali pa je razlika le posledica zunanjih dejavnikov in bi bil kakšen drug dan rezultat ravno obraten? Kaj pa, če se enaka razlika pojavi še pri naslednjem testu? S kakšno gotovostjo lahko rečemo, da ni šlo za naključje? Statistika nam na taka vprašanja zna odgovoriti, vendar so odgovori dostikrat precej zapleteni. Na seminarju si bomo zato ogledali alternativen pristop, pri katerem iskano gotovost ocenimo s pomočjo računalniških simulacij.
Programming is a skill that often demands that students engage in a significantly high amount of individual practice and experimentation in order to acquire basic competence. Teachers are required to both encourage students by exposing them to numerous problems and supervise the students' attempts to solve them.
To support this teaching approach we developed a web service called Projekt Tomo, presented in the article. The service is designed in such a way that it requires little or no additional work from students and teachers, enabling them to focus on the content. Furthermore, the service can be used in almost all teaching environments, as it can be adapted to most programming languages and has minor technical requirements.
Joint work with Matija Lokar