Peter Dybjer Professor of Computing Science Department of Computer Science and Engineering Chalmers University of Technology S-412 96 Göteborg, Sweden Email: peterd@chalmers ... Phone: +46 31 772 1035

Research interests

• Reading material for my lectures on Intuitionistic Type Theory for the Summer School on Types, Sets and Constructions, Hausdorff Research Institute for Mathematics, Bonn, 3 - 9 May, 2018.
• An article about Intuitionistic Type Theory (written together with Erik Palmgren) in the Stanford Encyclopedia of Philosophy.
• Editor of the Bulletin of Symbolic Logic.
• A Note on Generalized Algebraic Theories and Categories with Families (with Marc Bezem, Thierry Coquand, and Martin Escardo), arXiv:2012.08370, December 2020.

Activities

2019

• Fellow at the Centre for Advanced Studies at the Norwegian Academy of Science and Letters, Oslo, January - June 2019. Programme Homotopy Type Theory and Univalent Foundations.
• TYPES 2019, Lecture on Categories with Families, Unityped, Simply Typed, Dependently Typed, TYPES 2019, Oslo, June 2019.
• Member of the Programme Committee for 4th International Conference on Foundational Structures in Computation and Deduction, Dortmund, 24-30 June.
• Lecture on Categories with Families: Unityped, Simply Typed, and Dependently Typed at the Workshop on Foundations and Applications of Univalent Mathematics, Herrsching, Germany, 18-20 December 2019.

2020

• Member of the Programme Committee for 5th International Conference on Foundational Structures in Computation and Deduction, Paris, 29 June- 5 July, 2020.
• Invited speaker for the workshop on Logics and Calculability at the VI Congreso LatinoAmericano de Matematica, Montevideo, 20 - 24 July 2020 (postponed).
• Invited speaker at the HoTT/UF mini-symposium during the 8th European Congress of Mathematics, Portoroz, Slovenia, 5 - 11 July 2020 (postponed).
• Talk on Erik Palmgren and the Higher Infinite in Type Theory at the Memorial Conference for Erik Palmgren, 1963–2019, online, 19-21 November 2020.

Earlier

Some papers and slides from talks

• Dependent type theory and proof assistants - introductions and overviews
• Inductive and inductive-recursive definitions in type theory
• Universes
• Higher inductive types
• Generic programming
• Normalization by evaluation
• Combining testing and proving
• Logic of general recursive functional programs
• Category theory and type theory
• Game semantics
• Strictness analysis
• Meaning explanations for intuitionistic type theory
• Material for the 2015 Oregon Programming Languages Summer School

Courses in international schools for postgraduate students

• Oregon Programming Languages Summer School, Eugene, Oregon, 15 - 27 June 2015. Lectures on Inductive and Inductive-Recursive Definitions in Type Theory.
• Midlands Graduate School in the Foundations of Computer Science, Leicester, UK, 30 March - 3 April, 2009. Lectures on Normalization by Evaluation.
• 14th Estonian Winter School in Computer Science (EWSCS), Palmse, Estonia, 1-6 March, 2009. Lectures on Normalization by Evaluation.
• University of Warsaw, open lectures for PhD students in computer science, 18-19 January 2008. Lectures on Normalization by Evaluation.
• Summer School on Language Engineering and Rigorous Software Development (LerNet), Piriapolis, Uruguay, February - March 2008. Lectures on Dependent Types at Work (with Ana Bove),
• TYPES Summer School, Göteborg, August 2005. Lectures on Inductive and Recursive Definitions in Constructive Type Theory,
• International Winter School on Semantics and Applications, Montevideo, Uruguay, July 2003. Lectures on Type Systems.
• TYPES Summer School, Giens, France, September 2002. Lectures on Dependent Types in Programming,
• Applied Semantics. International Summer School, Caminha, Portugal, September 2000. Lectures on Normalization and Partial Evaluation.
• European Summer School on Logic, Language, and Information (ESSLLI), Copenhagen, August 1994. Lectures on Inductive Definitions and Type Theory.
• Logic for IT Summer School, Isle of Thorns, August 1988. Lectures on Martin-Löf type theory.

Graduate education at Chalmers

• I initiated and directed the Master's Programme in Computer Science - Algorithms, Languages, and Logic 2006 - 2010.
• Types for Programs and Proofs, Master's course.

Disclaimer