The troublesome reflection rule (TYPES 2015 slides)

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].

Another PhD position in Ljubljana

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.

A HoTT PhD position in Ljubljana

I am looking for a PhD student in mathematics. Full tuition & stipend will be provided for a period of three years, which is also the official length of the programme. The topic of research is somewhat flexible and varies from constructive models of homotopy type theory to development of a programming language for a proof assistant based on dependent type theory, see the short summary of the Effmath project for a more detailed description.

The candidate should have as many of the following desiderata as possible, and at the very least a master’s degree (or an equivalent one):

  1. a master’s degree in mathematics, with good knowledge of computer science
  2. a master’s degree in computer science, with good knowledge of mathematics
  3. experience with functional programming
  4. experience with proof assistants
  5. familiarity with homotopy type theory

The student will officially enrol in October 2015 at the University of Ljubljana. No knowledge of Slovene is required. However, it is possible, and even desirable, to start with the actual work (and stipend) earlier, as soon as in the spring of 2015. The candidates should contact me by email as soon as possible. Please include a short CV and a statement of interest.

Update 2015-03-28: the position has been taken.

TEDx “Zeroes”

I spoke at TEDx University of Ljubljana. The topic was how programming influences various aspects of life. I showed the audence how a bit of simple programming can reveal the beauty of mathematics. Taking John Baez’s The Bauty of Roots as an inspiration, I drew a very large image (20000 by 17500 pixels) of all roots of all polynomials of degree at most 26 whose coefficients are $-1$ or $1$. That’s 268.435.452 polynomials and 6.979.321.752 roots. It is two degrees more than Sam Derbyshire’s image,  so consider the race to be on! Who can give me 30 degrees?

Continue reading TEDx “Zeroes”

Reductions in computability theory from a constructive point of view

Here are the slides from my Logic Coloquium 2014 talk in Vienna. This is joint work with Kazuto Yoshimura from Japan Advanced Institute for Science and Technology.

Abstract: In constructive mathematics we often consider implications between non-constructive reasoning principles. For instance, it is well known that the Limited principle of omniscience implies that equality of real numbers is decidable. Most such reductions proceed by reducing an instance of the consequent to an instance of the antecedent. We may therefore define a notion of instance reducibility, which turns out to have a very rich structure. Even better, under Kleene’s function realizability interpretation instance reducibility corresponds to Weihrauch reducibility, while Kleene’s number realizability relates it to truth-table reducibility. We may also ask about a constructive treatment of other reducibilities in computability theory. I shall discuss how one can tackle Turing reducibility constructively via Kleene’s number realizability.

Slides with talk notes:  lc2014-slides-notes.pdf