1 Best student Paper: A New Approach to One-Pass Transformations [1]
Kevin Millikin
1.1 Introduction
1.2 Cata/build Fusion for [?-Terms]
1.3 The Call-by-value CPS Transformation Using Build
1.4 A Catamorphic Normalization Function
1.5 A New One-Pass Call-by-value CPS Transformation
1.6 Suppressing Contraction of Source Redexes
1.7 Comparison to Danvy and Filinski's One-Pass CPS Transformation
1.8 A New One-Pass Call-by-name CPS Transformation
1.9 Related Work and Conclusion
References
2 A Static Checker for Safe Pattern Matching in Haskell [15]
Neil Mitchell and Colin Runciman
2.1 Introduction
2.2 Reduced Haskell
2.3 A Constraint Language
2.4 Determining the Constraints
2.5 A Worked Example
2.6 Some Small Examples and a Case Study
2.7 Related Work
2.8 Conclusion and Further Work
References
3 Software Metrics: Measuring Haskell [31]
Chris Ryder, Simon Thompson
3.1 Introduction
3.2 What Can Be Measured
3.3 Validation Methodology
3.4 Results
3.5 Conclusion and Further Work
References
4 Type-Specialized Serialization with Sharing [47]
Martin Elsman
4.1 Introduction
4.2 The Serialization Library
4.3 Implementation
4.4 Experiments with the MLKit
4.5 Conclusions and Further Work
References
5 Logical Relations for Call-by-value Delimited Continuations [63]
Kenichi Asai
5.1 Introduction
5.2 Preliminaries
5.3 Specializer for Call-by-name []-Calculus
5.4 Logical Relations for Call-by-value []-Calculus
5.5 Specializer in CPS
5.6 Specializer in Direct Style
5.7 Interpreter and A-normalizer for Shift and Reset
5.8 Specializer for Shift and Reset
5.9 Type System for Shift and Reset
5.10 Logical Relations for Shift and Reset
5.11 Related Work
5.12 Conclusion
References
6 Epigram Reloaded: A Standalone Typechecker for ETT [79]
James Chapman, Thorsten Altenkirch, Conor McBride
6.1 Introduction
6.2 Dependent Types and Typechecking
6.3 Epigram and its Elaboration
6.4 ETT Syntax in Haskell
6.5 Checking Types
6.6 From Syntax to Semantics
6.7 Checking Equality
6.8 Related Work
6.9 Conclusions and Further Work
References
7 Formalisation of Haskell Refactorings [95]
Huiqing Li, Simon Thompson
7.1 Introduction
7.2 Related Work
7.3 The []-Calculus with Letrec ([]LETREC)
7.4 The Fundamentals of ([]LETREC)
7.5 Formalisation of Generalizing a Definition
7.6 Formalisation of a Simple Module System []M
7.7 Fundamentals of []M
7.8 Formalisation ofMove a definition from one module to anotherin []M
7.9 Conclusions and Further Work
References
8 Systematic Search for Lambda Expressions [111]
Susumu Katayama
8.1 Introduction
8.2 Implemented System
8.3 Efficiency Evaluation
8.4 Discussions for Further Improvements
8.5 Conclusions
References
9 First-Class Open and Closed Code Fragments [127]
Morten Rhiger
9.1 Introduction
9.2 Open and Closed Code Fragments
9.3 Syntactic Type Soundness
9.4 Examples
9.5 Related Work
9.6 Conclusions
References
10 Comonadic Functional Attribute Evaluation [145]
Tarmo Uustalu and Varmo Vene
10.1 Introduction
10.2 Comonads and Dataflow Computation
10.3 Comonadic Attribute Evaluation
10.4 Related Work
10.5 Conclusions and Future Work
References
11 Generic Generation of the Elements of Data Types [163]
Pieter Koopman, Rinus Plasmeijer
11.1 Introduction
11.2 Introduction to Automatic Testing
11.3 Generic Test Data Generation in Previous Work
11.4 Generic Test Data Generation: Basic Approach
11.5 Pseudo-Random Data Generation
11.6 Restricted Data Types
11.7 Related Work
11.8 Conclusion
References
12 Extensible Record with Scoped Labels [179]
Daan Leijen
12.1 Introduction
12.2 Record operations
12.3 The Types of Records
12.4 Higher-Ranked Impredicative Records
12.5 Type Rules
12.6 Type Inference
12.7 Implementing Records
12.8 Related Work
12.9 Conclusion
References
13 Project Start Paper: The Embounded Project [195]
Kevin Hammond, Roy Dyckhoff, Christian Ferdinand, Reinhold Heckmann, Martin Hofmann, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Robert Pointon, Norman Scaife, JocelynSerot and Andy Wallace
13.1 Project Overview
13.2 The Hume Language
13.3 Project Work Plan
13.4 The State of the Art in in Program Analysis for Real-Time Embedded Systems
13.5 Existing Work by the Consortium
13.6 Conclusions
References
14 Project Evaluation Paper: Mobile Resource Guarantees [211]
Donald Sannella, Martin Hoffmann, David Aspinall, Stephen Gilmore, Ian Stark, Lennart Beringer, Hans-Wolfgang Loidl, Kenneth MacKenzie, Alberto Momigliano, Olha Shkaravska
14.1 Introduction
14.2 Project Objectives
14.3 An Infrastructure for Resource Certification
14.4 A PCC Infrastructure for Resources
14.5 Results
References
