QuickSpec: a lightweight theory exploration tool for programmers (system demonstration)
This document gives the outline of a system demonstration for the QuickSpec theory exploration tool.
26,098 papers · page 464 of 1,305
Hardware software co-design in Haskell
We present a library in Haskell for programming Field Programmable Gate Arrays (FPGAs), including hardware software co-design. Code for software (in C) and hardware (in VHDL) is generated from a single program, along with the code to support communication between hardware and sof…
Packrats parse in packs
We present a novel but remarkably simple formulation of formal language grammars in Haskell as functions mapping a record of pro- duction parsers to itself. Thus formulated grammars are first-class objects, composable and reusable. We also provide a simple parser implementation f…
Quantified class constraints
Quantified class constraints have been proposed many years ago to raise the expressive power of type classes from Horn clauses to the universal fragment of Hereditiary Harrop logic. Yet, while it has been much asked for over the years, the feature was never implemented or studied…
Speculate: discovering conditional equations and inequalities about black-box functions by reasoning from test results
This paper presents Speculate, a tool that automatically conjectures laws involving conditional equations and inequalities about Haskell functions. Speculate enumerates expressions involving a given collection of Haskell functions, testing to separate those expressions into appar…
Adaptive lock-free data structures in Haskell: a general method for concurrent implementation swapping
A key part of implementing high-level languages is providing built- in and default data structures. Yet selecting good defaults is hard. A mutable data structure’s workload is not known in advance, and it may shift over its lifetime—e.g., between read-heavy and write- heavy, or f…
Streaming irregular arrays
Previous work has demonstrated that it is possible to generate efficient and highly parallel code for multicore CPUs and GPUs from combinator-based array languages for a range of applications. That work, however, has been limited to operating on flat, rectangular structures witho…
Composable network stacks and remote monads
Monads and applicative functors are two ways that Haskell programmers bundle effectful primitives into effectful program fragments. In this paper, we investigate using monads and applicative functors to bundle remote effectful primitives, specifically aiming to amortize the cost …
A meta-EDSL for distributed web applications
We present a domain-specific language for constructing and configuring web applications distributed across any number of networked, heterogeneous systems. Our language is embedded in Haskell, provides a common framework for integrating components written in third-party EDSLs, and…
Elaboration on functional dependencies: functional dependencies are dead, long live functional dependencies!
Functional dependencies are a popular extension to Haskell's type-class system because they provide fine-grained control over type inference, resolve ambiguities and even enable type-level computations.
Ode on a random urn (functional pearl)
We present the urn, a simple tree-based data structure that supports sampling from and updating discrete probability distributions in logarithmic time. We avoid the usual complexity of traditional self-balancing binary search trees by not keeping values in a specific order. Inste…
Algebraic graphs with class (functional pearl)
The paper presents a minimalistic and elegant approach to working with graphs in Haskell. It is built on a rigorous mathematical foundation --- an algebra of graphs --- that allows us to apply equational reasoning for proving the correctness of graph transformation algorithms. Al…
The linearity Monad
We introduce a technique for programming with domain-specific linear languages using the monad that arises from the theory of linear/non-linear logic. In this work we interpret the linear/non-linear model as a simple, effectful linear language embedded inside an existing non-line…
Back to the future: time travel in FRP
Functional Reactive Programming (FRP) allows interactive applications to be modelled in a declarative manner using time-varying values. For practical reasons, however, operational constraints are often imposed, such as having a fixed time domain, time always flowing forward, and …
Algorithmic music in Haskell (invited talk)
Functional programming is becoming increasingly popular in artistic areas such as algorithmic music composition. Euterpea and Kulitta are two libraries for working with music in Haskell. Euterpea is a library for representing and manipulating basic musical structures, and is usef…
Ornaments: exploiting parametricity for safer, more automated code refactorization and code reuse (invited talk)
Inductive datatypes and parametric polymorphism are two key features introduced in the ML family of languages, which have already been widely exploited for structuring programs: Haskell and ML programs are often more elegant and more correct by construction. Still, we sometimes n…
Well-typed music does not sound wrong (experience report)
Music description and generation are popular use cases for Haskell, ranging from live coding libraries to automatic harmonisation systems. Some approaches use probabilistic methods, others build on the theory of Western music composition, but there has been little work done on ch…
A tale of two provers: verifying monoidal string matching in liquid Haskell and Coq
We demonstrate for the first time that Liquid Haskell, a refinement type checker for Haskell programs, can be used for arbitrary theorem proving by verifying a parallel, monoidal string matching algorithm implemented in Haskell. We use refinement types to specify correctness prop…
Using Coq to write fast and correct Haskell
Correctness and performance are often at odds in the field of systems engineering, either because correct programs are too costly to write or impractical to execute, or because well-performing code involves so many tricks of the trade that formal analysis is unable to isolate the…
Improving STM performance with transactional structs
Software transactional memory (STM) has made it significantly easier to write correct concurrent programs in Haskell. Its performance, however, is limited by several inefficiencies. While safe concurrent computations are easy to express in Haskell's STM, concurrent data structure…