Mathematics and Computation

I have participated in a couple of lengthy discussions about formal proofs. I realized that an old misconception is creeping in. Let me expose it.

→ continue reading (24 comments)

Mike Shulman just wrote a very nice blog post on what is a formal proof. I much agree with what he says, but I would like to offer my own perspective. I started writing it as a comment to Mike's post and then realized that it is too long, and that I would like to have it recorded independently as well. Please read Mike's blog post first.

→ continue reading (55 comments)

This post is going to draw an angry Haskell mob, but I just have to say it out loud: I have never seen a definition of the so-called category Hask and I do not actually believe there is one until someone does some serious work.

→ continue reading (66 comments)

I am about to give an invited talk at the  Workshop on Categorical Logic and Univalent Foundations 2016 in Leeds, UK. It's a charming workshop that I am enjoing a great deal. Here are the slides of my talk, with speaker notes, as well as the Andromeda examples that I am planning to cover.

• Slides: AndromedaProofAssistant.pdf
  
• Andromeda files: nat.m31, universe.m31

→ continue reading (30 comments)

I am about to give an invited talk at the Computability and Complexity in Analysis 2016 conference (yes, I am in the south of Portugal, surrounded by loud English tourists, but we are working here, in a basement no less). Here are the slides, with extensive speaker notes, comment and questions are welcome.

Slides: hott-reals-cca2016.pdf

→ continue reading (6 comments)

In a paper accepted at POPL 2016 Matt Brown and Jens Palsberg constructed a self-interpreter for System $F_\omega$, a strongly normalizing typed $\lambda$-calculus. This came as a bit of a surprise as it is “common knowledge” that total programming languages do not have self-interpreters.

Thinking about what they did I realized that their conditions allow a self-interpreter for practically any total language expressive enough to encode numbers and pairs. In the PDF note accompanying this post I give such a self-interpreter for Gödel's System T, the weakest such calculus. It is clear from the construction that I abused the definition given by Brown and Palsberg. Their self-interpreter has good structural properties which mine obviously lacks. So what we really need is a better definition of self-interpreters, one that captures the desired structural properties. Frank Pfenning and Peter Lee called such properties reflexivity, but only at an informal level. Can someone suggest a good definition?

Note: self-interpreter-for-T.pdf

→ continue reading (11 comments)

A postdoc position in the Effmath research project is available at the University of Ljubljana, Faculty of Mathematics and Physics. The precise topic is flexible, but should generally be aligned with the project (see project description). Possible topics include:

•  reasoning about computational effects
•  implementation of computational effects
• proof assistants and formalization of mathematics

The candidate should have a PhD degree in mathematics or computer science, with background knowledge relevant to the project area. The position is available for a period of one year with possibility of extension, preferably starting in early 2016. No knowledge of the Slovene language is required.

The candidates should contact Andrej Bauer by email as soon as possible, but no later than January 8th 2016. Please include a short CV and a statement of interest.

→ continue reading

My student Marko Koležnik is about to finish his Master's degree in Mathematics at the University of Ljubljana. He implemented Agda Writer, a graphical user interface  for the Agda proof assistant on the OS X platform. As he puts it, the main advantage of Agda Writer is no Emacs, but the list of cool features is a bit longer:

• bundled Agda: it comes with preinstalled Agda so there is zero installation effort (of course, you can use your own Agda as well).
• UTF-8 keyboard shortcuts: it is super-easy to enter UTF-8 characters by typing their LaTeX names, just like in Emacs. It trumps Emacs by converting ASCII arrows to their UTF8 equivalents on the fly. In the preferences you can customize the long list of shortcuts to your liking.
• the usual features expected on OS X are all there: auto-completion, clickable error messages and goals, etc.

Agda Writer is open source. Everybody is welcome to help out and participate on the Agda Writer repository.

Who is Agda Writer for? Obviously for students, mathematicians, and other potential users who were not born with Emacs hard-wired into their brains. It is great for teaching Agda as you do not have to spend two weeks explaining Emacs. The only drawback is that it is limited to OS X. Someone should write equivalent Windows and Linux applications. Then perhaps proof assistants will have a chance of being more widely adopted.

→ continue reading (5 comments)

This is officially a rant and should be read as such.

Here is my pet peeve: theoretical computer scientists misuse the word “provably”. Stop it. Stop it!

→ continue reading (10 comments)

I have not written a blog post in a while, so I decided to write up a short observation about truth values in intuitionistic logic which sometimes seems a bit puzzling.

Let $\Omega$ be the set of truth values (in Coq this would be the setoid whose underlying type is $\mathsf{Prop}$ and equality is equivalence $\leftrightarrow$, while in HoTT it is the h-propostions). Call a truth value $p : \Omega$ intermediate if it is neither true nor false, i.e., $p \neq \bot$ and $p \neq \top$. Such a “third” truth value $p$ is proscribed by excluded middle.

The puzzle is to explain how the following two facts fit together:

1. “There is no intermediate truth value” is an intuitionistic theorem.
2. There are models of intuitionistic logic with many truth values.

→ continue reading (6 comments)