Matija Pretnar: Logika z lokalnimi algebrajskimi teorijami
Datum objave: 31. 7. 2018
Seminar za temelje matematike in teoretično računalništvo
Sreda, 1. 8. 2018, ob 11:15 v predavalnici 3.07 na Jadranski 21
Pozor: dobimo se ob nestandardnem času, v sredo 1. 8. 2018 ob 11:15 v 3.07!
Attention: we meet at a non-standard time on Wednesday, 1. 8. 2018 at 11:15 in 3.07!
Povzetek: Osnovna predpostavka algebrajskih učinkov je, da lahko učinke opišemo z algebrajsko teorijo, sestavljeno iz množice operacij ter enačb med njimi. Ker pa mnogo računsko zanimivih prestreznikov algebrajskih učinkov tem enačbam ne zadošča, običajno predpostavimo trivialno algebrajsko teorijo. Na seminarju bom predstavil pristop, v katerem lokalno veljavne enačbe zapišemo v tipih. (skupno delo z Žigo Lukšičem)
Abstract: 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 locally respected equations may be encoded in computation types. (joint work with Žiga Lukšič)
