Matija Pretnar

Matija Pretnar

Fakulteta za matematiko in fiziko
Jadranska 21,
SI-1000 Ljubljana
tel: +386 1 4766 668
mail: matija.pretnar@fmf.uni-lj.si
GitHub: matijapretnar
ORCID iD: 0000-0001-7755-2303
Bibliografija: COBISS DBLP Scholar Scopus Sicris

Življenjepis (PDF)

Raziskovanje

Ukvarjam se s formalizacijo, implementacijo in semantiko programskih jezikov. Moje trenutne raziskave so usmerjene na algebrajske učinke in njihove prestreznike.

Poučevanje

Zaposlen sem na Fakulteti za matematiko in fiziko, kjer poučujem večinoma računalniške predmete.

Dejavnost

  1. 2026

    1. Uvod v kvantno računalništvo

      Povzetek

      V medijih pogosto beremo, da so kvantni računalniki hitri, ker jim kvantna superpozicija omogoča, da so v več stanjih hkrati, s čimer lahko izračunajo vse možne rezultate v enem samem koraku. Kot bomo videli, stvari niso tako preproste, saj se kvantni svet obnaša tudi tako, da na koncu lahko preberemo le enega od vseh rezultatov, pa še ta je naključno izbran. Da bi vseeno pripravili računalnik do tega, da izračuna rezultat, ki si ga želimo, moramo biti malo bolj zviti in uporabiti interferenco, s katero se neželeni rezultati med seboj izničijo. Na predavanju bomo spoznali nenavadne vidike kvantnega sveta ter si ogledali Groverjev algoritem za iskanje igle v kopici sena (natančneje, zaporedja bitov, za katerega dana funkcija vrne 1) in Shorov algoritem za razcep na praštevila.

      • Programski odbor, OOPSLA

  2. 2025

    1. Symmetric programming

      • IFIP WG2.1 meeting #83
      • 8. september 2025
      • Viana do Castelo
      • PDF
      • Keynote
      Povzetek

      In computer science, symmetry in data structures such as binary search trees is often handled either by code replication or by clever tricks that unify symmetric cases. This talk explores a mathematical framework based on group actions, which captures such constructions directly and uniformly. It also provides a natural way to express proofs that rely on “without loss of generality” (wlog), a mathematical staple whose computational significance is increasingly important with the proliferation of proof assistants.

      Joint work with Ohad Kammar.

      • Prodekan za informatiko UL FMF
        • 2025–2027
      • Programski odbor, FoSSaCS

  3. 2024

    1. Simplifying explicit subtyping coercions in a polymorphic calculus with effects.

      Filip Koprivec, Matija Pretnar

    2. Bringing the WebAssembly Standard up to Speed with SpecTec.

      Dongjun Youn, Wonho Shin, Jaehyun Lee, Sukyoung Ryu, Joachim Breitner, Philippa Gardner, Sam Lindley, Matija Pretnar, Xiaojia Rao, Conrad Watt, Andreas Rossberg

      • Proc. ACM Program. Lang.
      • DOI
      • DBLP

    3. A case study in mathematically inspired language constructs

      • IFIP WG2.1 meeting #81
      • 5. april 2024
      • Neustadt
      • PDF
      • Keynote
      Povzetek

      Even though the mathematical core of algebraic effect handlers has remained unchanged, they have evolved into a more useful programming construct since their introduction. In the talk, I will talk about steps (and one missed opportunity!) on the way to their discovery, initial considerations behind their design, and lessons learnt along the way.

    4. Effect handlers and mathematically inspired language constructs

      Povzetek

      Effect handlers are a programming language construct able to express and combine diverse computational features such as backtracking, stream redirection, multiple scheduling strategies, or continuations. This flexibility comes as no surprise since handlers are based on even more versatile homomorphisms of algebraic theories. Even though the design of handlers witnessed multiple iterations and extensions, their mathematical core remained unchanged.

      In this seminar, I will discuss the discovery of effect handlers and initial considerations behind their design, in particular steps required when translating a mathematical concept into a useful programming tool. We shall also take a look at subsequent research on handlers, for example various effect systems or an efficient transpiler to OCaml, comparing features guided by mathematics and those with a more practical motivation.

      • Programski odbor, ESOP
      • Programski odbor, APLAS

  4. 2023

    1. Wasm SpecTec: Engineering a Formal Language Standard.

      Joachim Breitner, Philippa Gardner, Jaehyun Lee, Sam Lindley, Matija Pretnar, Xiaojia Rao, Andreas Rossberg, Sukyoung Ryu, Wonho Shin, Conrad Watt, Dongjun Youn

    2. Higher-Order Asynchronous Effects.

      Danel Ahman, Matija Pretnar

    3. Continuing WebAssembly with Effect Handlers.

      Luna Phipps-Costin, Andreas Rossberg, Arjun Guha, Daan Leijen, Daniel Hillerström, KC Sivaramakrishnan, Matija Pretnar, Sam Lindley

    4. The state of Eff

      Povzetek

      The talk describes the history and the current state of Eff, the first programming language with native support of algebraic effect handlers. The first version of Eff was developed by Andrej Bauer and myself and appeared in 2010. It was untyped and had a syntax similar to Python. In the next version in 2011, we introduced the more commonly known ML-like syntax and dynamic generation of effect instances that worked analogously to references in OCaml. After that, the versions are a bit harder to reconstruct, but the main improvement was a subtyping-based effect system.

      Building on the effect system, the next goal for Eff was an optimizing compiler, on which I worked together with Tom Schrijvers and his students. The compiler would produce efficient code by inlining handlers as much as possible, and monadically embed the rest in OCaml. It soon became obvious that the effect system has to be more robust, which was achieved by using coercions as explicit witnesses of subtyping. Currently, Filip Koprivec, my PhD student, focuses on simplifying those witnesses in the polymorphic setting, as otherwise each coercion needs to be passed around as an additional parameter at runtime. In parallel to the optimizing compiler project, Žiga Lukšič developed EEff, a variant of Eff that tracks algebraic equations between operations that have to be respected by the handlers. Currently, EEff only prints out the obligations, though one could envision sending them to an SMT solver or producing specifications for a proof assistant.

      Finally, the talk mentions Millet, a language one can use as a basis when developing a prototype language exploring an interesting novel idea. Millet implements all the boring and expected components of a programming language (parsing, algebraic datatypes, simple type-checking, interactive toplevel, compilation pipeline, …), and any fork just needs to extend all the components with the support for the additional features. Then, any later change to Millet (right now, a module system, a Wasm backend, and LSP support are in the works) should be orthogonal and can hopefully be merged into forks with not too much additional work.

    5. Simplifying explicit subtyping

      • IFIP WG2.1 meeting #80
      • 18. julij 2023
      • Oxford
      • Notes
      Povzetek

      Our recent work (Karachalias et al., OOPSLA 2021) has shown that code written using the full flexibility of handlers can be transformed into a pure one that matches the performance of a conventional handcrafted one. However, to do so, the compiler tracks effect information through explicit subtyping coercions, and for polymorphic functions, these need to be passed around as additional parameters. Since subtyping coercions are inferred automatically, their number grows with the size of the program, which drastically reduces the performance. To avoid this, all polymorphic functions need to be annotated with particular types, or monomorphised by the compiler, neither of which is a satisfactory solution. In the talk, I will describe a simple algorithm that drastically, yet soundly, reduces (and often completely eliminates) redundant coercion parameters, leading to a performance comparable to monomorphic code.

    6. Asynchronous Effects

      • Scottish Programming Languages Seminar
      • 7. junij 2023
      • University of the West of Scotland, Paisley
      • PDF
      • Keynote
      • SPLS
      Povzetek

      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 such signals and receiving corresponding interrupts, and show a small prototype in which one can express promises, preemptive multi-threading and remote function calls.

      Joint work with Danel Ahman.

      • Programski odbor, OCaml Workshop
      • Programski odbor, ML Family Workshop

  5. 2022

    1. Mentorstva pri zaključnih delih

      • Luna Strah: Kvantni algebrajski učinki
      • Tadej Petrič: ZX-račun
      • Organizacijski odbor, OCaml Users and Developers Workshop
        • 2022–2027
      • Vodja programskega odbora, OCaml Workshop
      • Programski odbor, ICFP
      • Programski odbor, TYPES
      • Programski odbor, ML Family Workshop

  6. 2021

    1. (Higher-order) asynchronous effects

      Danel Ahman, Matija Pretnar, Janez Radešček

      • Scalable handling of effects : Report from Dagstuhl Seminar 21292

    2. Asynchronous effects

      Danel Ahman, Matija Pretnar

      • Proceedings of the ACM on Programming Languages
      • DOI
      • DBLP

    3. Efficient compilation of algebraic effect handlers

      Georgios Karachalias, Filip Koprivec, Matija Pretnar, Tom Schrijvers

      • Proceedings of the ACM on Programming Languages
      • DOI
      • DBLP

    4. Spletna storitev za generiranje nalog

      • FMF seminar za učitelje matematike, Fakulteta za matematiko in fiziko
      • 25. september 2021
      • Ljubljana

    5. Efficient compilation of algebraic effect handlers

      • Dagstuhl Seminar 21292
      • 21. julij 2021
      • Dagstuhl (remotely)
      • PDF
      • Keynote
      Povzetek

      The popularity of algebraic effect handlers as a programming language feature for user-defined computational effects is steadily growing. Yet, even though efficient runtime representations have already been studied, most handler-based programs are still much slower than hand-written code.

      This paper shows that the performance gap can be drastically narrowed (in some cases even closed) by means of type-and-effect directed optimising compilation. Our approach consists of source-to-source transformations in two phases of the compilation pipeline. Firstly, elementary rewrites, aided by judicious function specialisation, exploit the explicit type and effect information of the compiler’s core language to aggressively reduce handler applications. Secondly, after erasing the effect information further rewrites in the backend of the compiler emit tight code.

      This work comes with a practical implementation: an optimizing compiler from Eff, an ML style language with algebraic effect handlers, to OCaml. Experimental evaluation with this implementation demonstrates that in a number of benchmarks, our approach eliminates much of the overhead of handlers, outperforms capability-passing style compilation and yields competitive performance compared to hand-written OCaml code as well Multicore OCaml’s dedicated runtime support.

    6. Introduction to Quantum Computing

      Povzetek

      We often read in the media that quantum computers are fast because quantum superposition allows them to be in multiple states at once, enabling them to explore all the possible solutions in a single step.

      As we shall see, things are not that simple because, in the end, we can observe only one randomly chosen result, which is likely not going to be the one we need. After all, with all the possible solutions out there, what’s the guarantee that the one we want is the one randomly chosen by the quantum computer? So we want to be able to increase the probability of getting the solution we want from among all the possible paths.

      What can be done is to use interference to cancel out all the undesirable paths and unwanted solutions. Although we still end up with a randomly chosen path, it is a path chosen from among the ones we want.

    7. Mentorstva pri zaključnih delih

      • Janez Radešček: Asinhroni algebrajski učinki
        • magisterij
        • somentor Danel Ahman
        • COBISS
      • Rok Koleša: Prevajanje prestreznikov algebrajskih učinkov v Javascript
      • Jakob Zmrzlikar: Jedrne metode

  7. 2020

    1. Explicit effect subtyping.

      Georgios Karachalias, Matija Pretnar, Amr Hany Shehata Saleh, Stien Vanderhallen, Tom Schrijvers

      • Journal of functional programming
      • DOI
      • DBLP

    2. Local algebraic effect theories.

      Žiga Lukšič, Matija Pretnar

      • Journal of functional programming
      • DOI
      • DBLP

    3. Kvantno računalništvo

      • Gimnazija Bežigrad
      • 23. januar 2020
      • Ljubljana
      • PDF
      • Keynote

    4. Asynchronous operations

      • IFIP WG2.1 meeting #79
      • 8. januar 2020
      • Otterlo
      • PDF
      • Keynote
      Povzetek

      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.

    5. Mentorstva pri zaključnih delih

      • Žiga Lukšič: Applications of algebraic effect theories
      • Urša Pertot: Knjižnica za samodejno generiranje matematičnih nalog
      • Žiga Zupančič: Prevajanje prestreznikov algebrajskih učinkov v jezik brez učinkov
      • Redni član IFIP Working Group 2.1 on Algorithmic Languages and Calculi
        • 2020–
      • Programski odbor, LOLA

  8. 2019

    1. On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control

      Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar

      • Journal of functional programming
      • DOI
      • DBLP

    2. Bringing equations back to algebraic effect handlers

      Povzetek

      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č

    3. Projekt Tomo

      • Maps ∩ Configurations ∩ Polytopes ∩ Molecules ⊆ Graphs: The mathematics of Tomaž Pisanski on the occasion of his 70th birthday
      • 23. maj 2019
      • Ljubljana
      • PDF
      • Keynote
      Povzetek

      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.

    4. Local algebraic effect theories

      • Meet The Jury!
      • 23. januar 2019
      • Leuven
      • PDF
      • Keynote
      Povzetek

      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č.

    5. Mentorstva pri zaključnih delih

      • Filip Koprivec: Eksplicitna izpeljava učinkov
      • Anže Nunar: Analiza in vizualizacija nepremičninskih podatkov v Sloveniji
      • Nina Slivnik: Uporaba polkolobarjev z zaprtjem
        • diploma
        • somentorica Polona Oblak
        • COBISS
        • RUL
      • Vodja programerskega kluba UL FMF
        • 2019–

  9. 2018

    1. Design and implementation of the Andromeda proof assistant

      Andrej Bauer, Gaëtan Gilbert, Philipp Georg Haselwarter, Matija Pretnar, Christopher A Stone

      • 22nd International Conference on Types for Proofs and Programs : TYPES 2016
      • DOI
      • DBLP

    2. Explicit effect subtyping.

      Amr Hany Shehata Saleh, Georgios Karachalias, Matija Pretnar, Tom Schrijvers

      • 27th European Symposium on Programming, ESOP 2018
      • DOI
      • DBLP

    3. Putting reason back into handlers

      • IFIP WG2.1 meeting #77
      • 3. julij 2018
      • Brandenburg
      • PDF
      • Keynote
      Povzetek

      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č.

    4. Mentorstva pri zaključnih delih

      • Lenart Treven: Metode podpornih vektorjev
        • diploma
        • Fakultetna Prešernova nagrada, somentor Jan Kralj
        • COBISS
        • RUL
      • Soorganizator, Dagstuhl Seminar 18172 (Algebraic Effect Handlers go Mainstream)
      • Skrbnik študijskega programa Računalništvo in matematika (1. in 2. stopnja) UL FMF
        • 2018–2025

  10. 2017

    1. Modelling the spread of bluetongue in Slovenia.

      Tanja Knific, Tadej Malovrh, Marko Potočnik, Matija Pretnar, Milica Krković, Aljoša Vodopija, Jasna Prezelj-Perman

      • ModAH, Nantes, 14 - 16. June 2017

    2. No value restriction is needed for algebraic effects and handlers.

      Ohad Kammar, Matija Pretnar

      • Journal of functional programming
      • DOI
      • DBLP

    3. On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control

      Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar

      • Proceedings of the ACM on Programming Languages
      • DOI
      • DBLP

    4. Explicit effects subtyping

      • IFIP WG2.1 meeting #76
      • 18. oktober 2017
      • Lesbos
      • HTML
      Povzetek

      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.

    5. Mentorstva pri zaključnih delih

      • Samo Kralj: Modul za analizo oddanih rešitev na spletni storitvi Projekt Tomo
      • Filip Koprivec: Uporaba tipov za zagotavljanje pravilnosti programov
      • Organizator, MFPS in CALCO (združeni konferenci)
      • Sovodja programskega odbora, LOLA
      • Programski odbor, HOPE

  11. 2016

    1. Capturing algebraic equations in an effect system.

      Matija Pretnar

      • From theory to practice of algebraic effects and handlers : Report from Dagstuhl Seminar 16112

    2. Compiling Eff to OCaml.

      Matija Pretnar, Amr Hany Shehata Saleh, Tom Schrijvers

      • From theory to practice of algebraic effects and handlers : Report from Dagstuhl Seminar 16112

    3. No value restriction is needed for algebraic effects and handlers.

      Ohad Kammar, Sean Moss, Matija Pretnar

      • From theory to practice of algebraic effects and handlers : Report from Dagstuhl Seminar 16112
      • DBLP

    4. Towards an effect system for OCaml.

      Matija Pretnar, Stephen Dolan, KC Sivaramakrishnan, Leo White

      • From theory to practice of algebraic effects and handlers : Report from Dagstuhl Seminar 16112

    5. A tutorial on algebraic effects and handlers.

      Matija Pretnar

      • From theory to practice of algebraic effects and handlers : Report from Dagstuhl Seminar 16112

    6. Executive summary.

      Andrej Bauer, Martin Hofmann, Matija Pretnar, Jeremy Yallop

      • From theory to practice of algebraic effects and handlers : Report from Dagstuhl Seminar 16112

    7. Design and implementation of the Andromeda proof assistant

      Andrej Bauer, Gaëtan Gilbert, Philipp Georg Haselwarter, Matija Pretnar, Christopher A Stone

      • TYPES 2016 : book of abstracts
      • DBLP

    8. No value restriction is needed for algebraic effects and handlers

      Ohad Kammar, Sean Moss, Matija Pretnar

      • TYPES 2016 : book of abstracts
      • DBLP

    9. Hekerski pristop k statistiki

      • FMF seminar za učitelje matematike
      • 1. oktober 2016
      • Ljubljana
      • PDF
      • Keynote
      Povzetek

      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.

    10. Modeliranje širjenja kužnih bolezni: primer bolezni modrikastega jezika v Sloveniji

      Tanja Knific, Tadej Malovrh, Marko Potočnik, Matija Pretnar, Milica Krković, Aljoša Vodopija, Jasna Prezelj-Perman

      • 6. Slovenski veterinarski kongres 2016

    11. Mentorstva pri zaključnih delih

      • Valerija Kac: Razvoj podatkovne baze za veterinarsko ambulanto
      • Soorganizator, Dagstuhl Seminar 16112 (From Theory to Practice of Algebraic Effects and Handlers)
      • Vzpostavitev in razvoj sistema za urnike na UL FMF
        • 2016–2021
        • Na osnovi storitve je podjetje AFlabs zgradilo rešitev za urnike na UL.
      • Programski odbor, IFL

  12. 2015

    1. A low overhead automated service for teaching programming

      • Koli Calling 2015
      • 20. november 2015
      • Koli
      • PDF
      • Keynote
      Povzetek

      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.

    2. A low overhead automated service for teaching programming.

      Matija Lokar, Matija Pretnar

      • 15th Koli Calling Conference on Computing Education Research, November 19-22, 2015
      • DOI

    3. An introduction to algebraic effects and handlers. Invited tutorial paper.

      Matija Pretnar

      • The 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI)
      • DOI

    4. An Introduction to Algebraic Effects and Handlers

    5. Preparing programming exercises with efficient automated validation tests.

      Gregor Jerše, Sonja Jerše, Matija Lokar, Matija Pretnar

      • International Conference on Informatics in Schools - ISSEP 2015

    6. Programming with algebraic effects and handlers.

      Andrej Bauer, Matija Pretnar

      • Journal of logical and algebraic methods in programming
      • DOI
      • DBLP

    7. A web service for teaching programming.

      Gregor Jerše, Sonja Jerše, Matija Lokar, Matija Pretnar

      • International Conference on Informatics in Schools - ISSEP 2015, September 28- October 1, Ljubljana, Slovenia

    8. YASAAPE - Yet Another System for Automatic Assessment of Programming Exercises.

      Gregor Jerše, Sonja Jerše, Matija Lokar, Matija Pretnar

      • International Conference on Informatics in Schools - ISSEP 2015, September 28- October 1, Ljubljana, Slovenia

    9. Mentorstva pri zaključnih delih

      • Tina Janša: Izračun zahtevanega solventnostnega kapitala za zavarovalnice in pozavarovalnice po standardni formuli v programskem jeziku R
        • magisterij
        • somentorica Nataša Đukić
        • COBISS
        • RUL
      • Vzpostavitev in razvoj sistema Boter za administrativne evidence na UL FMF
        • 2015–2020

  13. 2014

    1. An effect system for algebraic effects and handlers.

      Andrej Bauer, Matija Pretnar

      • Logical methods in computer science
      • DOI
      • DBLP

    2. Inferring algebraic effects

      Matija Pretnar

      • Logical methods in computer science
      • DOI
      • DBLP

    3. Osnove kvantnega računalništva, 2. del

      Matija Pretnar

      • Obzornik za matematiko in fiziko

    4. Spletna storitev za poučevanje programiranja.

      Matija Pretnar

      • Vzgoja in izobraževanje v informacijski družbi - VIVID 2014

  14. 2013

    1. An effect system for algebraic effects and handlers.

      Andrej Bauer, Matija Pretnar

      • 5th Conference on Algebra and Coalgebra in Computer Science, CALCO 2013
      • DOI
      • DBLP

    2. Handling algebraic effects.

      Gordon Plotkin, Matija Pretnar

      • Logical methods in computer science
      • DOI
      • DBLP

    3. Osnove kvantnega računalništva, 1. del.

      Matija Pretnar

      • Obzornik za matematiko in fiziko

    4. Mentorstva pri zaključnih delih

      • Tomaž Stepišnik Perdih: Generiranje izrekov iz tipov funkcij v polimorfnem lambda računu

  15. 2012

    1. Mentorstva pri zaključnih delih

      • Tina Janša: Spletna aplikacija za linearno programiranje
      • Andrej Maršič: Uporaba genetskih algoritmov in metod Monte Carlo za iskanje optimalne strategije samozadrževanja v bonus-malus sistemih

  16. 2011

    1. The f-calculus

      Povzetek

      To see how useful Plotkin and Power’s algebraic effects are in programming, Andrej Bauer and I have developed a language called eff, based on such an approach. As it turns out, eff is very suitable for writing programs that use nondeterminism, rollback, delimited continuations, scheduling, and many other effects. In the talk, I will present the f-calculus, which formalizes eff’s core, its type system, and its semantics.

      • Soorganizator, European Workshop on Computational Effects

  17. 2010

    1. The logic and handling of algebraic effects

      Matija Pretnar

      • Tajnik slovenske podružnice ACM
        • 2010–2012

  18. 2009

    1. Handlers of algebraic effects.

      Gordon Plotkin, Matija Pretnar

      • 18th European Symposium on Programming, ESOP 2009
      • ETAPS 2022 Test of Time Award
      • DOI
      • Soorganizator, 6. mednarodna konferenca Computability and Complexity in Analysis (CCA)
      • Skrbnik spletne učilnice UL FMF
        • 2009–

  19. 2008

    1. A logic for algebraic effects.

      Gordon Plotkin, Matija Pretnar

      • Twenty-third Annual IEEE Symposium on Logic in Computer Science, LICS 2008
      • DOI

  20. 2005

    1. Sintetična topologija

      Matija Pretnar

      • Univerza v Ljubljani
      • Fakultetna Prešernova nagrada