Here are the slides for the talk I just gave at TYPES 2017 in Budapest. It is joint work with Philipp Haselwarter and Théo Winterhalter. The abstract for the talk is available online.
It describes a complete formalization of dependent type theory which allows you to turn various features of type theory on and off, and it proves several basic formal theorems.
GitHub repository: formal-type-theory
Slides: TYPES 2017 – A modular formalization of type theory in Coq [PDF]
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
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.
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 Provably considered harmful
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.
Recently I reviewed a paper in which most proofs were done in a proof assistant. Yes, the machine guaranteed that the proofs were correct, but I still had to make sure that the authors correctly formulated their definitions and theorems, that the code did not contain hidden assumptions, that there were no unfinished proofs, and so on.
In a typical situation an author submits a paper accompanied with some source code which contains the formalized parts of the work. Sometimes the code is enclosed with the paper, and sometimes it is available for download somewhere. It is easy to ignore the code! The journal finds it difficult to archive the code, the editor naturally focuses on the paper itself, the reviewer trusts the authors and the proof assistant, and the authors are tempted not to mention dirty little secrets about their code. If the proponents of formalized mathematics want to avert a disaster that could destroy their efforts in a single blow, they must adopt a set of rules that will ensure high standards. There is much more to trusting a piece of formalized mathematics than just running it through a proof checker.
Continue reading How to review formalized mathematics
The HoTT book is finished!
Since spring, and even before that, I have participated in a great collaborative effort on writing a book on Homotopy Type Theory. It is finally finished and ready for public consumption. You can get the book freely at http://homotopytypetheory.org/book/. Mike Shulman has written about the contents of the book, so I am not going to repeat that here. Instead, I would like to comment on the socio-technological aspects of making the book, and in particular about what we learned from open-source community about collaborative research.
Continue reading The HoTT book
It seems to me that people think I am a constructive mathematician, or worse a constructivist (a word which carries a certain amount of philosophical stigma). Let me be perfectly clear: it is not decidable whether I am a constructive mathematician.
Continue reading Am I a constructive mathematician?
This is an advertisement for two great meetings we are organizing in Ljubljana from June 15 to June 20, 2012:
There are many reasons why you should come: Ljubljana is lovely in June, with many cafes and restaurants on the Ljubljanica river bank, we have a very interesting programme, and when will you next be able to attend a meeting in which the keynote speakers are Per Martin-Löf, Ieke Moerdijk and Vladimir Voevodsky? Not to mention that the schedule is fairly light, everything is within walking distance, and we are organizing dinners at some excellent restaurants.
If you decide to come, make sure to book a hotel early and register today!
I remember how hard it was to assimilate category theory when I was a student. A beginning student on math.stackexchange.com is asking for a solution to a basic lemma about pullbacks. It really is the sort of thing one should do by oneself. Nevertheless, here it is, in gory details.