Peter Dybjer

Professor, Computing Science Department, Chalmers University of Technology, S-412 96 Göteborg, Sweden.

• Email: peterd@cs.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.
• 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.
• 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, Tsukuba, Japan, November 2008.
• ACM SIGPLAN Workshop on Types in Language Design and Implementation, to be co-located with POPL 2009 21-23 January, 2009, in Savannah, Georgia. Member of the programme committe.

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:

• 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'94, Copenhagen.

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 beginning in the autumn of 2007.

Courses and notes:

• Datastrukturer
• Dependent Type Theory
• Computability via PCF lecture notes for the course Foundations of Computation.

Disclaimer

To Chalmers CS Dept. Welcome page.