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.

• 1 Best student Paper: A New Approach to One-Pass Transformations          [1]Kevin Millikin1.1 Introduction1.2 Cata/build Fusion for [?-Terms]1.3 The Call-by-value CPS Transformation Using Build1.4 A Catamorphic Normalization Function1.5 A New One-Pass Call-by-value CPS Transformation1.6 Suppressing Contraction of Source Redexes1.7 Comparison to Danvy and Filinski's One-Pass CPS Transformation1.8 A New One-Pass Call-by-name CPS Transformation1.9 Related Work and ConclusionReferences 2 A Static Checker for Safe Pattern Matching in Haskell          [15]Neil Mitchell and Colin Runciman2.1 Introduction2.2 Reduced Haskell2.3 A Constraint Language 2.4 Determining the Constraints2.5 A Worked Example2.6 Some Small Examples and a Case Study2.7 Related Work2.8 Conclusion and Further WorkReferences 3 Software Metrics: Measuring Haskell          [31]Chris Ryder, Simon Thompson3.1 Introduction3.2 What Can Be Measured3.3 Validation Methodology3.4 Results3.5 Conclusion and Further WorkReferences 4 Type-Specialized Serialization with Sharing          [47]Martin Elsman4.1 Introduction4.2 The Serialization Library 4.3 Implementation4.4 Experiments with the MLKit4.5 Conclusions and Further WorkReferences 5 Logical Relations for Call-by-value Delimited Continuations          [63]Kenichi Asai5.1 Introduction5.2 Preliminaries5.3 Specializer for Call-by-name []-Calculus5.4 Logical Relations for Call-by-value []-Calculus5.5 Specializer in CPS5.6 Specializer in Direct Style5.7 Interpreter and A-normalizer for Shift and Reset5.8 Specializer for Shift and Reset5.9 Type System for Shift and Reset5.10 Logical Relations for Shift and Reset5.11 Related Work5.12 ConclusionReferences 6 Epigram Reloaded: A Standalone Typechecker for ETT          [79]James Chapman, Thorsten Altenkirch, Conor McBride6.1 Introduction6.2 Dependent Types and Typechecking6.3 Epigram and its Elaboration6.4 ETT Syntax in Haskell6.5 Checking Types6.6 From Syntax to Semantics6.7 Checking Equality6.8 Related Work6.9 Conclusions and Further WorkReferences 7 Formalisation of Haskell Refactorings          [95]Huiqing Li, Simon Thompson7.1 Introduction7.2 Related Work7.3 The []-Calculus with Letrec ([]LETREC)7.4 The Fundamentals of ([]LETREC)7.5 Formalisation of Generalizing a Definition7.6 Formalisation of a Simple Module System []M7.7 Fundamentals of []M7.8 Formalisation of Move a definition from one module to another in []M7.9 Conclusions and Further WorkReferences 8 Systematic Search for Lambda Expressions          [111]Susumu Katayama8.1 Introduction8.2 Implemented System8.3 Efficiency Evaluation8.4 Discussions for Further Improvements8.5 ConclusionsReferences 9 First-Class Open and Closed Code Fragments          [127]Morten Rhiger9.1 Introduction9.2 Open and Closed Code Fragments9.3 Syntactic Type Soundness9.4 Examples9.5 Related Work9.6 ConclusionsReferences 10 Comonadic Functional Attribute Evaluation          [145]Tarmo Uustalu and Varmo Vene10.1 Introduction10.2 Comonads and Dataflow Computation10.3 Comonadic Attribute Evaluation10.4 Related Work10.5 Conclusions and Future WorkReferences 11 Generic Generation of the Elements of Data Types          [163]Pieter Koopman, Rinus Plasmeijer 11.1 Introduction11.2 Introduction to Automatic Testing11.3 Generic Test Data Generation in Previous Work11.4 Generic Test Data Generation: Basic Approach11.5 Pseudo-Random Data Generation11.6 Restricted Data Types11.7 Related Work11.8 ConclusionReferences 12 Extensible Record with Scoped Labels          [179]Daan Leijen 12.1 Introduction12.2 Record operations12.3 The Types of Records12.4 Higher-Ranked Impredicative Records12.5 Type Rules12.6 Type Inference12.7 Implementing Records12.8 Related Work12.9 ConclusionReferences 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 Wallace13.1 Project Overview13.2 The Hume Language13.3 Project Work Plan13.4 The State of the Art in in Program Analysis for Real-Time Embedded Systems13.5 Existing Work by the Consortium13.6 ConclusionsReferences 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 Shkaravska14.1 Introduction14.2 Project Objectives14.3 An Infrastructure for Resource Certification14.4 A PCC Infrastructure for Resources14.5 ResultsReferences