In 2013 I gave a talk about constructive mathematics “Five stages of accepting constructive mathematics” (video) at the Institute for Advanced Study. I turned the talk into a paper, polished it up a bit, added things here and there, and finally it has now been published in the Bulletin of the American Mathematical Society. It is not quite a survey paper, but it is not very technical either. I hope you will enjoy reading it.

Free access to the paper:  Five stages of accepting constructive mathematics (PDF)

→ continue reading (12 comments)

It is my pleasure to announce the new and improved Programming languages Zoo, a potpourri of miniature but fully functioning programming language implementations. The new zoo has a decent web site, it is now hosted on GitHub, and the source code was cleaned up. Many thanks to Matija Pretnar for all the work.

The purpose of the zoo is to demonstrate design and implementation techniques, from dirty practical details to lofty theoretical considerations:

• functional, declarative, object-oriented, and procedural languages
• source code parsing with a parser generator
• recording of source code positions
• pretty-printing of values
• interactive shell (REPL) and non-interactive file processing
• untyped, statically and dynamically typed languages
• type checking and type inference
• subtyping, parametric polymorphism, and other kinds of type systems
• eager and lazy evaluation strategies
• recursive definitions
• exceptions
• interpreters and compilers
• abstract machine

There is still a lot of room for improvement and new languages. Contributions are welcome!

 

→ continue reading

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)