Posts in the year 2017
Spartan type theory
- 11 December 2017
- Type theory, Talks, Tutorial
The slides from the talk “Spartan type theory”, given at the School and Workshop on Univalent Mathematics.
Download slides with speaker notes: Spartan Type Theory [PDF]→ continue reading (7 comments)
A modular formalization of type theory in Coq
- 29 May 2017
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]
Two PhD positions in Ljubljana starting October 2017
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 or Matija Pretnar, depending on their primary interest. Please include a short CV, academic record, and a statement of interest.→ continue reading