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

Logics and semantics of programs, mechanized proofs, combining tests and proofs, intuitionistic type theory, applications of category theory to programming.

Activities 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. Organizer.
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. Participant.
Minisymposium on Type Theory and Foundations, Uppsala, 15 January 2009. Lecture on Program Testing and Constructive Validity.
Public defense of PhD thesis of Johan Granström, Reference and Computation in Intuitionistic Type Theory, Uppsala 16 January 2009. Faculty opponent.
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, 1-6 March, 2009. Invited lecturer.
Programming, Types, and Languages. A symposium in connection with Bengt Nordström's 60th birthday. 19 March 2009. Organizer.
Midlands Graduate School in the Foundations of Computer Science, Leicester, UK, 30 March - 3 April, 2009. Invited lecturer.
Philosophy and Foundations of Mathematics: Ontological and Epistemological Aspects, Uppsala, 5-8 May 2009. Member of organizing and programme committee.
Workshop on Normalization by Evaluation, Los Angeles, Ca, 15 August 2009, co-located with LICS 2009. Keynote speaker.
22nd Conference on Theorem Proving in Higher Order Logics (TPHOLs), Munich, 17-20 August 2009. Member of programme committee.
British Logic Colloquium 2009. Swansea, UK, 3 - 5 September 2009. Invited speaker.
Research meeting for EPSRC-project on Induction-Recursion. Swansea, UK, 5 - 6 September 2009.
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.
10th Agda Implementors' Meeting, Göteborg, 14-18 September 2009. Organizer.
11th Agda Implementors' Meeting, Awaji Island, Japan, 24-30 March 2010.
ICALP 2010, 37th International Colloquium on Automata, Languages and Programming, Bordeaux, 5-12 July 2010. Member of programme committee.
ICFP 2010 : The 15th ACM SIGPLAN International Conference on Functional Programming, Baltimore, Maryland, 27-29 September 2010. Member of programme committee.

Some papers and slides from talks

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 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.

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 director of the Master's Programme in Computer Science - Algorithms, Languages, and Logic. 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.