A hott thesis

Egbert Rijke successfully defended his master thesis in Utrecht a couple of weeks ago. He published it on the Homotopy type theory blog (here is a direct link to the PDF file (revised)). The thesis is well written and it contains several new results, but most importantly, it is a gentle yet non-trivial introduction to homotopy [...]

Eff 3.0

Matija and I are pleased to announce a new major release of the eff programming language.

In the last year or so eff has matured considerably:

It now looks and feels like OCaml, so you won’t have to learn yet another syntax.
It has static typing with parametric polymorphism and type inference.
Eff now clearly separates three basic concepts: effect [...]

Bob Harper has a blog

Bob Harper of CMU, has recently started a blog, called Existential Type, about programming languages. He is a leading expert in Programming Languages. I remember being deeply inspired the first time I heard him talk. I was an incoming graduate student at CMU and he presented what the programming languages people at CMU did. His posts [...]

European workshop on computational effects

Alex Simpson, Matija Pretnar and I are organizing a workshop on computational effects. It will take place in Ljubljana on March 17th and 18th 2011. More information is available at the workshop [...]

An amazing functional

Martin Escardo and Paulo Oliva have been working on the selection monad and related functionals. The selection monad `S(X) = (X -> R) -> X` is a cousin of the continuation monad `C(X) = (X -> R) -> R` and it has a lot of useful and surprising applications. I recommend their recent paper “What Sequential Games, [...]

Hardware failure and phishing attacks

After more than 1300 days of uninterrupted service, the good old PC that served the blog started to spontaneously reboot every 4 minutes or so. It looks like a hardware failure. I moved the site to a temporary machine. I am seriously considering renting a private virtual server and just forget about buying my own hardware [...]

A comment about “Mathematical undecidability and quantum randomness” by Tomasz Paterek et al.

This is a short note pointing out that the recent paper on “Mathematical undecidability and quantum randomness” by Tomasz Paterek et al. is no black magic, and that the authors are well aware of it. Unfortunately the paper appeared on Slashdot and has since generated an infinite amount of quasi-mathematical discussions. Continue reading A comment about “Mathematical undecidability and quantum randomness” by Tomasz Paterek et al.

Exact real arithmetic in Haskell

HERA is an implementation of exact real arithmetic in Haskell using the approach by Andrej Bauer and Iztok Kavkler, see these and these slides. It uses the fast multiple precision floating point library MPFR. Download source, and see documentation and examples of usage at my home page.

[Note by Andrej: this is a guest post by Aleš [...]

Lambda calculus for real analysis by Paul Taylor

Paul Taylor has published a revised version of his `lambda`-calculus for real analysis. I recommend it to anyone who is interested in real analysis, be it a computer scientist, numerical analyst, or just a “true” analyst.

The first, second, and third time I talked to Paul I could not understand a word of what he was saying, and that’s not just because he is a native speaker of English English. I only began to “get it” when he visited me in Ljubljana. So I think it’s perhaps worth explaining a bit what this “`lambda`-calculus for real analysis” is about. Continue reading Lambda calculus for real analysis by Paul Taylor

International Mathematical Olympiad 2006

This year the International Mathematical Olympiad took place in Slovenia. I participated as one of the organizers (problem selection and coordination). It was probably one of the busiest and most exciting times of my life, Continue reading International Mathematical Olympiad 2006