This book presents latest research developments in the area of functional programming. The contributions in this volume cover a wide range of topics from theory, formal aspects of functional programming, transformational and generic programming to type checking and designing new classes of data types.
Not all papers in this book belong to the category of research papers. Also, the categories of project description (at the start of a project) and project evaluation (at the end of a project) papers are represented.
Particular trends in this volume are:
- software engineering techniques such as metrics and refactoring for high-level programming languages;
- generation techniques for data type elements as well as for lambda expressions;
- analysis techniques for resource consumption with the use of high-level programming languages for embedded systems;
- widening and strengthening of the theoretical foundations.
Tabella dei contenuti
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 Mc Bride
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 of Move a definition from one module to another in []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, Jocelyn Sérot 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 Mac Kenzie, 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
Circa l’autore
Dr. Marko van Eekelen is an associate professor in the Security of Systems Department of the Institute for Computing and Information Sciences, Radboud University, Nijmegen.
Altri ebook dello stesso autore / Editore
72.681 Ebook in questa categoria
