Presentation Papers
Fosa
Assigned Papers
| 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 |
Description
Below you can find a list of research papers for the (individual) presentations. Everyone should read the presented paper before the lecture 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 asWebCHR for online experimentation with more than 40 constraint solvers. More than 100 projects use CHR.
References: - Theory and Practice of Constraint Handling Rules, Thom Frühwirth. Journal of Logic Programming, Vol 37(1-3), 1998.
- A website dedicated to CHRs.
2. Chameleon
Chameleon is a Haskell-style language which supports several type extensions and improved type error diagnosis, and which is based on Constraint Handling Rules. References:- Interactive type debugging in Haskell, P.J. Stuckey, M. Sulzmann, and J. Wazny. Haskell Workshop 2003.
- Chameleon Homepage
3. Tinkertype
Tinkertype is a framework for compact and modular description of formal systems. An implementation in ML is available (with the paper). References:- TinkerType: A Language for Playing with Formal Systems, Michael Y. Levin and Benjamin C. Pierce. Journal of Functional Programming, 13(2), 2003.
4. Software Metrics
References:- Software Metrics: Measuring Haskell, Chris Ryder and Simon Thompson. Trends in Functional Programming, 2005.
- Software measurement for functional programming, Chris Ryder. Phd thesis, 2004.
5. Programming Environments
More specifically, take a look at the Visual Haskell development environment, and at an Eclipse plugin for Haskell. References:- Visual Haskell, Krasimir Angelov and Simon Marlow. Haskell Workshop, 2005.
- Eclipse 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. References:- Typed Contracts for Functional Programming, Ralf Hinze, Johan Jeuring, and Andres Loeh. FLOPS 2006
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. References:- Type error slicing in implicitly typed higher-order languages, Christian Haack and J. B. Wells. Sci. Comput. Programming, 50:189-224, 2004.
- Online demo
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. References:- How to repair type errors automatically, Bruce McAdam? . TFP 2001.
9. SEMINAL
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. References:- Seminal: Searching for ML Type-Error Messages, Benjamin Lerner, Dan Grossman and Craig Chambers. To appear at Workshop on ML, 2006.