An extensible equality checking algorithm for dependent type theories

Autor: Andrej Bauer, Anja Petković Komel

Publikováno v: Logical Methods in Computer Science, Vol Volume 18, Issue 1 (2022)

We present a general and user-extensible equality checking algorithm that is applicable to a large class of type theories. The algorithm has a type-directed phase for applying extensionality rules and a normalization phase based on computation rules,

Externí odkaz: https://doaj.org/article/3ef4283d74d345c5abd135862b0d338f

An Effect System for Algebraic Effects and Handlers

Autor: Andrej Bauer, Matija Pretnar

Publikováno v: Logical Methods in Computer Science, Vol Volume 10, Issue 4 (2014)

We present an effect system for core Eff, a simplified variant of Eff, which is an ML-style programming language with first-class algebraic effects and handlers. We define an expressive effect system and prove safety of operational semantics with res

Externí odkaz: https://doaj.org/article/9b9f8b6a6c904965a5c8a54c57a95284

Instance reducibility and Weihrauch degrees

Autor: Andrej Bauer

We identify a notion of reducibility between predicates, called instance reducibility, which commonly appears in reverse constructive mathematics. The notion can be generally used to compare and classify various principles studied in reverse construc

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6afeab6b17323b2a7cbf050944b79dcf
http://arxiv.org/abs/2106.01734

Runners in Action

Autor: Andrej Bauer, Danel Ahman

Publikováno v: Programming Languages and Systems-29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings
Programming Languages and Systems
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Programming Languages and Systems
Programming Languages and Systems ISBN: 9783030449131

Runners of algebraic effects, also known as comodels, provide a mathematical model of resource management. We show that they also give rise to a programming concept that models top-level external resources, as well as allows programmers to modularly

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ab37bb6ba32fe17a66b489fcf250e4b4

On fixed-point theorems in synthetic computability

Autor: Andrej Bauer

Publikováno v: Tbilisi Math. J. 10, iss. 3 (2017), 167-181

Lawvere's fixed point theorem captures the essence of diagonalization arguments. Cantor's theorem, Gödel's incompleteness theorem, and Tarski's undefinability of truth are all instances of the contrapositive form of the theorem. It is harder to appl

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::32382d8a70a18751287f4932d3a98671
https://doi.org/10.1515/tmj-2017-0107