We are looking for two PhD students at the Faculty of Mathematics and Physics, University of Ljubljana. The programme starts in October 2017 and lasts three years. The positions will be fully funded (subject to approval by the funding agency). The candidates should have a Master’s degree in mathematics or computer science. No knowledge of Slovene is required.
The first PhD student will be advised by dr. Andrej Bauer. The topic of research is foundations of type theory. The candidate should have interest in mathematical aspects of type theory, and familiarity with proof assistants is desirable.
The second PhD student will be advised by dr. Matija Pretnar. The topic of research is the theory of programming languages with a focus on computational effects. The candidate should have interest in both the mathematical foundations and practical implementation of programming languages.
Candidates should send their applications as soon as possible, but no later than the end of April, to Andrej Bauer email@example.com or Matija Pretnar firstname.lastname@example.org, depending on their primary interest. Please include a short CV, academic record, and a statement of interest.
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)
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
- interpreters and compilers
- abstract machine
There is still a lot of room for improvement and new languages. Contributions are welcome!
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 Formal proofs are not just deduction steps
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 What is a formal proof?