2: Emanuele Covino and Giovanni Pani. Complexity certification of C++ template metaprogramming (research paper)    submission   information
Abstract. Any partial recursive function can be computed at compile time, using C++ templates to define primitive recursion, composition, and minimalization. We define a dialect based on C++ templates, and we prove that it characterizes the set of polynomial-time functions, that is the set of functions computable by a Turing machine with time bounded by a polinomial. This language can be used as a form of complexity certification of functional programs.
====
3: Annette Bieniusa and Peter Thiemann. How to CPS Transform a Monad (research paper)    submission   information
Abstract. CPS transformation is an important tool in the compilation of
functional programming languages.  The existing transformations in
this area take some applied call-by-value lambda calculus as their
domain.  We integrate explicit monadic abstraction in such a source
language, present a Danvy-Filinski-style CPS transformation for
this extension, and verify that the translation preserves simple
typing.  We establish the simulation properties of this
transformation in an untyped setting and relate it to a two stage
transformation that implements the monadic abstraction with thunks and
introduces continuations in a second step.
====
4: Patricia Johann and Neil Ghani. Short Cut Fusion of Recursive Programs with Computational Effects (research paper)    submission   information
Abstract. Fusion is the process of improving the efficiency of modularly
constructed programs by transforming them into monolithic equivalents.
This paper defines a generalization of the standard build combinator
which expresses uniform production of functorial contexts containing
data of inductive types. It also proves correct a fusion rule which
generalizes the fold/build and fold/buildp rules from the literature,
and eliminates intermediate data structures of inductive types without
disturbing the contexts in which they are situated. An important
special case arises when this context is monadic. When it is, a second
rule for fusing combinations of producers and consumers via monad
operations, rather than via composition, is also available. We give
examples illustrating both rules, and consider their coalgebraic
duals as well.
====
5: Graham Hutton and Diana Fulger. Reasoning About Effects: Seeing the Wood Through the Trees (research paper)    submission   information
Abstract. Pure functional languages such as Haskell support programming with
impure effects by exploiting mathematical notions such as monads,
applicative functors, and arrows.  However, in contrast to the wealth
of research on the use of these notions to write effectful programs,
there has been comparatively little progress on reasoning about the
resulting programs.  In this article we focus on this problem, using a
simple but instructive example concerned with relabelling binary trees.
====
6: Michael Nissen and Ken Friis Larsen. FunSETL - Functional Reporting for ERP Systems. (project)    submission   information
Abstract. One of the essential features of enterprise information systems is the
ability to provide the users and decision makers with reports on how the
enterprise is running. By their nature these reports
needs to operate on large amounts of data and the decision makers need
the reports in a timely manner. Thus, the programs that generate the
reports are somewhat performance critical. To demonstrate our result we
introduce the reporting language FunSETL, which is a restricted ML dialect,
and show the test results, which have been produced by our FunSETL
benchmark suite.
====
7: Wouter Swierstra and Thorsten Altenkirch. Dependent Types for Distributed Arrays (research paper)    submission   information
Abstract. Locality-aware algorithms over distributed arrays can be very
difficult to write. Yet such algorithms are becoming more and more
important as desktop machines boast more and more processors.  We
show how a dependently-typed programming language can help develop
such algorithms by hosting a domain-specific embedded language
that ensures every well-typed program will only ever access local
data. Such static guarantees can help catch programming errors
early on in the development cycle and maximise the potential
speedup that multicore machines offer. At the same time, the
functional specification of effects we provide facilitates the
testing of and reasoning about algorithms that manipulate
distributed arrays.
====
8: Tom Schrijvers and Martin Sulzmann. Restoring Confluence for Functional Dependencies via Type Families (research paper)    submission   information
Abstract. Haskell-style functional dependencies provide a relational
specification of user-programmable type improvement connected to
type class instances. The more recent type families (also
known as type functions) equip the programmer with similar functionality,
but in a functional form and decoupled from type classes.
Functional dependencies are supported by both GHC and
Hugs, while the most recent version of GHC also supports type functions.

There was an enthusiastic and lively debate about which feature should be
adopted by the next Haskell standard, Haskell-Prime. Currently, further
progress in the standardization appears to be stalled on this issue.

In this work, we attempt to rekindle the debate with new insights in type
inference issues behind functional dependencies (FDs) and type functions (TFs),
without taking sides.  Specifically, we address the non-confluence issue of
Constraint Handling Rules (CHRs) resulting from non-full FDs.
CHRs serve as a meta-language to describe the constraint solver underlying the
type inferencer. Confluence of CHRs is important to ensure that the type
inferencer is complete.

We propose an alternative encoding which achieves confluence even for non-full
FDs.  We achieve this result by encoding FDs via TFs.  Technically, we could
use a different CHR encoding but by using TFs to encode FDs we can also explain
their commonalities and differences.  We give a sketch of the alternative
encoding below. The long version of this extended abstract will give an
in-depth discussion of several encodings and also address issues when violating
the (Weak) Coverage Condition.
====
9: Jocelyn SEROT. The semantics of a purely functional graph notation system (research paper)    submission   information
Abstract. We describe the formal semantics of a small, purely func-
tional language for describing graphs. Compared to other textual graph
notation systems, this language o?ers powerful features, such as higher-
order functions and polymorphism, for expressing concisely and elegantly
complex graph patterns. We give an interpretation of recursion in this
language as a way of describing cyclic graphs. We also introduce the
concept of meta-constructs to improve its expressivity.
====
10: Neil Brown and Adam T. Sampson. Matching, Modifying and Manufacturing with Generics (research paper)    submission   information
Abstract. Haskell has powerful features such as pattern matching, recursive data types for building tree structures easily, as well as type-classes. These features are not without problems, however; patterns are not composable, it can be hard to modify a specific part of a large tree structure, and deriving type-classes can be laborious. This paper explains how a particular Haskell generics approach, Scrap Your Boilerplate, can be used to solve all of these problems.
====
11: Jan Martin Jansen and rinus plasmeijer. Flexible Client/Server Processing for Web Apps (research paper)    submission   information
Abstract. Nowadays web browsers are often used as the universal interface for software systems. Since browsers runs on any platform it is possible to construct distributed applications without the need to install software on the client site and the need for the user to learn a new interface. In order to achieve acceptable response times it is sometimes necessary to handle parts of the event processing on the client by a browser plugin (requiring the installation of software), or better by the browser itself (e.g. with JavaScript). Existing Ajax technology enables exactly this. A drawback of current Ajax technology is that it is hard to construct programs. The parts that need to run on the client require a different programming language and style from the parts that run on the server. Moreover, the asynchronous communication between client and server needs to be programmed explicitly in each and every application.
In this paper we introduce a technology that enables the use of the same high level programming language on client and server and supports the necessary asynchronous communication. This makes it possible to write one program and indicate in a flexible way what parts of this program should be executed on the client.
As a result it is now much easier to create highly interactive user interfaces in an arbitrary web browser, again  without the need to install any special software at the client site.
====
12: Brian Campbell. Prediction of linear memory usage for first-order functional programs (research paper)    submission   information
Abstract. Hofmann and Jost have presented a type inference system for a pure
  first-order functional language which uses linear programming to give linear
  upper bounds on heap memory usage with respect to the input size.  We present
  an extended analysis which infers bounds for heap and stack space
  requirements, and which uses more expressive post-evaluation bounds to model
  a common pattern of stack space use.
====
13: Louis-Julien Guillemette and Stefan Monnier. One Vote for Type Families in Haskell! (position)    submission   information
Abstract. Generalized Algebraic Datatypes (GADTs) allow programmers to capture

important invariants of their data structures through type annotations

on data constructors.  However when working with GADTs, it is often

difficult to concisely and precisely express the way complex data

manipulations maintain those invariants.  One can approach the problem

in a few different ways, given the type arsenal of GHC's current

extensions.  One approach is to use type classes with functional

dependencies.  Another approach is to introduce yet more GADTs to

capture the behavior of individual functions.  A third alternative is

to use type families, a recent introduction of GHC by which functions

over types can be defined directly, much like term-level functions,

and appear in type signatures.



In this paper we illustrate the use of type families in the context of

a type-preserving compiler written in Haskell.  We compare the results

with an ad-hoc, all-GADT solution.  We argue that type families

promote a more direct programming style that eliminates much code

bloat and translates into increased run-time performance.  We

also briefly describe a use of type families to capture more complex

data structure invariants and the current limitations that appear with

these more advanced uses.
====
15: Mercedes Hidalgo-Herrero and yolanda Ortega-Mallén. Calculational Reasoning for Parallel Functional (research paper)    submission   information
Abstract. The functional parallel language Eden has proven to be highly
suitable for a programming methodology based on algorithmic
skeletons, and now we would like to reason about programs using
these skeletons. For this purpose we have defined a
continuation-based denotational semantics for Eden. In the present
paper we show how to use this semantics to reason about programs,
to detect and measure speculative computations, and to prove
behavioural equivalences.
====
16: Lidia Sánchez Gil and yolanda Ortega-Mallén. On the Relation between Operational and Denotational Semantics in a Parallel and Functional Setting (research paper)    submission   information
Abstract. Operational semantics and denotational semantics are the two faces
of a same coin. While operational semantics describe an abstract
model of program execution ---usually based on some abstract
machine--- and are intended for compiler and implementation
designers, denotational semantics construct for each program some
mathematical object that represents its meaning, and their higher
level of abstraction allow the analysis of program properties and
different forms of calculational reasoning, that are of great
interest for programmers. It is therefore very common to define
for a same language several formal semantics with separate
purposes  ---not only operational and denotational ones of various
levels of abstraction, but also of other kinds like axiomatic or
algebraic semantics---. The question is to establish the relation
between these, and to demonstrate its equivalence, i.e. that they
describe the same language. Typically this is done in terms of
correctness  (of the operational rules with respect to the
denotational semantics) and computational adequacy (i.e.
there exists a valid operational reduction iff the denotational
value is non-bottom), or  in terms of full abstraction with
respect to some appropriate notion of program behavior.
====
17: Manuel Montenegro, ricardo pena and Clara Segura. A Simple Region Inference Algorithm for a First-Order Functional Language (research paper)    submission   information
Abstract. Safe is a first-order eager language with facilities for programmer controlled destruction and copying of data structures. It provides also regions, i.e. disjoint parts of the heap, where the program  allocates data structures. The runtime system does not need a garbage collector and all allocation/deallocation actions are done in  constant time. The language is aimed at inferring and certifying upper bounds for memory consumption in a Proof Carrying Code environment. Some of its analyses have been presented elsewhere.

In this paper we present a simple region inference algorithm for annotating programs with regions arguments and region types. Programmers are assumed to write programs, and to declare datatypes, without any reference to regions. Then, the algorithm decides the regions that will be needed by every function and type. We show convincing examples of programs before and after region annotation. In the final paper we will prove the correctness and optimality of the inference algorithm and give its asymptotic cost.
====
18: Alejandro Tamalet, Olha Shakaravska and Marko van Eekelen. Size Analysis of Algebraic Data Types (research paper)    submission   information
Abstract. This work is part of the Amortised Heap space usage Analysis (AHA)
project, where we have earlier developed a size-aware type system for a
first-order functional language whose only data types were integers and lists.

In this paper we extend the language and the analysis to deal with algebraic
data types. We define how to generate typing rules for algebraic data types,
provided their size function meet certain requirements. We call such types shapely
with respect to that size function.

A parameterised ordinary inductive type is an initial algebra of the
parameterised polynomial endofunctor F defined by its type constructors.
For such types the canonical size function is shown to be a sensible
metric in the sense that it counts all the constructors of the type.
Proofs for soundness and decidability of the type system under a syntactic
restriction are sketched.
====
19: Abdallah Al Zain, Phil Trinder, Jost Berthold, Rita Loogen, Kevin Hammond and Hans-Wolfgang Loidl. Parallel Functional Middleware for Computational Algebra Systems (research paper)    submission   information
Abstract. This paper outlines the design, implementation and preliminary
  evaluation of CAG, a core component of the SymGrid-Par parallel
  functional middleware for a range of Computational Algebra (CA)
  systems. CAG is a set of algorithmic skeletons implemented in a
  parallel Haskell, with an interface provided in each of four
  computational algebra systems: Maple, MuPad, GAP and Kant. The
  interface represents mathematical objects in the standard OpenMath
  XML format, and hence enables the CA systems to interoperate. As
  part of SymGrid-Par, CAG is applied to real computational algebra
  problems, and many of these are highly-irregular, e.g.\ with task
  sizes varying by 6 orders of magnitude.
====
20: Edwin Brady, Christoph Herrmann and Kevin Hammond. Lightweight Invariants with Full Dependent Types (position)    submission   information
Abstract. Dependent types allow a programmer to express invariant properties of
functions, such as the relationship between the input and output
lengths of a list. Several ``lightweight'' approaches to dependent
types have been proposed for existing systems, such as Haskell's
Generalised Algebraic Data Types. Such approaches are lightweight in
the sense that they require minimal modifications to existing
systems. However, we run into limitations of these approaches fairly
quickly. In this paper we will demonstrate that what is lightweight
for the language implementor is not necessarily lightweight for the
programmer, and show that a full dependent type system allows
more straightforward implementation of simple invariants without
restricting expressivity.
====
21: Andre Rauber Du Bois and Gerson Cavalheiro. Design and Implementation of a semi-explicit parallel purely functional language (research paper)    submission   information
Abstract. In this paper we present the design and implementation of
$p$Fun, a semi-explicit parallel purely functional language. Parallelism is introduced in $p$Fun through simple annotations in the code. Task creation,
synchronization and scheduling of computations on remote hosts
are managed automatically by $p$Fun's distributed runtime system.
$p$Fun's programming model and  runtime system are described, and preliminary
measurements of the current prototype implementation are presented on an
SMP-machine and on a Beowulf Cluster.
====
22: Alexander Green and Thorsten Altenkirch. Shor in Haskell (The Quantum IO Monad) (research paper)    submission   information
Abstract. We present an interface from Haskell to quantum programming: the
Quantum IO monad, and use it to implement Shor's factorization
algorithm. The QIO monad separates reversible (i.e. unitary) and
irreversible (i.e. probabilistic) computations and provides a
reversible let operation (|ulet|), allowing us to use \emph{ancillas}
(auxiliary qubits) in a modular fashion. Exploiting Haskell's class
system we can present our algorithms in a high level way, implementing
abstractions in the functional paradigm. We describe the
implementation of Shor's algorithm in some detail also covering the
necessary reversible arithmetic. QIO programs can be simulated either
by calculating a probability distribution or by embedding it into the
IO monad using the random number generator.
====
23: Neil Sculthorpe and Henrik Nilsson. Optimisation of Dynamic, Hybrid Signal Function Networks (research paper)    submission   information
Abstract. Functional Reactive Programming (FRP) is an approach to reactive programming where systems are structured as networks of functions operating on signals. FRP is based on the synchronous data-flow paradigm and supports both continuous-time and discrete-time signals, i.e. hybrid systems. What sets FRP apart from most other languages for similar applications is its support for systems with dynamic structure and for higher-order data-flow constructs. This raises a range of implementation challenges. This paper contributes towards advancing the state of the art of FRP implementation by studying the notion of signal change and change propagation in a setting of hybrid signal function networks with dynamic structure. To sidestep some problems of certain previous FRP implementations that are structured using arrows, we suggest working with a notion of composable, multi-input and multi-output signal functions. A clear conceptual distinction is also made between continuous-time and discrete-time signals. We then show how establishing change-related properties of the signal functions in a network allows such networks to be simplified (static optimisation) and can help reducing the amount of computation needed for executing the networks (dynamic optimisation). Interestingly, distinguishing between continuous-time and discrete-time signals allows us to characterise the change-related properties of signal functions more precisely than what we otherwise would have been able to, which is helpful for optimisation.
====
24: Oleg Lobachev, Jost Berthold, Mischa Dieterle and Rita Loogen. Parallel FFT Using Divide and Conquer Skeletons (research paper)    submission   information
Abstract. The notion of `Fast Fourier Transform' (FFT) describes a range of efficient algorithms to compute the discrete Fourier transform, which plays a major role both for pure mathematical applications and for real-life scenarios such as digital signal processing. In essence, all FFT algorithms are based on divide and conquer strategies.

In our paper, we plan to investigate different concrete algorithms for FFT, with a focus on their parallelising potential. We will present the major FFT algorithm classes, apply suitable functional skeletons for divide and conquer for our implementation, and specialise them for the particular algorithms in question. We plan to do comparative measurements for our implementations and propose hybrid FFT algorithm combinations for better parallel performance.
====
25: Nik Sultana and Simon Thompson. A Certified Refactoring Engine (research paper)    submission   information
Abstract. The paper surveys how software tools such as refactoring systems can
be validated, and introduces a new mechanism, namely the extraction of
a refactoring engine for a functional programming language from an
Isabelle/HOL theory in which it is verified. This research is a first
step in a programme to construct certified programming tools from
verified theories. We also provide some empirical evidence of how
refactoring can be of significant benefit in reshaping
automatically-generated program code for use in larger systems.
====
26: Máté Tejfel, Tamás Kozsik and Zoltán Horváth. An Operational Semantics of Temporal Properties in Functional Programs (research paper)    submission   information
Abstract. This paper presents an operational semantics for functional programs extended with object abstraction. The introduced annotated tree-semantics makes it possible to interpret temporal properties of abstract objects. It also enables the investigation of the soundnes of the axiomatic semantics of temporal properties provided in earlier work.
====
27: Ulrik Schultz, Mirko Bordignon, David Christensen and Kasper Stoy. A Functional Language for Programming Self-Reconfigurable Robots (research paper)    submission   information
Abstract. A self-reconfigurable robot is a robotic device that can change its own shape.
  Self-reconfigurable robots are commonly built from multiple identical modules that can
  manipulate each other to change the shape of the robot. The robot can also perform tasks
  such as locomotion without changing shape.  Programming a modular, self-reconfigurable
  robot is however a complicated task: the robot is essentially a real-time, distributed
  embedded system, where control and communication paths often are tightly coupled to the
  current physical configuration of the robot.  To facilitate the task of programming
  modular, self-reconfigurable robots, we are currently developing a functional,
  domain-specific language that allows the programmer to use pattern matching and
  higher-order functions to program closely coordinated groups of modules.  In more
  detail, higher-order functions are used to specify behaviors that are applied to groups
  of modules and a distributed pattern matching mechanism is used to select specific
  behaviors from these functions depending on the state of the individual modules.  Our
  language is currently being implemented for a virtual machine running on the ATRON
  self-reconfigurable robot.
====
28: Liyang HU and Graham Hutton. Implementing Software Transactional Memory, Correctly (research paper)    submission   information
Abstract. In recent years there has been much interest in the idea of concurrent
programming using "transactional memory", for example as provided in
STM Haskell. While programmers are provided with a simple high-level model
of transactions in terms of a stop-the-world semantics, the low-level
implementation is rather more complex, involving subtle techniques that
allow multiple transactions to execute concurrently. In this article, we
take the first steps towards a formally verified implementation of
transactional memory. In particular, we present a stripped-down, idealised
concurrent language inspired by STM Haskell, and show how a low-level
implementation of this language can be justified with respect to
a high-level semantics, by means of a compiler and its correctness theorem,
validated using QuickCheck and HPC.
====
29: Arie Middelkoop, Atze Dijkstra and Doaitse Swierstra. A Simple Specification and Implementation for Generalized Abstract Data Types (research paper)    submission   information
Abstract. Current approaches for the specification and implementation of Generalized
Abstract Data Types are complicated and unconventional. Do we need
complex type systems to implement GADTs? To answer this question, we give a
simple specification for GADTs that covers all essential aspects. Furthermore, we
give an implementation in terms of already existing mechanisms (most notably
qualified types) to keep implementation complexity minimal.
====
30: Ryan Ralston. ACL2-Certified AVL Trees: an experiment in software engineering (project)    submission   information
Abstract. AVL trees supply operations for information storage and retrieval in
time proportional to the logarithm of the number of items stored and
in a space increment, beyond the space needed for the information
itself, that increases linearly with the number of items. The public
operations of insertion, deletion, and retrieval are supported
internally by rotations to maintain order and balance properties
that make it possible to meet logarithmic performance requirements.
This report describes an AVL implementation in ACL2, a subset of Common Lisp
with a built-in mechanical logic for verifying properties of defined
operations. It focuses on verifying correctness issues of order,
balance, and conservation of keys for the insertion operation, and
anticipates similar verifications for deletion. The report also
discusses the investment required to include such verifications as
part of the software development process, describes a continuing
experimental project in developing useful software components with
certified properties in standard programming languages, and argues
that a trend towards incorporating logic engines in programming
environments benefits both the discipline of software engineering
and the practice of software development.
====
31: Huiqing Li and Simon Thompson. Clone Detection and Removal for Erlang/OTP within a Refactoring Environment (research paper)    submission   information
Abstract. A well-known bad code smell in refactoring and software maintenance is duplicated code, or code clones. A code clone is a code fragment that is identical or similar to another. Unjustified code clones increase code size, make  maintenance and comprehension more difficult, and also indicate design problems such as lack of encapsulation or abstraction. Various approaches and techniques have been proposed
to facilitate the detection and removal of code clones especially for object-oriented code.   

Wrangler is the refactoring tool developed at Kent for Erlang/OTP, an industrial strength functional programming environment. Wrangler supports clone detection cross multiple modules, and user-controlled automatic clone removal. This paper first describes the implementation of the Wrangler clone detector, which makes use of both token suffix tree and abstract syntax trees to improve efficiency and accuracy. It then introduces the refactorings that have been implemented to support the removal of existing clones, and examines their application in a substantial case study.
====
32: Wolfgang Jeltsch. Push-based FRP Improved (research paper)    submission   information
Abstract. Push-based implementations of Functional Reactive Programming allow to write reactive programs in a declarative style and execute them efficiently.  Previous approaches in this area lack declarative means to describe systems with feedbacks, that is, systems where the input of some part depends on the output of this part.  In addition, they split the reaction to an event into multiple reactions in certain situations.  This may lead to efficiency problems and introduction of inconsistent intermediate states.  We present an implemenation of discrete FRP which does not suffer from these deficiencies.  This leads to an FRP core which is more declarative than previous solutions and offers performance improvements at the same time.
====
33: Sunil Kothari and James Caldwell. On Desugaring Polymorphic Lets (research paper)    submission   information
Abstract. Existing type literature has conflicting views on desugaring polymorphic lets
to lambda terms. The conflict arises because, in certain cases,
desugaring does not preserve typing. We describe a transformation of
polymorphic lets to monomorphic lets such that, when the monomorphic
lets are desugared, the typing is preserved.  Our transformation
requires no changes to either term or type syntax. This transformation
is used, in our past works, as a semantic tool for completeness and soundness of an extension to Wand's algorithm to handle polymorphic let.
====
35: Michael Haskel. The M Programming Language (project)    submission   information
Abstract. M aims to be a powerful tool for the mathematical expression
of programs and programming concepts.  As a functional programming
language with dependent types based closely on pure type systems, it
distinguishes itself from similar efforts by making use of the
relationship between dependent typing and constructive mathematics,
while still emphasizing programming over proving.
====
36: Vladimir Janjic and Kevin Hammond. Prescient Scheduling of Parallel Functional Programs on the Grid (position)    submission   information
Abstract. To allow efficient scheduling of multiple parallel
applications on Computational Grids, it is desirable to have a scheduling mechanism that can anticipate dynamic changes in parallelism for an application and
respond to these changes by  dynamically tuning the resources that
are allocated to the application.
It is our contention that functional programming technology
supports such scheduling, while simultaneously providing
support for high level parallelism abstractions to applications. This
benefits both Grid application developers (by allowing them to
concentrate on programming at a high level of abstraction, while ignoring
low level issues such as thread migration, synchronization etc.)
and Grid resource providers (by permitting high utilization of
resources)

This paper will present the design of a dynamic, adaptive prescient} scheduler
for parallel functional Grid programs, possesing both
foresight of future application behavior and foreknowledge of future application needs. We propose a set of experiments that will demonstrate that our scheduling methods can improve the average response times of parallel functional applications on the Grid, compared with classical static scheduling approaches.
