• View
• Edit
• History
• Print

ProgrammingLanguageSupportForACourseOnTypeSystems

Programming language support for a course on Type Systems

A course on type systems for programming languages covers both a number of formal systems (computation rules, type systems) and algorithms (evaluators, simplifiers, type checkers). It is very useful for a student to experiment with these notions by implementing them in a programming language. Functional languages are suitable for implementing these algorithms. But if the functional language is equipped with dependent types, then the type system can be used also to specify computation rules and type systems, and thus to express correctness properties of the algorithms.

In this project the task is to develop such support for the course on Types for Programs and Proofs - an advanced course at Chalmers. This course uses the book "Types and Programming Languages" by Benjamin Pierce: http://www.cis.upenn.edu/~bcpierce/tapl/index.html .

The task is to use the programming language Agda developed at Chalmers for implementing a number of notions covered by Pierce. In Pierce's course, given at the University of Pennsylvania, the Coq system is used for a similar purpose. The thesis is expected to contain a comparison between Agda and Coq for this purpose.

contact person: Peter Dybjer