A tutorial presented at the *Mathematical Foundations of Programming Semantics XXIII* Tutorial Day.

Continue reading Synthetic Computability (MFPS XXIII Tutorial)

# Category Archives: Tutorial

# On a proof of Cantor’s theorem

The famous theorem by Cantor states that the cardinality of a powerset $P(A)$ is larger than the cardinality of $A$. There are several equivalent formulations, and the one I want to consider is

Theorem (Cantor):There is no onto map $A \to P(A)$.

In this post I would like to analyze the usual proof of Cantor’s theorem and present an insightful reformulation of it which has applications outside set theory. Continue reading On a proof of Cantor’s theorem

# 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

# Sometimes all functions are continuous

You may have heard at times that there are mathematicians who think that *all* functions are continuous. One way of explaining this is to show that all *computable* functions are continuous. The point not appreciated by many (even experts) is that the truth of this claim depends on what programming language we use.

Continue reading Sometimes all functions are continuous

# Proof hacking

I recently lectured at an EST training workshop in Fischbachau, Germany. There were also a number of student talks, one of which was given by Luca Chiarabini from Munich. He talked about extraction of programs from proofs, using (a variant of) Curry-Howard isomorphism, also known as *propositions-as-types*. He had some very interesting ideas which were obviously related to old programming tricks, but he approached them from the logical point of view, rather than the programmer’s point of view. It got me thinking about how to write certain recursive programs as proofs. Since it is a nice application of program extraction, I want to share it with you here.