1,066 papers · page 33 of 54
Automatic differentiation (AD) is a precise, efficient, and convenient method for computing derivatives of functions. Its forward-mode implementation can be quite simple even when extended to compute all of the higher-order derivatives as well. The higher-dimensional case has als…
Functional programming languages ought to play a central role in mathematics education for middle schools (age range: 10-14). After all, functional programming is a form of algebra and programming is a creative activity about problem solving. Introducing it into mathematics cours…
Functional logic programming and probabilistic programming have demonstrated the broad benefits of combining laziness (non-strict evaluation with sharing of the results) with non-determinism. Yet these benefits are seldom enjoyed in functional programming, because the existing fe…
Scribble is a system for writing library documentation, user guides, and tutorials. It builds on PLT Scheme's technology for language extension, and at its heart is a new approach to connecting prose references with library bindings. Besides the base system, we have built Scribbl…
We describe in this paper our implementation of the Xenstored service which is part of the Xen architecture. Xenstored maintains a hierarchical and transactional database, used for storing and managing configuration values.
During the life cycle of an XML application, both schemas and queries may change from one version to another. Schema evolutions may affect query results and potentially the validity of produced data. Nowadays, a challenge is to assess and accommodate the impact of these changes i…
This pearl aims to demonstrate the ideas of wholemeal and projective programming using the Towers of Hanoi puzzle as a running example. The puzzle has its own beauty, which we hope to expose along the way.
We report on our experience using Haskell as an executable specification language in the formal verification of the seL4 microkernel. The verification connects an abstract operational specification in the theorem prover Isabelle/HOL to a C implementation of the microkernel. We de…
We construct a logical framework supporting datatypes that mix binding and computation, implemented as a universe in the dependently typed programming language Agda 2. We represent binding pronominally, using well-scoped de Bruijn indices, so that types can be used to reason abou…
Arrows are a popular form of abstract computation. Being more general than monads, they are more broadly applicable, and in particular are a good abstraction for signal processing and dataflow computations. Most notably, arrows form the basis for a domain specific language called…
Purely functional programs should run well on parallel hardware because of the absence of side effects, but it has proved hard to realise this potential in practice. Plenty of papers describe promising ideas, but vastly fewer describe real implementations with good wall-clock per…
Continuation-based Web servers provide distinct advantages over traditional Web application development: expressive power and modularity. This power leads to fewer errors and more interesting applications. Furthermore, these Web servers are more than prototypes; they are used in …
We derive a control-flow analysis that approximates the interprocedural control-flow of both function calls and returns in the presence of first-class functions and tail-call optimization. In addition to an abstract environment, our analysis computes for each expression an abstra…
Type abstraction and intensional type analysis are features seemingly at odds-type abstraction is intended to guarantee parametricity and representation independence, while type analysis is inherently non-parametric. Recently, however, several researchers have proposed and implem…
This paper presents our experience using a domain-specific functional language, WaveScript, to build embedded sensing applications used in scientific research. We focus on a recent computervision application for detecting birds in their natural environment. The application was po…
High-level tools have become unavoidable in industrial software development processes. Safety-critical embedded programs don't escape this trend. In the context of safety-critical embedded systems, the development processes follow strict guidelines and requirements. The developme…
Ambitious experiments using proof assistants for programming language research and teaching are all the rage. In this talk, I'll report on one now underway at the University of Pennsylvania and several other sites: a one-semester graduate course in the theory of programming langu…
There is certain diverse class of diagram that is found in a variety of branches of mathematics and which all share this property: there is a common scheme for translating all of these diagrams into useful functional code. These diagrams include Bayesian networks, quantum compute…
Concurrent ML (CML) is a high-level message-passing language that supports the construction of first-class synchronous abstractions called events. This mechanism has proven quite effective over the years and has been incorporated in a number of other languages. While CML provides…
We describe the implementation of first-class polymorphic delimited continuations in the programming language Scala. We use Scala's pluggable typing architecture to implement a simple type and effect system, which discriminates expressions with control effects from those without …