Peter Dybjer

Professor of Computing Science
Head of the Division 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
Room: 6467, EDIT-building

Research interests

Logics and semantics of programs, intuitionistic type theory, proof assistants, applications of category theory to programming.

Some papers and slides from talks

Courses in international schools for postgraduate students

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.

Upcoming activities

Interactive Theorem Proving, Princeton, NJ, 13-15 August 2012. Member of programme committee
8th Scandinavian Logic Symposium, Roskilde, 20-21 August 2012. Member of programme committee
16th Agda Implementors Meeting, 3-9 October 2012, Copenhagen.
Institute for Advanced Study, Princeton, NJ, November - December 2012, Invited participant at the Special Year on Univalent Foundations.

Past activities

2012

CIAO workshop, Göteborg, 18-19 April 2012. Lecture on Combining Interactive and Automatic Reasoning in a First Order Theory of Functional Programs.
First Workshop on Automation in Proof Assistants (AIPA), Tallinn 31 March - 1 April. Participant.
15th International Conference on Foundations of Software Science and Computation Structures (FOSSACS), Tallinn, 27 - 30 March 2012. Contributed paper on Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs (with Ana Bove and Andres Sicard-Ramirez).
Examintion of PhD thesis of Miguel Pagano, Universidad National Cordoba, Argentina. 23 March 2012. Lecture on Tests, Games and Martin-Löf's meaning explanations for Intuitionistic Type Theory.
15th Agda Implementors Meeting, Fischbachau, 19-26 February 2012. Participant.
Logic and Interaction, CIRM, Luminy, Marseille. 5 - 17 February 2012. Invited lecture on Tests, Games and Martin-Löf's meaning explanations for Intuitionistic Type Theory.

2011

Workshop to Celebrate Peter Hancock's 60th Birthday, Glasgow 19 December 2011. Lecture: Thoughts on Martin-Löf’s Meaning Explanations.
Workshop on Proofs and Programs, 22 October 2012. Lecture on The Evolution of Inductive Definitions in Type Theory (a Retrospective) to Christine Paulin on the occasion of her honorary doctorate at Gothenburg University.
Workshop on Dependently Typed Programming, Shonan Village, Japan, 14-17 September 2011. Participant.
14th Agda Implementors Meeting, Shonan Village, Japan, 6 - 14 September 2011. Organizer.
Gunma University, Japan, 5 - 9 September. Lectures on Constructive Mathematics and Computer Programming - Some Background and on Program Testing and Constructive Validity.
Typed Lambda Calculus and Applications, Novi Sad, 1 - 3 June 2011. Contributed paper on The Biequivalence of Locally Cartesian Closed Categories and Martin-Lof Type Theory.
Invited lecture on Program Testing and Constructive Validity at the Oberseminar Logik und Sprachtheorie at the University of Tubingen, 8 February 2011.

2010

Examination of PhD thesis of Dag Hovland, Bergen, 16 December 2010.
ICFP 2010 : The 15th ACM SIGPLAN International Conference on Functional Programming, Baltimore, Maryland, 27-29 September 2010. Member of programme committee.
Workshop on Induction-recursion, Edinburgh 15-16 September, 2010. Lecture on the Biequivalence of Locally Cartesian Closed Categories and Martin-Lof Type Theory.
LFCS seminar, Edinburgh, 14 September, 2010. Lecture on Program Testing and Constructive Validity.
Uppsala-Stockholm Logic Seminar, 24 August, 2010. Lecture on the Biequivalence of Locally Cartesian Closed Categories and Martin-Lof Type Theory.
ICALP 2010, 37th International Colloquium on Automata, Languages and Programming, Bordeaux, 5-12 July 2010. Member of programme committee.
Examination of PhD thesis of Jacob Thamsborg, IT University of Copenhagen, 15 June, 2010.
Programming and Constructive Mathematics A symposium in connection with Jan Smith's 60th birthday. 31 May 2010. Organizer.

2009

10th Agda Implementors' Meeting, Göteborg, 14-18 September 2009. Organizer.
6th Workshop on Fixed Points in Computer Science, FICS 2009, Coimbra, Portugal, 12-13 September 2009. a satellite workshop to CSL 2009. Member of programme committee.
Research meeting for EPSRC-project on Induction-Recursion. Swansea, UK, 5 - 6 September 2009.
British Logic Colloquium 2009. Swansea, UK, 3 - 5 September 2009. Invited lecture on Program Testing and Constructive Validity.
22nd Conference on Theorem Proving in Higher Order Logics (TPHOLs), Munich, 17-20 August 2009. Member of programme committee.
Workshop on Normalization by Evaluation, Los Angeles, Ca, 15 August 2009, co-located with LICS 2009. Keynote speaker.
Philosophy and Foundations of Mathematics: Ontological and Epistemological Aspects, Uppsala, 5-8 May 2009. Member of organizing and programme committee.
Midlands Graduate School in the Foundations of Computer Science, Leicester, UK, 30 March - 3 April, 2009. Invited lecturer.
Programming, Types, and Languages. A symposium in connection with Bengt Nordström's 60th birthday. 19 March 2009. Organizer.
14th Estonian Winter School in Computer Science (EWSCS), Palmse, Estonia, 1-6 March, 2009. Invited lecturer.
POPL 2009 21-23 January, 2009, in Savannah, Georgia. Member of the programme committe.
ACM SIGPLAN Workshop on Types in Language Design and Implementation affiliated with
Public defense of PhD thesis of Johan Granström, Reference and Computation in Intuitionistic Type Theory, Uppsala 16 January 2009. Faculty opponent.
Minisymposium on Type Theory and Foundations, Uppsala, 15 January 2009. Lecture on Program Testing and Constructive Validity.

2008

9th Agda Implementors' Meeting, Sendai, Japan, 27 November - 3 December, 2008. Participant.
5th IFIP International Conference on Theoretical Computer Science (TCS-2008), Milano, 7-10 September 2008. Member of the programme committee.
Mathematics of Program Construction (MPC '08), Marseille (Luminy), France, 15-18 July 2008. Member of the programme committee.
University of Cambridge, Computer Laboratory, 27 June 2008. Seminar on The Interpretation of Intuitionistic Type Theory - an Intuitionistic Perspective.
International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08), 23 June 2008. Workshop affiliated with LICS-23 at Pittsburgh, Pennsylvania. Member of the programme committee.
8th Agda Implementors' Meeting, Göteborg, 29 May - 4 June 2008. Organizer.
Twenty-fourth Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIV), Philadelphia, PA, 21-25 May 2008. Invited speaker at the special session honoring Phil Scott on the occasion of his 60th birthday year.
National Institute of Informatics, Tokyo, 21 April 2008. Lecture on Normalization by Evaluation.
International Symposium on Functional and Logic Programming (FLOPS 2008), Ise, Japan, 14-16 April 2008. Invited speaker.
25 Year Anniversary of the Stockholm-Uppsala Logic Seminar. Symposium on Type Theory, Uppsala, 26 March 2008. Lecture on Category-Theoretic Approach to Type-checking Dependent Types.
National University of Cordoba, Argentina, 3 March 2008. Lecture on Normalization by Evaluation.
Summer School on Language Engineering and Rigorous Software Development (LerNet), Piriapolis, Uruguay, 25 February - 1 March 2008. Lectures on Dependent Types at Work.
University of Warsaw, open lectures for PhD students in computer science, 18-19 January 2008. Lectures on Normalization by evaluation.

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.

Journals and conferences

Member of the advisory board of the journal Higher Order and Symbolic Computation.
Member of the steering committees of Programming Languages Meet Program Verification and Fixed Points in Computer Science.

Disclaimer

To Chalmers CS Dept. Welcome page.