Peter Dybjer Professor of Computing Science Address: 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

Events in 2008 and 2009

• 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, 25 February - 1 March 2008. Lectures on Dependent Types at Work.
• National University of Cordoba, Argentina, 3 March 2008. Lecture on Normalization by Evaluation.
• 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.
• International Symposium on Functional and Logic Programming (FLOPS 2008), Ise, Japan, 14-16 April 2008. Invited speaker.
• National Institute of Informatics, Tokyo, 21 April 2008. Lecture on Normalization by Evaluation.
• 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.
• 8th Agda Implementors' Meeting, Göteborg, 29 May - 4 June 2008.
• 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.
• University of Cambridge, Computer Laboratory, 27 June 2008. Seminar on The Interpretation of Intuitionistic Type Theory - an Intuitionistic Perspective.
• Mathematics of Program Construction (MPC '08), Marseille (Luminy), France, 15-18 July 2008. Member of the programme committee.
• 5th IFIP International Conference on Theoretical Computer Science (TCS-2008), Milano, 7-10 September 2008. Member of the programme committee.
• 9th Agda Implementors' Meeting, Sendai, Japan, 27 November - 3 December, 2008.
• ACM SIGPLAN Workshop on Types in Language Design and Implementation affiliated with POPL 2009 21-23 January, 2009, in Savannah, Georgia. Member of the programme committe.
• 14th Estonian Winter School in Computer Science (EWSCS), Palmse, Estonia, March 1-6, 2009. Lecturer.
• Philosophy and Foundations of Mathematics, Stockholm, 5-8 May 2009. Member of organizing and programme committee.
• 22nd Conference on Theorem Proving in Higher Order Logics (TPHOLs), Munich, 17-20 August 2009. Member of programme committee.

Some papers and slides from talks

• Dependent type theory and proof assistants - introductions and overviews
• Inductive and inductive-recursive definitions in type theory
• Generic programming
• Normalization by evaluation
• Combining testing and proving
• Logic of functional programs
• Category theory and type theory
• Strictness analysis

Courses in summer schools:

• Dependent Types at Work (with Ana Bove), Summer School on Language Engineering and Rigorous Software Development (LerNet), Piriapolis, Uruguay, February - March 2008.
• Inductive and Recursive Definitions in Constructive Type Theory, TYPES Summer School, Göteborg, August 2005.
• Type Systems, International Winter School on Semantics and Applications, Montevideo, Uruguay, July 2003.
• Dependent Types in Programming, TYPES Summer School, Giens, France, September 2002.
• Normalization and Partial Evaluation, Applied Semantics. International Summer School, Caminha, Portugal, September 2000.
• Inductive Definitions and Type Theory (with Thierry Coquand), lecture notes for ESSLLI, Copenhagen, August 1994.
• Martin-Löf type theory. Logic for IT Summer School, Isle of Thorns, August 1988.

Journals and conferences

Member of the steering committee of Programming Languages Meet Program Verification.

Projects

The Programming Logic Group at Chalmers.

TYPES - Computer-Assisted Reasoning Based on Type Theory (ESPRIT Working Group)

Agda - an Interactive Proof Editor joint project with the Research Centre for Verification and Semantics at the National Institute of Advanced Industrial Science and Technology (AIST), Japan.

APPSEM II - Applied Semantics (ESPRIT Working Group 2002-2006)

Cover - Combining Verification Methods in Software Development (SSF-project 2002-2005)

Master's Programme

I am the coordinator of the new Master's Programme in Foundations of Computing - Algorithms and Logic which began in the autumn of 2007.

Courses and notes:

• Types for Programs and Proofs, MSc course.
• Datastrukturer, BSc course.
• Dependent Type Theory, PhD course.
• Computability via PCF lecture notes for the course Foundations of Computation.

Disclaimer

To Chalmers CS Dept. Welcome page.