916 papers · page 19 of 46
Abstract Advanced type system features, such as GADTs, type classes and type families, have proven to be invaluable language extensions for ensuring data invariants and program correctness. Unfortunately, they pose a tough problem for type inference when they are used as local ty…
Abstract Earlier studies have introduced a list of high-level evaluation criteria to assess how well a language supports generic programming. Languages that meet all criteria include Haskell because of its type classes and C++ with the concept feature. We refine these criteria in…
Abstract Many computer science departments are debating the role of programming languages in the curriculum. These discussions often question the relevance and appeal of programming-languages content for today's students. In our experience, domain-specific, “little languages” pro…
Abstract Existing package and system configuration management tools suffer from an imperative model , where system administration actions such as package upgrades or changes to system configuration files are stateful: they destructively update the state of the system. This leads …
Abstract The increasing availability of commodity multicore processors is making parallel computing ever more widespread. In order to exploit its potential, programmers need languages that make the benefits of parallelism accessible and understandable. Previous parallel languages…
Abstract Session types support a type-theoretic formulation of structured patterns of communication, so that the communication behaviour of agents in a distributed system can be verified by static typechecking. Applications include network protocols, business processes and operat…
I have just taken over from Richard Bird as editor of the Functional Pearls column in the Journal of Functional Programming . I'm keen to receive submissions; please do get in touch if you'd like to discuss a potential paper.
Abstract This paper shows how to reason about streams concisely and precisely. Streams, infinite sequences of elements, live in a coworld: they are given by a coinductive datatype, operations on streams are implemented by corecursive programs, and proofs are typically concocted u…
Generic programming is about making programs more adaptable by making them more general. Generic programs often embody non-traditional kinds of polymorphism; ordinary programs are obtained from them by suitably instantiating their parameters. In contrast to normal programs, the p…
Abstract The worker/wrapper transformation is a general technique for improving the performance of recursive programs by changing their types. The previous formalisation (A. Gill & G. Hutton, J. Funct. Program. , vol. 19, 2009, pp. 227–251) was based upon a simple fixed-point sem…
Abstract We introduce the arrow calculus, a metalanguage for manipulating Hughes's arrows with close relations both to Moggi's metalanguage for monads and to Paterson's arrow notation. Arrows are classically defined by extending lambda calculus with three constructs satisfying ni…
Abstract Term-rewriting systems can be expressed as generic programs parameterised over the shape of the terms being rewritten. Previous implementations of generic rewriting libraries require users to either adapt the datatypes that are used to describe these terms or to specify …
Abstract Datatype-generic programming (DGP) involves parametrization of programs by the shape of data, in the form of type constructors such as ‘list of’. Most approaches to DGP are developed in pure functional programming languages such as Haskell. We argue that the functional o…
Abstract Semantic definitions of full-scale programming languages are rarely given, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics – usually either for informal mathematics or the formal mathematics of a proof assi…
Abstract We present a semantic space profiler for parallel functional programs. Building on previous work in sequential profiling, our tools help programmers to relate runtime resource use back to program source code. Unlike many profiling tools, our profiler is based on a cost s…
The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP) was held in Victoria, British Columbia, Canada, in September 2008. Peter Thiemann chaired the program committee. After the conference, the authors of a selection of the presented papers were invited to…
Abstract The aim of our work is to be able to do fully formal, machine-verified proofs over Generic Haskell-style polytypic programs. In order to achieve this goal, we embed polytypic programming in the proof assistant Coq and provide an infrastructure for polytypic proofs. Polyt…
Abstract Propositions that express type equality are a frequent ingredient of modern functional programming – they can encode generic functions, dynamic types, and GADTs. Via the Curry–Howard correspondence, these propositions are ordinary types inhabited by proof terms , compute…
Abstract C-Rules is a business rules management system developed by Constraint Technologies International ( www.constrainttechnologies.com ) that is designed for use in transport, travel and logistics problems. Individual businesses within these industries often need to solve the…
Abstract Transient faults that arise in large-scale software systems can often be repaired by reexecuting the code in which they occur. Ascribing a meaningful semantics for safe reexecution in multithreaded code is not obvious, however. For a thread to reexecute correctly a regio…