| Student || Paper || Presentation |
| Kasper || 10. Human-like error messages || September 27 |
| Mark || 7. Type Error Slices || September 29 |
| Thomas || 6. Typed Contracts || October 4 |
| Michiel || 5. Programming Environments || October 6 |
| John || 9. SEMINAL || October 11 |
| Sander || 1. Constraint Handling Rules (*) || October 13 |
| Gideon || 3. Tinkertype || October 18 |
| Eric || 4. Software Metrics || October 20 |
(*) Since paper 2 has not been assigned you are free to use this in your presentation (e.g., as a demo).
Below you can find a list of research papers for the (individual) presentations. Everyone should read the presented paper before
starts: you are expected to find and study a second paper yourself related to the paper assigned to you (other participants do not
have to read this). Your presentation should take 60 to 75 minutes, leaving some room for questions and discussion afterwards.
The audience is asked to write a short summary of the presented paper, and to evaluate the presentation (constructive advice and a mark).
These summaries and evaluations determine 15% of your overall grade (Feedback on Presentations
1. Constraint Handling Rules
Created by Thom Frühwirth in 1991, the CHR language has become a major specification and implementation language for constraint-based algorithms and applications. Algorithms are often specified using inference rules, rewrite rules, sequents, proof rules, or logical axioms that can be directly written in CHR. Based on first order predicate logic, the clean semantics of CHR facilitates non-trivial program analysis and transformation. About a dozen implementations of CHR exist in Prolog, Haskell, and Java. CHR is also available as
for online experimentation with more than 40 constraint solvers. More than 100 projects use CHR.
Chameleon is a Haskell-style language which supports several type extensions and improved type error diagnosis, and which is based on
Constraint Handling Rules.
Tinkertype is a framework for compact and modular description of formal systems.
An implementation in ML is available (with the paper).
4. Software Metrics
5. Programming Environments
More specifically, take a look at the Visual Haskell development environment, and at an
plugin for Haskell.
6. Typed Contracts
A robust software component fulfills a contract: it expects data satisfying a certain property and promises to return data satisfying another property. The object-oriented community uses the design-by-contract approach extensively. Proposals for language extensions that add contracts to higher-order functional programming have appeared recently. In this paper we propose an embedded domain-specific language for typed, higher-order and first-class contracts, which is both more expressive than previous proposals, and allows for better blame assignment. We take some first steps towards an algebra of contracts, and we show how to define a generic contract combinator for arbitrary algebraic data types. The contract language is implemented as a library in Haskell using the concept of generalised algebraic data types.
7. Type Error Slices
Previous methods have generally identified the location of a type error as a particular program point or the program subtree rooted at that point. We present an approach that identifies the location of a type error as a set of program points (a slice). On the one hand, type error slices contain enough program points to permit independent explanations of type errors (completeness). On the other hand, they contain only program points that are necessary for independent explanations (minimality). We discuss the advantages of complete and minimal type error slices over previous methods of presenting type errors. We describe algorithms for finding complete and minimal type error slices for implicitly typed higher-order languages like Standard ML.
8. Type Isomorphisms for Repairing Mistakes
This chapter introduces a novel system for generating type error messages which suggest ways of repairing mistakes. Both the theory behind this, and the implementation (as part of the MLj compiler) are described.
We present a new way to generate type-error messages in a polymorphic, implicitly, and strongly typed language (specifically Caml). Our method separates error-message generation from type-checking by taking a fundamentally new approach: we present to programmers small term-level modifications that cause an ill-typed program to become well-typed. This approach aims to improve feedback to programmers with no change to the underlying type-checker nor the compilation of well-typed programs.
10. Human-like error messages
Explaining Polymorphic Types
, Yang Jun, Greg Michaelson, and Phil Trinder. The Computer Journal, 2002.