Programming with Algebraic Effects and Handlers

With Matija Pretnar.

Abstract: Eff is a programming language based on the algebraic approach to computational effects, in which effects are viewed as algebraic operations and effect handlers as homomorphisms from free algebras. Eff supports first-class effects and handlers through which we may easily define new computational effects, seamlessly combine existing ones, and handle them in novel [...]

On the Bourbaki-Witt Principle in Toposes

With Peter LeFanu Lumsdaine.

Abstract: The Bourbaki-Witt principle states that any progressive map on a chain-complete poset has a fixed point above every point. It is provable classically, but not intuitionistically. We study this and related principles in an intuitionistic setting. Among other things, we show that Bourbaki-Witt fails exactly when the trichotomous ordinals form a set, but does not [...]

Constructive gem: an injection from Baire space to natural numbers

I am not sure whether to call this one a constructive gem or stone. I suppose it is a matter of personal taste. I think it is a gem, albeit a very unusual one: there is a topos in which $\mathbb{N}^\mathbb{N}$ can be embedded into $\mathbb{N}$. Continue reading Constructive gem: an injection from Baire space to natural numbers

Stone Duality for Skew Boolean Algebras with Intersections

With Karin Cvetko Vah.

For the last two months or so I got “distracted” by a topic which is not properly my core interest, namely non-commutative algebra. It was very strange at first, but now that I got used to non-commutative lattices (yes, there is such a thing) it’s kind of fun. Anyhow, Karin Cvetko Vah and [...]

Canonical Effective Subalgebras of Classical Algebras as Constructive Metric Completions

Jens Blanck and I presented a paper at Computability and Complexity in Analysis 2009 with a complicated title (I like complicated titles):

Canonical Effective Subalgebras of Classical Algebras as Constructive Metric Completions

which has been published in Volume 16, Issue 18 of the Journal of Universal Computer Science. I usually just post the abstract, but this time I would like to explain the general idea informally, the way one can do it on a blog. But first, here is the abstract:

Abstract: We prove general theorems about unique existence of effective subalgebras of classical algebras. The theorems are consequences of standard facts about completions of metric spaces within the framework of constructive mathematics, suitably interpreted in realizability models. We work with general realizability models rather than with a particular model of computation. Consequently, all the results are applicable in various established schools of computability, such as type 1 and type 2 effectivity, domain representations, equilogical spaces, and others.

Download paper: effalg.pdf or directly from JUCS

Metric Spaces in Synthetic Topology

With Davorin Lešnik.

Abstract: We investigate the relationship between the synthetic approach to topology, in which every set is equipped with an intrinsic topology, and constructive theory of metric spaces. We relate the synthetic notion of compactness of Cantor space to Brouwer’s Fan Principle. We show that the intrinsic and metric topologies of complete separable metric spaces [...]

On the Failure of Fixed-point Theorems for Chain-complete Lattices in the Effective Topos

Abstract: In the effective topos there exists a chain-complete distributive lattice with a monotone and progressive endomap which does not have a fixed point. Consequently, the Bourbaki-Witt theorem and Tarskiâ€™s fixed-point theorem for chain-complete lattices do not have constructive (topos-valid) proofs.

Download: fixed-points.pdf

Published in: Theoretical Computer Science Volume 430, 27 April 2012, Pages 43–50. Mathematical Foundations of [...]

A constructive theory of domains suitable for implementation

With Iztok Kavkler.

Abstract: We formulate a predicative, constructive theory of continuous domains whose realizability interpretation gives a practical implementation of continuous Ï‰-chain complete posets and continuous maps between them. We apply the theory to implementation of the interval domain and exact real [...]

Implementing real numbers with RZ

With Iztok Kavkler.

Abstract: RZ is a tool which translates axiomatizations of mathematical structures to program speciï¬cations using the realizability interpretation of logic. This helps programmers correctly implement data structures for computable mathematics. RZ does not prescribe a particular method of implementation, but allows programmers to write efficient code by hand, or to extract trusted code from [...]

RZ: a tool for bringing constructive and computable mathematics closer to programming practice

With Chris Stone.

Abstract:
Realizability theory is not only a fundamental tool in logic and computability, but also has direct application to the design and implementation of programs: it can produce interfaces for the data structure corresponding to a mathematical theory. Our tool, called RZ, serves as a bridge between the worlds of constructive mathematics and programming. By [...]

König's Lemma and the Kleene Tree

For the benefit of the topology seminar audience at the math department of University of Ljubljana, I have written a self-contained explanation of the Kleene tree, which is an interesting object in computability theory. For the benefit of the rest of the planet, I am publishing it here.
Continue reading König’s Lemma and the Kleene Tree

Realizability as the Connection between Computable and Constructive Mathematics

Lecture notes for my tutorial at Computability and Complexity in Analysis 2005, Kyoto. [...]

The Dedekind Reals in Abstract Stone Duality

With Paul Taylor.

Abstract: Abstract Stone Duality (ASD) is an approach to topology that provides an abstract and conceptually satisfying account of topological spaces. The calculus of ASD reveals the computational content of various topological notions and suggests how to compute with them. The distinguishing feature of ASD is a direct axiomatisation in terms of spaces and [...]

Blog as a repository for research papers

So I decided to put all my research papers on the blog. [...]

First Steps in Synthetic Computability Theory (MFPS XXI)

Abstract: Computability theory, which investigates computable functions and computable sets, lies at the foundation of computer science. Its classical presentations usually involve a fair amount of Gödel encodings which sometime obscure ingenious arguments. Consequently, there have been a number of presentations of computability theory that aimed to present the subject in an abstract and conceptually pleasing [...]

Specifications via Realizability (CLASE 2005)

How to build specifications for abstract data types using realizability [...]

Two Constructive Embedding-Extension Theorems with Applications to Continuity Principles and to Banach-Mazur Computability

With Alex Simpson.

Abstract: We prove two embedding and extension theorems in the context of the constructive theory of metric spaces. The first states that Cantor space embeds in any inhabited complete separable metric space (CSM) without isolated points, X, in such a way that every sequentially continuous function from Cantor space to ZZ extends to a [...]

Propositions as [Types]

With Steve Awodey.

Abstract: Image factorizations in regular categories are stable under pullbacks, so they model a natural modal operator in dependent type theory. This unary type constructor [A] has turned up previously in a syntactic form as a way of erasing computational content, and formalizing a notion of proof irrelevance. Indeed, semantically, the notion of [...]

A Relationship between Equilogical Spaces and Type Two Effectivity

Abstract: In this paper I compare two well studied approaches to topological semantics—the domain-theoretic approach, exemplified by the category of countably based equilogical spaces, omegaEqu, and Type Two Effectivity, exemplified by the category of Baire space representations, Rep(B). These two categories are both locally cartesian closed extensions of countably based T_0-spaces. A natural question to ask [...]

Equilogical Spaces

With Lars Birkedal and Dana Scott.

Abstract: It is well known that one can build models of full higher-order dependent type theory (also called the calculus of constructions) using partial equivalence relations (PERs) and assemblies over a partial combinatory algebra (PCA). But the idea of categories of PERs and ERs (total equivalence relations) can be applied [...]

Comparing Functional Paradigms for Exact Real-number Computation

With Alex Simpson and MartÃ­n EscardÃ³.

Abstract: We compare the definability of total functionals over the reals in two functional-programming approaches to exact real-number computation: the extensional approach, in which one has an abstract datatype of real numbers; and the intensional approach, in which one encodes real numbers using ordinary datatypes. We show that [...]

Sheaf Toposes for Realizability

with Steve Awodey.

Abstract: We compare realizability models over partial combinatory algebras by embedding them into sheaf toposes. We then use the machinery of Grothendieck toposes and geometric morphisms to study the relationship between realizability models over different partial combinatory algebras. This research is part of the Logic of Types and Computation project at Carnegie Mellon [...]

The Realizability Approach to Computable Analysis and Topology

This is my Ph.D. dissertation, which I forgot to post on this blog. So I am doing it now. [...]

Continuous Functionals of Dependent Types and Equilogical Spaces

with Lars Birkedal.

Abstract: We show that dependent sums and dependent products of continuous parametrizations on domains with dense, codense, and natural totalities agree with dependent sums and dependent products in equilogical spaces, and thus also in the realizability topos RT(P(NN)).

Published in: In Proceedings of Computer Science Logic 2000, Lecture Notes in Computer Science, Vol. 1862, Editors: [...]

Mixed multibasic and hypergeometric Gosper-type algorithms

with Marko PetkovÅ¡ek.

Abstract: Gosper’s summation algorithm finds a hypergeometric closed form of an indefinite sum of hypergeometric terms, if such a closed form exists. We extend the algorithm to the case when the terms are simultaneously hypergeometric and multibasic hypergeometric. We also provide algorithms for finding polynomial as well as hypergeometric solutions to recurrences in the [...]

Analytica — An Experiment in Combining Theorem Proving and Symbolic Computation

with Edmund Clarke and Xudong Zhao.

Abstract: Analytica is an automatic theorem prover for theorems in elementary analysis. The prover is written in Mathematica language and runs in the Mathematica environment. The goal of the project is to use a powerful symbolic computation system to prove theorems that are beyond the scope of previous automatic theorem provers. [...]