Search

• < Previous
• 1
• Next >

---

An Effect System for Algebraic Effects and Handlers

Andrej Bauer ; Matija Pretnar.

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 respect to it. Then we give a domain-theoretic&nbsp;[&hellip;]

---

Every metric space is separable in function realizability

Andrej Bauer ; Andrew Swan.

We first show that in the function realizability topos every metric space is separable, and every object with decidable equality is countable. More generally, working with synthetic topology, every $T_0$-space is separable and every discrete space is countable. It follows that intuitionistic logic&nbsp;[&hellip;]

---

An extensible equality checking algorithm for dependent type theories

Andrej Bauer ; Anja Petković Komel.

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, where both kinds of rules are defined using the&nbsp;[&hellip;]

---

Instance reducibility and Weihrauch degrees

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 constructive mathematics (formal Church's thesis,&nbsp;[&hellip;]

---