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)

Here are the slides of my TYPES 2015 talk “The troublesome reflection rule” with fairly detailed presenter notes. The meeting is  taking place in Tallinn, Estonia – a very cool country in many senses (it's not quite spring yet even though we're in the second half of May, and it's the country that gave us Skype).

Download slides: The troublesome reflection rule (TYPES 2015) [PDF].

→ continue reading (2 comments)

It is my pleasure to announce a second PhD position in Ljubljana!

A position is available for a PhD student at the University of Ljubljana in the general research area of modelling and reasoning about computational effects. The precise topic is somewhat flexible, and will be decided in discussion with the student. The PhD will be supervised by Alex Simpson who is Professor of Computer Science at the Faculty of Mathematics and Physics.

The position will be funded by the Effmath project (see project description). Full tuition & stipend will be provided.

The candidate should have a master's (or equivalent) degree in either mathematics or computer science, with background knowledge relevant to the project area. The student will officially enrol in October 2015 at the University of Ljubljana. No knowledge of the Slovene language is required.

The candidates should contact Alex.Simpson@fmf.uni-lj.si by email as soon as possible. Please include a short CV and a statement of interest.

→ continue reading