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.