title: Experience report: developing high performance HTTP/2 server in Haskell

abstract: While the speed of the Internet has been increasing, HTTP/1.1 has been plagued by head-of-line blocking, low concurrency and redundant headers. To solve these problems, HTTP/2 was standardized. This paper summarizes our experience implementing HTTP/2 in Haskell. We found several techniques to improve the performance of the header compression and identified a suitable data structure for HTTP/2 priority. Also, we showed that Haskell lightweight threads are useful for HTTP/2 where the common tactics of one lightweight thread per connection cannot be used. The HTTP/2 implementation of Warp, the popular HTTP server library in Haskell, ultimately provides better throughput than its HTTP/1.1 counterpart.


venue: haskell

title: QuickSpec: a lightweight theory exploration tool for programmers (system demonstration)

authors:
Maximilian Algehed
Koen Claessen
Moa Johansson
Nicholas Smallbone

abstract: This document gives the outline of a system demonstration for the QuickSpec theory exploration tool.


title: Hardware software co-design in Haskell

authors:
Markus Aronsson
Mary Sheeran

abstract: 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 software. We present type-based techniques for the simultaneous implementation of more than one embedded domain specific language (EDSL). We build upon a generic representation of imperative programs that is loosely coupled to instruction and expression types, allowing the individual parts to be developed and improved separately. Code generation is implemented as a series of translations between progressively smaller, typed EDSLs, safeguarding against errors that arise in untyped translations. Initial case studies show promising performance.


title: Packrats parse in packs

authors:
Mario Blazevic
Jacques Légaré

abstract: 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 for them, based on an improved packrat algorithm. In order to make the grammar manipulation code reusable, we introduce a set of type classes mirroring the existing type classes from Haskell base library, but whose methods have rank-2 types.


title: Quantified class constraints

authors:
Gert-Jan Bottu
Georgios Karachalias
Tom Schrijvers
Bruno C. d. S. Oliveira
Philip Wadler

abstract: 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 in depth. Instead, several workarounds have been proposed, all of which are ultimately stopgap measures.


title: Speculate: discovering conditional equations and inequalities about black-box functions by reasoning from test results

authors:
Rudy Braquehais
Colin Runciman

abstract: 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 apparent equivalence classes. Expressions in the same equivalence class are used to conjecture equations. Representative expressions of different equivalence classes are used to conjecture conditional equations and inequalities. Speculate uses lightweight equational reasoning based on term rewriting to discard redundant laws and to avoid needless testing. Several applications demonstrate the effectiveness of Speculate.


title: Adaptive lock-free data structures in Haskell: a general method for concurrent implementation swapping

authors:
Chao-Hong Chen
Vikraman Choudhury
Ryan R. Newton

abstract: 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 from heavy contention by multiple threads to single- threaded or low-frequency use. One idea is to switch implementa- tions adaptively, but it is nontrivial to switch the implementation of a concurrent data structure at runtime. Performing the transition requires a concurrent snapshot of data structure contents, which normally demands special engineering in the data structure’s de- sign. However, in this paper we identify and formalize an relevant property of lock-free algorithms. Namely, lock-freedom is su cient to guarantee that freezing memory locations in an arbitrary order will result in a valid snapshot. Several functional languages have data structures that freeze and thaw, transitioning between mutable and immutable, such as Haskell vectors and Clojure transients, but these enable only single-threaded writers. We generalize this approach to augment an arbitrary lock-free data structure with the ability to gradually freeze and optionally transition to a new representation. This aug- mentation doesn’t require changing the algorithm or code for the data structure, only replacing its datatype for mutable references with a freezable variant. In this paper, we present an algorithm for lifting plain to adaptive data and prove that the resulting hy- brid data structure is itself lock-free, linearizable, and simulates the original. We also perform an empirical case study in the context of heating up and cooling down concurrent maps.


title: Streaming irregular arrays

authors:
Robert Clifton-Everest
Trevor L. McDonell
Manuel M. T. Chakravarty
Gabriele Keller

abstract: 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 without any facilities for irregularity or nesting.


title: Composable network stacks and remote monads

authors:
Justin Dawson
Mark Grebe
Andy Gill

abstract: 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 of remote communications using bundling. We look at several ways of maximizing the bundling of primitives, drawing from the remote monad design pattern and Haxl system, and provide a taxonomy of mechanism for amortization, with examples. The result of this investigation is that monadic fragments can be efficiently bundled into packets, almost for free, when given a user-supplied packet transportation mechanism, and the primitives obey some simple pre- and post-conditions.


title: A meta-EDSL for distributed web applications

abstract: 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 enables type-safe, access-controlled communication between nodes, as well as effortless sharing and movement of functionality between application components. We give an implementation of our language and demonstrate its applicability by using it to implement several important components of distributed web applications, including RDBMS integration, load balancing, and fine-grained sandboxing of untrusted third party code.


title: Elaboration on functional dependencies: functional dependencies are dead, long live functional dependencies!

authors:
Georgios Karachalias
Tom Schrijvers

abstract: 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.


title: Ode on a random urn (functional pearl)

authors:
Leonidas Lampropoulos
Antal Spector-Zabusky
Kenneth Foner

abstract: 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. Instead, we keep the tree maximally balanced at all times using a single machine word of overhead: its size.


title: Algebraic graphs with class (functional pearl)

abstract: 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. Algebraic graphs let us avoid partial functions typically caused by `malformed graphs' that contain an edge referring to a non-existent vertex. This helps to liberate APIs of existing graph libraries from partial functions.


title: The linearity Monad

authors:
Jennifer Paykin
Steve Zdancewic

abstract: 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-linear host language. We implement a modular framework for defining these linear EDSLs in Haskell, allowing both shallow and deep embeddings. To demonstrate the effectiveness of the framework and the linearity monad, we implement languages for file handles, mutable arrays, session types, and quantum computing.


title: Back to the future: time travel in FRP

abstract: 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 limiting the exploration of the past.


title: Algorithmic music in Haskell (invited talk)

abstract: 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 useful both in a pedagogical setting to teach functional programming through the arts and as a tool to create complex pieces of algorithmic music. Kulitta is a framework for automated composition that addresses music at a more abstract level than Euterpea, capturing aspects of musical style through geometric models and probabilistic grammars. Both of these libraries leverage Haskell’s pure functional nature and strong type system to achieve versatile, yet concise designs that allow the creation of diverse and interesting music. Features from these libraries have also been integral in the design of newer systems for natural language processing and artificial intelligence in the musical domain. This talk will explore challenges presented by creating these kinds of domain-specific embedded languages for working with music, and how taking functional approaches to them yields elegant solutions.


title: Ornaments: exploiting parametricity for safer, more automated code refactorization and code reuse (invited talk)

abstract: 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 need code to be refactored or adapted to be reused in a slightly different context. While the type system is considerably helpful in these situations, by automatically locating type-inconsistent program points or incomplete pattern matchings, this process could be made safer and more automated by further exploiting parametricity. We propose a posteriori program abstraction as a principle for such code transformations.


title: Well-typed music does not sound wrong (experience report)

authors:
Dmitrij Szamozvancev
Michael B. Gale

abstract: 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 checking the correctness of musical pieces in terms of voice leading, harmony, and structure. Haskell's recent additions to the type-system now enable us to perform such analysis statically.


title: A tale of two provers: verifying monoidal string matching in liquid Haskell and Coq

authors:
Niki Vazou
Leonidas Lampropoulos
Jeff Polakow

abstract: 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 properties, Haskell terms to express proofs of these properties, and Liquid Haskell to check the proofs. We evaluate Liquid Haskell as a theorem prover by replicating our 1428 LoC proof in a dependently-typed language (Coq - 1136 LoC). Finally, we compare both proofs, uncovering the relative advantages and disadvantages of the two provers.


title: Using Coq to write fast and correct Haskell

authors:
John Wiegley
Benjamin Delaware

abstract: 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 main properties of the algorithm.


title: Improving STM performance with transactional structs

authors:
Ryan Yates
Michael L. Scott

abstract: 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 structures suffer unfortunate bloat in the implementation due to an extra level of indirection for mutable references as well as the inability to express unboxed mutable transactional values. We address these deficiencies by introducing TStruct to the GHC run-time system, allowing strict unboxed transactional values as well as mutable references without an extra indirection. Using TStruct we implement several data structures, discuss their design, and provide benchmark results on a large multicore machine. Our benchmarks show that concurrent data structures built with TStruct out-scale and out-perform their TVar-based equivalents.


title: Assessing the quality of evolving Haskell systems by measuring structural inequality

authors:
Sander Kamps
Bastiaan Heeren
Johan Jeuring

abstract:
Software metrics are used to measure the quality of a software system, and to understand the evolution of the system's quality over time. In this paper we report on an empirical study that investigates whether structural degradation in Haskell systems is related to decreasing software quality. For our study we use three metrics that measure internal attributes at the level of Haskell modules: intra-modular complexity (cohesion), inter-modular complexity (coupling), and module size. For these metrics, we calculate the Gini coefficient, which is a measure of the inequality in a distribution of values within a certain population, and the deviation of the population's central tendency from an empirically established ideal value. We develop a method to track the evolution, and measure the correlation between the calculated system-level information and post-release defects.

The results show that: (1) post-release defects are significantly correlated with the degree of inequality between the size of modules, (2) the inequality measure is able to indicate significant structural shifts in Haskell source code, and (3) the deviation of a population's central tendency from an ideal value can serve as a benchmark to evaluate the structural characteristics of a Haskell system. The results, however, do not show that a combined measure for inequality and ideal value deviation increases the ability to indicate the defect proneness of Haskell source code.


title: Stitch: the sound type-indexed type checker (functional pearl)

abstract: A classic example of the power of generalized algebraic datatypes (GADTs) to verify a delicate implementation is the type-indexed expression AST. This functional pearl refreshes this example, casting it in modern Haskell using many of GHC's bells and whistles. The Stitch interpreter is a full executable interpreter, with a parser, type checker, common-subexpression elimination, and a REPL. Making heavy use of GADTs and type indices, the Stitch implementation is clean Haskell code and serves as an existence proof that Haskell's type system is advanced enough for the use of fancy types in a practical setting. The paper focuses on guiding the reader through these advanced topics, enabling them to adopt the techniques demonstrated here.


title: Scripted signal functions

abstract: Programming time-dependent signals like animations involves expressing both continuous and discrete changes in signal values. The method of functional reactive programming (FRP) represents this simply and effectively as discrete modes of an otherwise continuous signal. In variants of FRP based on arrows, programs are composed not of signals but rather functions on signals. Accordingly, these signal functions can switch between discrete modes of operation. However, the literature emphasizes expressions of mode switching that are unnecessarily limited. An analysis of their limitations indicates the need for two new, primitive transformations of signal functions. These transformations help to define a monad that represents signal function modes, and this allows programmers to express switching in an imperative, script-like style. This scripting interface gains flexibility and power from several novel operations, including a general-purpose mapping between modes and a combination that mixes two concurrent modes into one. We demonstrate its usefulness with several examples.


title: Describing microservices using modern Haskell (experience report)

authors:
Alejandro Serrano
Flavio Corpa

abstract:
We present Mu, a domain specific language to describe and develop microservices in Haskell. At its core, Mu provides a type level representation of schemas, which we leverage in various ways. These schemas can be automatically imported from industry-standard interface definition languages.

Mu uses many of the type level extensions to GHC, and techniques such as (data type) generic programming and attribute grammars. Apart from the description of the library, we discuss a series of shortcomings in current GHC/Haskell, mostly related to the friendliness of the exposed library interface once complex types enter the scene.


title: Type your matrices for great good: a Haskell library of typed matrices and applications (functional pearl)

authors:
Armando Santos
José N. Oliveira

abstract: We study a simple inductive data type for representing correct-by-construction matrices. Despite its simplicity, it can be used to implement matrix-manipulation algorithms efficiently and safely, performing in some cases faster than existing alternatives even though the algorithms are written in a direct and purely functional style. A rich collection of laws makes it possible to derive and optimise these algorithms using equational reasoning, avoiding the notorious off-by-one indexing errors when fiddling with matrix dimensions. We demonstrate the usefulness of the data type on several examples, and highlight connections to related topics in category theory.


title: Eliminating bugs with dependent Haskell (experience report)

abstract: Using dependent types in production code is a practical way to eliminate errors. While there are many examples of using dependent Haskell to prove invariants about code, few of these are applied to large scale production systems. Critics claim that dependent types are only useful in toy examples and that they are impractical for use in the real world. This experience report analyzes real world examples where dependent types have enabled us to find and eliminate bugs in production Haskell code.


title: Staged sums of products

authors:
Matthew Pickering
Andres Löh
Nicolas Wu

abstract: Generic programming libraries have historically traded efficiency in return for convenience, and the generics-sop library is no exception. It offers a simple, uniform, representation of all datatypes precisely as a sum of products, making it easy to write generic functions. We show how to finally make generics-sop fast through the use of staging with Typed Template Haskell.


title: Effect handlers in Haskell, evidently

authors:
Ningning Xie
Daan Leijen

abstract: Algebraic effect handlers offer an alternative to monads to incorporate effects in Haskell. In recent work Xie _et al._ show how to give semantics to effect handlers in terms of plain polymorphic lambda calculus through _evidence translation_. Besides giving precise semantics, this translation also allows for potentially more efficient implementations. Here we present the first implementation of this technique as a library for effect handlers in Haskell. We show how the design naturally leads to a concise effect interface and how evidence translation enables evaluating _tail resumptive_ operations _in-place_. We give detailed benchmark results where our library performs well with respect to other approaches.


title: Composing effects into tasks and workflows

authors:
Yves Parès
Jean-Philippe Bernardy
Richard A. Eisenberg

abstract:
Data science applications tend to be built by composing tasks: discrete manipulations of data. These tasks are arranged in directed acyclic graphs, and many frameworks exist within the data science community supporting such a structure, which is called a workflow. In realistic applications, we want to be able to both analyze a workflow in the absence of data, and to execute the workflow with data.

This paper combines effect handlers with arrow-like structures to abstract out data science tasks. This combination of techniques enables a modular design of workflows. Additionally, these workflows can both be analyzed prior to running (e.g., to provide early failure) and run conveniently. Our work is directly motivated by real-world scenarios, and we believe that our approach is applicable to new data science and machine learning applications and frameworks.


title: A graded Monad for deadlock-free concurrency (functional pearl)

authors:
Andrej Ivašković
Alan Mycroft

abstract: We present a new type-oriented framework for writing shared memory multithreaded programs that the Haskell type system guarantees are deadlock-free. The implementation wraps all concurrent computation inside a graded monad and assumes a total order is defined between locks. The grades within the type of such a computation specify which locks it acquires and releases. This information is drawn from an algebra that ensures that types can, in principle, be inferred in polynomial time.


title: Finger trees explained anew, and slightly simplified (functional pearl)

abstract: We explicitly motivate the subtle intricacies of Hinze and Paterson's Finger Tree datastructure, by step-wise refining a naive implementation. The result is a new explanation of how Finger Trees work and why they have the particular structure they have, and also a small simplification of the original implementation.


title: Towards secure IoT programming in Haskell

authors:
Nachiappan Valliappan
Robert Krook
Alejandro Russo
Koen Claessen

abstract: IoT applications are often developed in programming languages with low-level abstractions, where a seemingly innocent mistake might lead to severe security vulnerabilities. Current IoT development tools make it hard to identify these vulnerabilities as they do not provide end-to-end guarantees about how data flows within and between appliances. In this work we present Haski, an embedded domain specific language in Haskell (eDSL) for secure programming of IoT devices. Haski enables developers to write Haskell programs that generate C code without falling into many of C’s pitfalls. Haski is designed after the synchronous programming language Lustre, and sports a backwards compatible information-flow control extension to restrict how sensitive data is propagated and modified within the application. We present a novel eDSL design which uses recursive monadic bindings and allows a natural use of functions and pattern-matching in Haskell to write Haski programs. To showcase Haski, we implement a simple smart house controller where communication is done via low-energy Bluetooth on Zephyr OS.


title: Chesskell: a two-player game at the type level

authors:
Toby Bailey
Michael B. Gale

abstract: Extensions to Haskell's type system, as implemented in GHC, have given developers more tools to express the domain-specific rules and invariants of their programs in types. For these extensions to see mainstream adoption, their use in complex applications has to be practical. We present Chesskell, an EDSL for describing Chess games where a type-level model of the full FIDE ruleset prevents us from expressing games with invalid moves. Our work highlights current limitations when using GHC to express such complex rules due to the resulting memory usage and compile times, which we report on. We further present some approaches for working around those limitations.


title: Evaluating linear functions to symmetric monoidal categories

authors:
Jean-Philippe Bernardy
Arnaud Spiwack

abstract:
A number of domain specific languages, such as circuits or data-science workflows, are best expressed as diagrams of boxes connected by wires. Unfortunately, functional languages have traditionally been ill-equipped to embed this sort of languages. The Arrow abstraction is an approximation, but we argue that it does not capture the right properties.

A faithful abstraction is Symmetric Monoidal Categories (SMCs), but, so far, it hasn't been convenient to use. We show how the advent of linear typing in Haskell lets us bridge this gap. We provide a library which lets us program in SMCs with linear functions instead of SMC combinators. This considerably lowers the syntactic overhead of the EDSL to be on par with that of monadic DSLs. A remarkable feature of our library is that, contrary to previously known methods for categories, it does not use any metaprogramming.


title: Seeking stability by being lazy and shallow: lazy and shallow instantiation is user friendly

authors:
Gert-Jan Bottu
Richard A. Eisenberg

abstract:
Designing a language feature often requires a choice between several, similarly expressive possibilities. Given that user studies are generally impractical, we propose using stability as a way of making such decisions. Stability is a measure of whether the meaning of a program alters under small, seemingly innocuous changes in the code (e.g., inlining).

Directly motivated by a need to pin down a feature in GHC/Haskell, we apply this notion of stability to analyse four approaches to the instantiation of polymorphic types, concluding that the most stable approach is lazy (instantiate a polytype only when absolutely necessary) and shallow (instantiate only top-level type variables, not variables that appear after explicit arguments).


title: Graded monads and type-level programming for dependence analysis

authors:
Finnbar Keating
Michael B. Gale

abstract: Programmers make assumptions about the order of memory operations, which are not captured in the operations' types and therefore cannot be enforced statically by a compiler. This can lead programmers to accidentally violate those assumptions if they are not careful. To address this issue, we encode the memory locations that are accessed by a given computation using a graded monad. We use the data flow dependencies which arise from this to construct a type-level graph that we analyse to automatically order the computations so that no dependencies are violated. This also allows for computations which have no dependencies on each other to be run concurrently.


title: Deadlock-free session types in linear Haskell

authors:
Wen Kokke
Ornela Dardha

abstract:
Priority Sesh is a library for session-typed communication in Linear Haskell which offers strong compile-time correctness guarantees. Priority Sesh offers two deadlock-free APIs for session-typed communication. The first guarantees deadlock freedom by restricting the process structure to trees and forests. It is simple and composeable, but rules out cyclic structures. The second guarantees deadlock freedom via priorities, which allows the programmer to safely use cyclic structures as well.

Our library relies on Linear Haskell to guarantee linearity, which leads to easy-to-write session types and more idiomatic code, and lets us avoid the complex encodings of linearity in the Haskell type system that made previous libraries difficult to use.


title: Express: applications of dynamically typed Haskell expressions

abstract: This paper presents Express, a library for manipulating dynamically typed Haskell expressions involving function application and variables. Express works as a wrapper around the Data.Dynamic module and provides additional features such as: explicit encoding of function applicaion thus delayed application between values, support for variable placeholders and expression matching. This paper shows these additions make this library useful in generating program specifications, automated testing and program synthesis.


title: Safe mutation with algebraic effects

authors:
Hashan Punchihewa
Nicolas Wu

abstract: It can be difficult to write safe concurrent programs which use shared mutable state. Subtle mistakes can lead to data races that manifest as unexpected program behaviour. The prevailing approaches to solving this dilemma are to either eschew mutable state altogether, or design bespoke languages that prevent data races by design. This article introduces a third approach by showing how safe mutation can be integrated into a mainstream functional programming language with algebraic effects. This article produces a framework that tracks the use of mutable state and guarantees data race freedom at compile time.


title: Haskell⁻¹: automatic function inversion in Haskell

authors:
Finn Teegen
Kai-Oliver Prott
Niels Bunkenburg

abstract: We present an approach for automatic function inversion in Haskell. The inverse functions we generate are based on an extension of Haskell's computational model with non-determinism and free variables. We implement this functional logic extension of Haskell via a monadic lifting of functions and type declarations. Using inverse functions, we additionally show how Haskell's pattern matching can be augmented with support for functional patterns, which enable arbitrarily deep pattern matching in data structures. Finally, we provide a plugin for the Glasgow Haskell Compiler to seamlessly integrate inverses and functional patterns into the language, covering almost all of the Haskell2010 language standard.


title: Practical normalization by evaluation for EDSLs

authors:
Nachiappan Valliappan
Alejandro Russo
Sam Lindley

abstract: Embedded domain-specific languages (eDSLs) are typically implemented in a rich host language, such as Haskell, using a combination of deep and shallow embedding techniques. While such a combination enables programmers to exploit the execution mechanism of Haskell to build and specialize eDSL programs, it blurs the distinction between the host language and the eDSL. As a consequence, extension with features such as sums and effects requires a significant amount of ingenuity from the eDSL designer. In this paper, we demonstrate that Normalization by Evaluation (NbE) provides a principled framework for building, extending, and customizing eDSLs. We present a comprehensive treatment of NbE for deeply embedded eDSLs in Haskell that involves a rich set of features such as sums, arrays, exceptions and state, while addressing practical concerns about normalization such as code expansion and the addition of domain-specific features.


title: Design patterns for parser combinators (functional pearl)

authors:
Jamie Willis
Nicolas Wu

abstract: Parser combinators are a popular and elegant approach for parsing in functional languages. The design and implementation of such libraries are well discussed, but having a well-designed library is only one-half of the story. In this paper we explore several reusable approaches to writing parsers in combinator style, focusing on easy to apply patterns to keep parsing code simple, separated, and maintainable.


title: A totally predictable outcome: an investigation of traversals of infinite structures

abstract: Functors with an instance of the Traversable type class can be thought of as data structures which permit a traversal of their elements. This has been made precise by the correspondence between traversable functors and finitary containers (also known as polynomial functors) -- established in the context of total, necessarily terminating, functions. However, the Haskell language is non-strict and permits functions that do not terminate. It has long been observed that traversals can at times in fact operate over infinite lists, for example in distributing the Reader applicative. The result of such a traversal remains an infinite structure, however it nonetheless is productive -- i.e. successive amounts of finite computation yield either termination or successive results. To investigate this phenomenon, we draw on tools from guarded recursion, making use of equational reasoning directly in Haskell.


title: Liquid proof macros

authors:
Henry Blanchette
Niki Vazou
Leonidas Lampropoulos

abstract:
Liquid Haskell is a popular verifier for Haskell programs, leveraging the power of SMT solvers to ease users' burden of proof. However, this power does not come without a price: convincing Liquid Haskell that a program is correct often necessitates giving hints to the underlying solver, which can be a tedious and verbose process that sometimes requires intricate knowledge of Liquid Haskell's inner workings.

In this paper, we present Liquid Proof Macros, an extensible metaprogramming technique and framework for simplifying the development of Liquid Haskell proofs. We describe how to leverage Template Haskell to generate Liquid Haskell proof terms, via a tactic-inspired DSL interface for more concise and user-friendly proofs, and we demonstrate the capabilities of this framework by automating a wide variety of proofs from an existing Liquid Haskell benchmark.


title: Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs

authors:
Jesper Cockx
Orestis Melkonian
Lucas Escot
James Chapman
Ulf Norell

abstract:
Modern dependently typed languages such as Agda can be used to statically enforce the correctness of programs. However, they still lack the large ecosystem of a more popular language like Haskell. To combine the strength of both approaches, we present agda2hs, a tool that translates an expressive subset of Agda to readable Haskell, erasing dependent types and proofs in the process. Thanks to Agda's support for erasure annotations, this process is both safe and transparent to the user. Compared to other tools for program extraction, agda2hs uses a syntax that is already familiar to functional programmers, allows for both intrinsic and extrinsic approaches to verification, and produces Haskell code that is easy to read and audit by programmers with no knowledge of Agda.

We present a practical use case of agda2hs at IOG to verify properties of a program generator. While both agda2hs and its ecosystem are still young, our experiences so far show that this is a viable approach to make verified functional programming available to a broader audience.

This paper is a literate Agda script, hence all rendered (Agda) code has been typechecked.


title: Open transactional actions: interacting with non-transactional resources in STM Haskell

authors:
Jonathas Augusto de Oliveira Conceição
André Rauber Du Bois
Samuel da Silva Feitosa
Gerson Geraldo Homrich Cavalheiro
Rodrigo Geraldo Ribeiro

abstract: This paper addresses the problem of accessing external resources from inside transactions in STM Haskell, and for that purpose introduces a new abstraction called Open Transactional Actions (OTAs) that provides a framework for wrapping non-transactional resources in a transactional layer. OTAs allow the programmer to access resources through IO actions, from inside transactions, and also to register commit and abort handlers: the former are used to make the accesses to resources visible to other transactions at commit time, and the latter to undo changes in the resource if the transaction has to roll back. OTAs, once started, are guaranteed to be executed completely before the hosting transaction can be aborted, guarantying that if a resource is accessed, its respective commit and abort actions will be properly registered. We believe that OTAs could be used by expert programmers to implement useful system libraries and also to give a transactional semantics to fast linearizable data structures, i.e., transactional boosting. As a proof of concept, we present examples that use OTAs to implement transactional file access and transactional boosted data types that are faster than pure STM Haskell in most cases.


title: Investigating magic numbers: improving the inlining heuristic in the Glasgow Haskell Compiler

authors:
Celeste Hollenbeck
Michael F. P. O'Boyle
Michel Steuwer

abstract:
Inlining is a widely studied compiler optimization that is particularly important for functional languages such as Haskell and OCaml. The Glasgow Haskell Compiler (GHC) inliner is a heuristic of such complexity, however, that it has not significantly changed for nearly 20 years. It heavily relies on hard-coded numeric constants, or magic numbers, based on out-of-date intuition. Dissatisfaction with inlining performance has led to the widespread use of inlining pragmas by programmers.

In this paper, we present an in-depth study of the effect of inlining on performance in functional languages. We specifically focus on the inlining behavior of GHC and present techniques to systematically explore the space of possible magic number values, or configurations, and evaluate their performance on a set of real-world benchmarks where inline pragmas are present. Pragmas may slow down individual programs, but on average improve performance by 10%. Searching for the best configuration on a per-program basis increases this performance to an average of 27%. Searching for the best configuration for each program is, however, expensive and unrealistic, requiring repeated compilation and execution. This paper determines a new single configuration that gives a 22% improvement on average across the benchmarks. Finally, we use a simple machine learning model that predicts the best configuration on a per-program basis, giving a 26% average improvement.


title: Partial type constructors in practice

authors:
Apoorv Ingle
Alex Hubers
J. Garrett Morris

abstract: Type constructors in functional programming languages are total: a Haskell programmer can equally readily construct lists of any element type. In practice, however, not all applications of type constructors are equally sensible: collections may only make sense for orderable elements, or embedded DSLs might only make sense for serializable return types. Jones et al. proposed a theory of partial type constructors, which guarantees that type applications are sensible, and extends higher-order abstractions to apply equally well to partial and total type constructors. This paper evaluates the practicality of partial type constructors, in terms of both language design and implementation. We extend GHC, the most widely used Haskell compiler, with support for partial type constructors, and test our extension on the compiler itself and its libraries. We show that introducing partial type constructors has a minimal impact on most code, but raises important questions in language and library design.


title: Coinduction inductively: mechanizing coinductive proofs in Liquid Haskell

authors:
Lykourgos Mastorou
Nikolaos Papaspyrou
Niki Vazou

abstract: Liquid Haskell is an inductive verifier that cannot reason about codata. In this work we present two alternative approaches, namely indexed and constructive coinduction, to consistently encode coinductive proofs in Liquid Haskell. The intuition is that indices can be used to enforce the base case in the setting of classical logic and the guardedness check in the constructive proofs. We use our encodings to machine check 10 coinductive proofs, about unary and binary predicates on infinite streams and lists, showcasing how an inductive verifier can be used to check coinductive properties of Haskell code.


title: Embedded pattern matching

authors:
Trevor L. McDonell
Joshua D. Meredith
Gabriele Keller

abstract: Haskell is a popular choice for hosting deeply embedded languages. A recurring challenge for these embeddings is how to seamlessly integrate user defined algebraic data types. In particular, one important, convenient, and expressive feature for creating and inspecting data—pattern matching—is not directly available on embedded terms. We present a novel technique, embedded pattern matching, which enables a natural and user friendly embedding of user defined algebraic data types into the embedded language, and allows programmers to pattern match on terms in the embedded language in much the same way they would in the host language.


title: How to safely use extensionality in Liquid Haskell

authors:
Niki Vazou
Michael Greenberg

abstract:
Refinement type checkers are a powerful way to reason about functional programs. For example, one can prove properties of a slow, specification implementation and port the proofs to an optimized pure implementation that behaves the same. But to reason about higher-order programs, we must reason about equalities between functions: we need a consistent encoding of functional extensionality.

A natural but naive phrasing of the functional extensionality axiom (funExt) is inconsistent in refinement type systems with semantic subtyping and polymorphism: if we assume funExt, then we can prove false. We demonstrate the inconsistency and develop a new approach to equality in Liquid Haskell: we define a propositional equality in a library we call PEq. Using PEq avoids the inconsistency while proving useful equalities at higher types; we demonstrate its use in several case studies. We validate PEq by building a model and developing its metatheory. Additionally, we prove metaproperties of PEq inside Liquid Haskell itself using an unnamed folklore technique, which we dub 'classy induction'.


title: Oregano: staging regular expressions with Moore Cayley fusion

authors:
Jamie Willis
Nicolas Wu
Tom Schrijvers

abstract:
Regular expressions are a tool for recognising regular languages, historically implemented using derivatives or non-deterministic finite automata. They are convenient for many light-weight parsing workloads, but their traditional formulation only lends them to matching text, not returning fully-structured results. This contrasts with other forms of parsing, where the aim is to extract meaningful data, for example abstract syntax trees. Yet, most regular expression libraries do not support this useful output, and those that do are often slower, and backed by parser combinator libraries.

This paper presents Oregano, a redesign of regular expressions to make use of Moore machines as the underlying machinery; this way the regular expression matcher can produce results. We further show how to produce heterogeneous results, providing a classic applicative interface. To make this representation performant, we leverage the relationship between Cayley representations, continuation-passing style, and staged meta-programming to generate performant code for regular expression matching with fully-structured results.


title: The Essence of Reactivity

authors:
Ivan Perez
Frank Dedden

abstract: Reactive programming, functional reactive programming, event-based programming, stream programming, and temporal logic all share an underlying commonality: values can vary over time. These languages differ in multiple ways, including the nature of time itself (e.g., continuous or discrete, dense or sparse, implicit or explicit), on how much of the past and future can be referenced, on the kinds of values that can be represented, as well as the mechanisms used to evaluate expressions or formulas. This paper presents a series of abstractions that capture the essence of different forms of time variance. By separating the aspects that differentiate each family of formalisms, we can better express the commonalities and differences between them. We demonstrate our work with a prototype in Haskell that allows us to write programs in terms of a generic interface that can be later instantiated to different abstractions depending on the desired target.


title: This Is Driving Me Loopy: Efficient Loops in Arrowized Functional Reactive Programs

abstract:
Arrowized Functional Reactive Programming (AFRP) is one approach to writing reactive programs declaratively, based on the arrows abstraction in Haskell. While AFRP elegantly expresses the relationships between inputs and outputs of a reactive system, na'ive implementations suffer from poor performance. In particular, the loop combinator depends on lazy semantics: this inflicts the overheads of lazy evaluation and simultaneously prevents existing optimisation techniques from being applied to it.

We present a novel program transformation which utilises the Arrow and ArrowLoop laws to transform typical uses of loop into restricted forms that have an execution order that is known at compile-time and therefore can be executed strictly. We evaluate the performance gained from our transformations and prove that the transformations are correct.


title: Don't Go Down the Rabbit Hole: Reprioritizing Enumeration for Property-Based Testing

authors:
Segev Elazar Mittelman
Aviel Resnick
Ivan Perez
Alwyn E. Goodloe
Leonidas Lampropoulos

abstract: In our implementation, we integrate a state-of-the-art enumeration-based property-based testing framework, LazySearch, with a state-of-the-art combinatorial testing tool, NIST’s ACTS, and demonstrate how it can significantly speed up the effectiveness of testing—up to more than 20× in the case of a prior System F case study from the literature.


title: Effect Handlers for Programmable Inference

authors:
Minh Nguyen
Roly Perera
Meng Wang
Steven Ramsay

abstract:
Inference algorithms for probabilistic programming are complex imperative programs with many moving parts. Efficient inference often requires customising an algorithm to a particular probabilistic model or problem, sometimes called inference programming. Most inference frameworks are implemented in languages that lack a disciplined approach to side effects, which can result in monolithic implementations where the structure of the algorithms is obscured and inference programming is hard. Functional programming with typed effects offers a more structured and modular foundation for programmable inference, with monad transformers being the primary structuring mechanism explored to date.

This paper presents an alternative approach to inference programming based on algebraic effects. Using effect signatures to specify the key operations of the algorithms, and effect handlers to modularly interpret those operations for specific variants, we develop two abstract algorithms, or inference patterns, representing two important classes of inference: Metropolis-Hastings and particle filtering. We show how our approach reveals the algorithms’ high-level structure, and makes it easy to tailor and recombine their parts into new variants. We implement the two inference patterns as a Haskell library, and discuss the pros and cons of algebraic effects vis-à-vis monad transformers as a structuring mechanism for modular imperative algorithm design.


title: Haskell Library for Safer Virtual Machine Introspection (Experience Report)

authors:
Takato Otsuka
Hideya Iwasaki

abstract: Virtual machine introspection (VMI) is a technique for inspecting a virtual machine from the outside, typically to analyze the operating system (guest OS) running on it. LibVMI is a C library for VMI and provides APIs for accessing guest OS's memory. However, in using LibVMI APIs directly in C, the programmer must compute target addresses in the kernel memory and then access them with their exact bit widths and types. This is an enormous burden for the programmer and is prone to introducing statically undetected but fatal errors. We create HaVMI, a Haskell library that facilitates VMI programming. HaVMI provides meta-functions for compile-time code generation by Template Haskell. These meta-functions make it easy to write safer VMI programs. HaVMI uses Haskell language features to detect the programmer's errors statically.


title: An Exceptional Actor System (Functional Pearl)

authors:
Patrick Redmond
Lindsey Kuper

abstract:
The Glasgow Haskell Compiler is known for its feature-laden runtime system (RTS), which includes lightweight threads, asynchronous exceptions, and a slew of other features. Their combination is powerful enough that a programmer may complete the same task in many different ways --- some more advisable than others.

We present a user-accessible actor framework hidden in plain sight within the RTS and demonstrate it on a classic example from the distributed systems literature. We then extend both the framework and example to the realm of dynamic types. Finally, we raise questions about how RTS features intersect and possibly subsume one another, and suggest that GHC can guide good practice by constraining the use of some features.


title: HasTEE: Programming Trusted Execution Environments with Haskell

authors:
Abhiroop Sarkar
Robert Krook
Alejandro Russo
Koen Claessen

abstract:
Trusted Execution Environments (TEEs) are hardware enforced memory isolation units, emerging as a pivotal security solution for security-critical applications. TEEs, like Intel SGX and ARM TrustZone, allow the isolation of confidential code and data within an untrusted host environment, such as the cloud and IoT. Despite strong security guarantees, TEE adoption has been hindered by an awkward programming model. This model requires manual application partitioning and the use of error-prone, memory-unsafe, and potentially information-leaking low-level C/C++ libraries.

We address the above with HasTEE, a domain-specific language (DSL) embedded in Haskell for programming TEE applications. HasTEE includes a port of the GHC runtime for the Intel-SGX TEE.HasTEE uses Haskell’s type system to automatically partition an application and to enforce Information Flow Control on confidential data. The DSL, being embedded in Haskell, allows for the usage of higher-order functions, monads, and a restricted set of I/O operations to write any standard Haskell application. Contrary to previous work, HasTEE is lightweight, simple, and is provided as a simple security library; thus avoiding any GHC modifications. We show the applicability of HasTEE by implementing case studies on federated learning, an encrypted password wallet, and a differentially-private data clean room.


title: falsify: Internal Shrinking Reimagined for Haskell

abstract: In unit testing we apply the function under test to known inputs and check for known outputs. By contrast, in property based testing we state properties relating inputs and outputs, apply the function to random inputs, and verify that the property holds; if not, we found a bug. Randomly generated inputs tend to be large and should therefore be minimised. Traditionally this is done with an explicitly provided shrinker, but in this paper we propose a way to write generators that obsoletes the need to write a separate shrinker. Inspired by the Python library Hypothesis, the approach can work even across monadic bind. Compared to Hypothesis, our approach is more suitable to the Haskell setting: it depends on a minimal set of core principles, and handles generation and shrinking of infinite data structures, including functions.


title: The Evolution of Effects (Keynote)

abstract:
Functional programming has been celebrated for its promise of pure functions, delivering referential transparency and elegant reasoning about programs. However, real-world applications are not pure, and necessitate interaction with the outside world, introducing computational effects such as IO, state, and exceptions. The journey to harmonize these seemingly contradictory paradigms has led to a fascinating evolution of effectful programming in Haskell.

The introduction of monads as a practical programming tool was a pivotal discovery, enabling controlled sequencing of effectful computations and addressing the challenge of handling side effects in a pure language. However, it soon became evident that the lack of modularity in composing effects using monads posed a limitation to effectful programming. To overcome this obstacle, monad transformers emerged as a solution, providing a composable manner of building effects on top of one another.

More recent advancements have led to algebraic effects as an alternative framework that is easy to extend, particularly as domain-specific languages crafted to work in specific contexts. Nevertheless, these effects are not without quirks and limitations, leading to the development of higher-order effects. These higher-order effects extend the capabilities of algebraic effects, providing greater flexibility for expressing effectful computations, while also shedding light on the connection between the monad approach and the algebraic approach to effects.

This talk will survey the historical milestones that have shaped the landscape of effectful programming in Haskell, exploring the transition from monads to monad transformers and the emergence of algebraic and higher-order effects.


title: Haskell for Choice-Based Learning (Keynote)

abstract:
Machine learning has achieved many successes during the past decades, spanning domains of game-playing, protein folding, competitive programming, and many others. However, while there have been major efforts in building programming techniques and frameworks for machine learning programming, there has been very little study of general language design for machine learning programming.

We pursue such a study in this talk, focusing on choice-based learning, particularly where choices are driven by optimizations. This includes widely-used decision-making models and techniques (e.g., Markov decision processes or gradient descent) which provide frameworks for describing systems in terms of choices (e.g., actions or parameters) and their resulting feedback as losses (dually, rewards).

We propose and give evidence for the following thesis: languages for choice-based learning can be obtained by combining two paradigms, algebraic effects and handlers, and the selection monad. We provide a prototype implementation as a Haskell library and present a variety of programming examples for choice-based learning: stochastic gradient descent, hyperparameter tuning, generative adversarial networks, and reinforcement learning.


title: MicroHs: A Small Compiler for Haskell

abstract: MicroHs is a compiler for Haskell2010. It translates Haskell to SKI style combinators via λ-calculus. The runtime system is quite small with few dependencies.


title: Liquid Amortization: Proving Amortized Complexity with LiquidHaskell (Functional Pearl)

abstract: Formal reasoning about the time complexity of algorithms and data structures is usually done in interactive theorem provers like Isabelle/HOL. This includes reasoning about amortized time complexity which looks at the worst case performance over a series of operations. However, most programs are not written within a theorem prover and thus use the data structures of the production language. To verify the correctness it is necessary to translate the data structures from the production language into the language of the prover. Such a translation step could introduce errors, for example due to a mismatch in features between the two languages. We show how to prove amortized complexity of data structures directly in Haskell using LiquidHaskell. Besides skipping the translation step, our approach can also provide a didactic advantage. Learners do not have to learn an additional language for proofs and can focus on the new concepts only. For this paper, we do not assume prior knowledge of amortized complexity as we explain the concepts and apply them in our first case study, a simple stack with multipop. Moving to more complicated (and useful) data structures, we show that the same technique works for binomial heaps which can be used to implement a priority queue. We also prove amortized complexity bounds for Claessen’s version of the finger tree, a sequence-like data structure with constant-time cons/uncons on either end. Finally we discuss the current limitations of LiquidHaskell that made certain versions of the data structures not feasible.


title: Making a Curry Interpreter using Effects and Handlers

authors:
Niels Bunkenburg
Nicolas Wu

abstract: Despite the intended use for prototyping or as a first step towards giving semantics to a new programming language, interpreters are often monolithic and difficult to extend. Higher-order effects and handlers promise modular composition of handlers and semantics; in practice, however, they have been mostly applied to toy examples. We present an approach that successfully combines algebraic, scoped, and latent effects into a handler pipeline for interpreting the functional logic programming language Curry. We show which effects make up Curry, discuss the infrastructure needed to combine effects of different classes and shed light on how these effects interact in order to lessen the barrier to entry for using effects in practical projects.


title: Calculating Compilers Effectively (Functional Pearl)

authors:
Zac Garby
Graham Hutton
Patrick Bahr

abstract: Much work in the area of compiler calculation has focused on pure languages. While this simplifies the reasoning, it reduces the applicability. In this article, we show how an existing compiler calculation methodology can be naturally extended to languages with side effects. We achieve this by exploiting an algebraic approach to effects, which keeps the reasoning simple and provides flexibility in how effects are interpreted. To make the ideas accessible we only use elementary functional programming techniques.


title: Functional Reactive Programming, Rearranged

authors:
Finnbar Keating
Michael B. Gale

abstract: At present, the most efficient implementations of Arrowized Functional Reactive Programming (AFRP), such as Scalable FRP (SFRP), do not support the loop combinator. This prevents us from expressing fundamental programs in such implementations, which limits AFRP’s use in domains where both performance and expressivity are required. We introduce Oxbow, which extends SFRP with support for the loop combinator by leveraging an improved variant of the rearrange technique. In benchmarks, Oxbow performs at least 2.2x better than Yampa, an AFRP implementation that supports the loop combinator.


title: Welcome to the Parti(tioning) (Functional Pearl): Using Rewrite Rules and Specialisation to Partition Haskell Programs

authors:
Robert Krook
Samuel Hammersberg

abstract: Writing distributed applications is hard, as the programmer needs to describe the communication protocol between the different endpoints. If this is not done correctly, we can introduce bugs such as deadlocks and data races. Tierless and choreographic programming models aim to make this easier by describing the interactions of every endpoint in a single compilation unit. When such a program is compiled, ideally, a single endpoint is projected and the code for the other endpoints is removed. This leads to smaller binaries with fewer dependencies, and is called program partitioning. In this pearl, we show how we can use rewrite rules and specialisation to get GHC to partition our Haskell programs (almost) for free, if they are written using the Haste App or HasChor framework. As an example of why partitioning is useful, we show how an example application can be more easily built and deployed after being partitioned.


title: Cloaca: A Concurrent Hardware Garbage Collector for Non-strict Functional Languages

authors:
Craig R. Ramsay
Robert J. Stewart

abstract: Most functional language runtime systems context switch between executing user code and a non-concurrent garbage collector (GC), exposing GC latency to overall wall-clock time. Recent concurrent software-based GCs reduce these latencies, but wall-clock times are instead increased due to their synchronisation and write barrier overheads, by as much as 21%. This GC overhead is exacerbated further for pure non-strict languages like Haskell, due to the abundance of allocations for storing immutable data structures and closures. This paper presents Cloaca, an FPGA-based hardware implementation of a concurrent, hybrid GC for a pure non-strict functional language. It combines mark-and-sweep tracing and one-bit reference counting. It traces live heap data using hardware-level synchronisation and write barriers, without damaging graph reduction performance. To ensure the correctness of Cloaca, three invariants of its Haskell-based implementation are verified with property-based testing. Despite GHC running on an Intel i7 CPU operating at a x25 higher clock frequency than Cloaca; Cloaca takes, on average, 4.1% of GHC's GC wall-clock time across 14 of 15 benchmarks.


title: Higher Order Patterns for Rewrite Rules

abstract: GHC’s rewrite rules enable programmers to write local program transformation rules for their own functions. The most notable use case are fusion optimizations, which merge multiple traversals of a data structure into one and avoids allocation of intermediate structures. However, GHC’s rewrite rules were too limited to express a rewrite rule that is necessary for proper fusion of the concatMap function in a variant of fusion called stream fusion. We introduce higher order patterns as a simple extension of GHC’s rewrite rules. Higher order patterns substantially broaden the expressiveness of rewrite rules that involve local variables. In particular, they enable the rewriting of concatMap such that it can be properly optimized. We implement a stream fusion framework to replace the existing fusion framework in GHC and evaluate it on GHC’s benchmark suite. Our stream fusion framework with higher order patterns shows an average speedup of 7% compared to our stream fusion framework without it. However, our stream fusion framework is not yet able to match the performance of GHC’s existing fusion framework. Additionally, we show that our higher order patterns can be used to simplify GHC’s existing mechanism for rolling back failed attempts at fusion and, at the same time, solve a problem that prevented proper optimization in one example program. However, evaluating it on GHC’s benchmark suite shows a small regression in performance overall.


title: Controlling Computation Granularity through Fusion in Improving Floating-Point Numbers

authors:
Momoka Saito
Hideya Iwasaki
Hideyuki Kawabata
Tsuneyasu Komiya

abstract: Improving Floating-Point Numbers (IFN) is a numerical computation library for Haskell. It allows the user to directly specify the accuracy of the result, making accurate computation easy. The library's computation process is based on adaptive control of accuracies, which propagates the demands for more accurate values from an expression to its appropriate subexpressions. However, despite its unique features, programs utilizing the IFN library often encounter efficiency issues regarding memory consumption and execution time due to its fine granularity of computations. This paper presents the computational granularity control mechanism through fusion transformation to resolve these problems and proposes two fusion strategies, the maximal fusion and chain fusion. We have successfully implemented a fusion system that automatically applies these strategies through program transformation. Its effectiveness was confirmed through numerical computation programs.


title: Haskelite: A Tracing Interpreter Based on a Pattern-Matching Calculus

authors:
Pedro B. Vasconcelos
Rodrigo Marques

abstract: Many Haskell textbooks explain the evaluation of pure functional programs as a process of stepwise rewriting using equations. However, usual implementation techniques perform program transformations that make producing the corresponding tracing evaluations difficult. This paper presents a tracing interpreter for a subset of Haskell based on the pattern matching calculus of Kahl. We start from a big-step semantics in the style of Launchbury and develop a small-step semantics in the style of Sestoft's machines. This machine is used in the implementation of a step-by-step educational interpreter. We also discuss some implementation decisions and present illustrative examples.


title: Automatic C Bindings Generation for Haskell

authors:
Travis Cardwell
Sam Derbyshire
Edsko de Vries
Dominik Schrempf

abstract:
Interfacing Haskell with C libraries is a common necessity, but the manual creation of bindings is both error-prone and laborious. We present hs-bindgen, a new tool that provides fully automatic generation of Haskell FFI bindings directly from C header files.

We introduce a novel method for describing bindings through binding specifications, providing a compositional method for using bindings for one library in bindings for another. Furthermore, we define a domain-specific language in Haskell to represent C expressions found in C macros, along with a corresponding type inference algorithm, to allow us to generate bindings for functions defined as C macros.


title: A Tale of Two Lambdas: A Haskeller's Journey into OCaml (Keynote)

abstract: After spending a decade focusing mostly on Haskell, I have spent the last three years looking deeply at OCaml. This talk will capture some lessons learned about my work in the two languages and their communities -- how they are similar, how they differ, and how each might usefully grow to become more like the other. I will compare Haskell's purity against OCaml's support for mutation, type classes against modules as abstraction paradigms, laziness against strictness, along with some general thoughts about language philosophy. We'll also touch on the some of the challenges both languages face as open-source products, in need of both volunteers and funding. While some functional programming experience will definitely be helpful, I'll explain syntax as we go -- no Haskell or OCaml knowledge required, as I want this talk to be accessible equally to the two communities.


title: A Clash Course in Solving Sudoku (Functional Pearl)

abstract: Clash is a compiler from Haskell to hardware description. We explore a "Haskell-first" approach to hardware design by building an FPGA Sudoku solver based on a well-known software implementation, showing the step-by-step process of adapting it to hardware. The final code still exhibits the benefits of Haskell's powerful tools for abstraction.


title: The Calculated Typer (Functional Pearl)

authors:
Zac Garby
Patrick Bahr
Graham Hutton

abstract: We present a calculational approach to the design of type checkers, showing how they can be derived from behavioural specifications using equational reasoning. We focus on languages whose semantics can be expressed as a fold, and show how the calculations can be simplified using fold fusion. This approach enables the compositional derivation of correct-by-construction type checkers based on solving and composing fusion preconditions. We introduce our approach using a simple expression language, to which we then add support for exception handling and checked exceptions.


title: Join Points in Practice (Keynote)

abstract:
Eight years ago "Compiling without continuations" introduced the idea of so-called join points as a powerful optimisation tool in a functional language compiler. Since then join points have become more and more deeply entwined in GHC's optimisation passes; for example they are treated specially by the Simplifier and its Occurrence Analyser, and a dedicated pass called Exitification makes a join-point-specific transformation

With the perspective of this experience, I am convinced that any serious functional compiler should use join points (or something equivalent): it's a powerful and re-usable idea. Yet beyond the initial paper, none of what we have learned has appeared in print. In this talk I will share the lessons of the last eight years of using join points in practice in GHC.


title: Staging Automatic Differentiation with Fusion

authors:
Samuel Klumpers
Tom Schrijvers

abstract:
Automatic differentiation (AD) is a family of algorithms with many applications in scientific computing and machine learning. They compute numerical derivatives by interpreting or transforming the source code of numeric expressions. The correctness and efficiency of such AD algorithms has been the subject of much research, in particular that of reverse-mode AD which is particularly efficient for computing large gradients, but the code it generates is highly non-obvious.

In this paper, we build on the earlier approach of van den Berg et al. [Science of Computer Programming, 231 (2024)], reverse-engineering their algorithm in terms of established program transformation techniques from abstract algebra and functional programming. We transform the existing interpreter-based approach into an efficient code generator by means of staging with Template Haskell, and leverage a fold fusion variant for staging and algebraic preservation maps to perform correct-by-construction binding time improvements.

The resulting generated code achieves speedups of a factor of 110.


title: Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)

authors:
Ziyang Liu
Kenneth MacKenzie
Roman Kireev
Michael Peyton Jones
Philip Wadler
Manuel M. T. Chakravarty

abstract:
The Cardano blockchain is the first to use proof of stake, offers native support for multiple currencies and is evolving toward a distributed governance model. It supports smart contracts through Plutus, a language based on System Fω with recursion. About half a dozen languages compile into Plutus, the first of which is Plinth (formerly Plutus Tx) — a language that reuses a subset of the Haskell syntax, and has been in commercial use since 2021.

Our journey building Plinth has been unconventional in a number of ways. First, Plinth programs are written in a subset of Haskell, using standard Haskell syntax and types, which brings a number of advantages. Second, compilation is primarily handled by a GHC plugin, one of the most intricate we are aware of. Third, while some compiler optimizations mirror those in Haskell, others diverge significantly to meet on-chain execution constraints. Fourth, Plutus programs run on an instrumented CEK machine with a formal specification in Agda. This report reflects on our design choices, outlining effective practices, challenges, and key takeaways, with an emphasis on recent advances in the language, compiler, and runtime.


title: Lightweight Testing of Persistent Amortized Time Complexity in the Credit Monad

abstract: Persistent data structures are ubiquitous in functional programming languages and their designers frequently have to reason about amortized time complexity. But proving amortized bounds is difficult in a persistent setting, and pen-and-paper proofs give little assurance of correctness, while a full mechanization in a proof assistant can be too involved for the casual user. In this work, we define a strict domain specific language (DSL) for testing the amortized time complexity of persistent data structures using QuickCheck. Our DSL can give strong evidence of correctness, while imposing low overhead on the user. We have used our DSL to check the amortized time complexity of all lazy data structures in Okasaki's book. As a sign of our approach's effectiveness, we re-discovered a previously unreported gap in the analysis of persistent Finger Trees.


title: Rebound: Efficient, Expressive, and Well-Scoped Binding

authors:
Noé De Santo
Stephanie Weirich

abstract: We introduce the Rebound library that supports well-scoped term representations in Haskell and automates the definition of substitution, alpha-equivalence, and other operations that work with binding structures. The key idea of our design is the use of first-class environments that map variables to expressions in some new scope. By statically tracking scopes, users of this library gain confidence that they have correctly maintained the subtle invariants that stem from using de Bruijn indices. Behind the scenes, Rebound uses environments to optimize the application of substitutions, while providing explicit access to these data structures when desired. We demonstrate that this library is expressive by using it to implement a wide range of language features with sophisticated uses of binding and several different operations that use this abstract syntax. Our examples include pi-forall, a tutorial implementation of a type checker for a dependently-typed programming language. Finally, we benchmark Rebound to understand its performance characteristics and find that it produces faster code than competing libraries.


title: Freer Arrows and Why You Need Them in Haskell

authors:
Grant VanDomelen
Gan Shen
Lindsey Kuper
Yao Li

abstract: Freer monads are a useful structure commonly used in various domains due to their expressiveness. However, a known issue with freer monads is that they are not amenable to static analysis. This paper explores freer arrows, a relatively expressive structure that is amenable to static analysis. We propose several variants of freer arrows. We conduct a case study on choreographic programming to demonstrate the usefulness of freer arrows in Haskell.


title: Total Type Classes

authors:
Robert Weingart
Nicolas Wu

abstract:
In Haskell, type classes can act like functions from types to terms. However, unlike for functions, there is no way for the programmer to ask the compiler to verify that classes pattern-match exhaustively on their arguments, and their usage must always be marked by a constraint even when they are exhaustive.

This paper introduces the notion of total type classes and, more generally, total constraints, which allow the programmer to describe a set of instances whose existence can be verified by inspecting the instance declarations of the class, instead of on a case-by-case basis when a specific instance is demanded. To achieve this functionality, our implementation records the missing constraints during typechecking and then modifies the typechecked program, rewriting it as though the programmer had included the constraints.


title: The Next 700 Block-Based Editors (Keynote)

abstract: Block-based code editors have been adopted widely in classrooms with young learners, yet they are often perceived as inferior compared to the ultimate flexibility of text editors. Beyond blocks, alternatives to manipulating programs as text have been pursued through various structure-editing interfaces. But blocks, text, and structure-editing each have merits. Can’t we all just get along? This talk presents ongoing work which aims to integrate these complementary ways of reading, writing, and maintaining programs. The central element is a novel user interface primitive called ragged blocks (or rocks), which allow nested passages of structured text—like code—to be styled and rendered in ways that suggest alluring possibilities for future programming environments and other GUIs.


title: Coercive Subtyping for Implicit Functorial Programming

authors:
Ryan Doenges
Caden Parajuli
Ayden Lamparski
Ke Wu
Aaron Stump

abstract: Programming with typeclass-defined combinators like fmap allows programs a great deal of generality and concision, but programmers have to explicitly invoke combinators in the right places in order to get their programs to type check. In this paper, we propose inferring these operations using a coercive subtyping discipline and study the metatheory of the resulting algebra of coercions. For functors, we promote the fmap combinator of type (A → B) → F A → F B to a coercion A → B ≤ F A → F B. We incorporate it into a monomorphic system of coercions for base types, arrow types, and functor types. We prove that the resulting system of coercions is coherent, meaning that all possible choices of coercions from A to B end up equivalent. The proof of the theorem is based on coherence by evaluation, an approach to coherence proofs based on the well-known technique of normalization by evaluation. All definitions and theorems in the paper are checked in Agda, which played a valuable role in the design of the system.


title: Turning Parser Errors into Suggestions for REPL-Driven DSLs (Functional Pearl)

authors:
Matthías Páll Gissurarson
Elisabet Lobo Vesga
Alejandro Russo

abstract: Many of the domain-specific languages we use every day are not written to files but typed at an interactive prompt, e.g., database shells, cloud CLIs, and in-house analytics consoles. For these REPL-driven command languages, autocomplete is, we argue, not a polish feature but a core usability requirement --and yet they are precisely the languages whose authors often have the fewest resources to invest in tooling. Designing a new programming language tailored to specific domain challenges can be both powerful and rewarding. However, a major hurdle for adoption among users is, in our experience, the lack of tooling support, particularly features like autocomplete that enhance usability and reduce the learning curve. In this paper, we present a fresh perspective that turns parser errors -- traditionally seen as roadblocks -- into opportunities for generating valid, context-aware autocomplete suggestions. By leveraging the parser's built-in feedback mechanisms, our method offers a lightweight, adaptable, and simple solution, enabling domain-specific languages to provide basic development assistance with minimal overhead. The technique fits the REPL-driven DSL genre by design: inputs are modest-size single statements, the cursor sits at the end of the line, and parser-error recovery is unnecessary. We apply the technique to DPella DSL, a production REPL-driven DSL whose grammar comprises 43 top-level command constructors, 130 reserved keywords, and 22 labelled syntactic categories that drive identifier completion.


title: A Cost-Aware Probability Monad for Liquid Haskell

authors:
Matthias Hetzenberger
Georg Moser
Florian Zuleger

abstract: Probabilistic algorithms and data structures are widely used to obtain favourable expected performance guarantees. While their mathematical analysis is often well understood, mechanising expected-cost analyses remains challenging, requiring reasoning about probability distributions, expectations, and recursive stochastic behaviour. Existing formal approaches frequently require substantial manual proof effort, since expected costs are often encoded separately from probabilistic computations and must therefore be propagated explicitly throughout proofs.


title: Tikka: An Interpreter and Debugger for a Pedagogical Subset of Haskell

authors:
Alex Hobbs
Alex Dixon

abstract: Functional programming is a core part of many undergraduate-level courses in Computer Science. Pedagogical interest in Haskell continues to grow as functional idioms become commonplace in popular multi-paradigm languages. The Glasgow Haskell Compiler (GHC) is by far Haskell’s most used compiler, but can hinder students’ initial learning because of its detailed and verbose error messages which are designed to support experienced users and cover a broad language surface. In this paper we introduce Tikka, an interpreter for a carefully-selected subset of Haskell with concise, beginner-friendly error messages, evaluation tracing, and a bespoke IDE. This paper discusses the design of an interpreter targeted towards novice users, and presents an evaluation of its use in practice through user testing and a side-by-side comparison of GHC and Tikka.


title: Evaluating Shrinking (Experience Report)

authors:
Alperen Keles
George Miao
Leonidas Lampropoulos

abstract: Property-based testing frameworks rely on shrinking to turn noisy random failures into counterexamples that developers can debug. Although bug-finding performance is routinely measured, shrinking itself is rarely evaluated quantitatively. We present an experience report on evaluating shrinking across three Haskell frameworks: QuickCheck, Hedgehog, and Falsify. The comparison spans four ETNA workloads and several generator families, including type-based, API-based, and correct-by-construction generators. We measure both effectiveness, using tree edit distance to a ground-truth minimum found by exhaustive search, and cost, using shrink time and time per unit of shrinking progress. Across these workloads, QuickCheck's structural shrinking is usually faster and remains competitive on final counterexample quality; integrated shrinking does not by itself guarantee a performance or effectiveness advantage. We discuss what these results imply for future evaluations and designs of shrinking algorithms.


title: CloudMicroHaskell: Direct-Style Distributed Haskell via Runtime Graph Serialisation

authors:
Robert Krook
Lennart Augustsson

abstract: Cloud Haskell brings Erlang-style distributed programming to Haskell, but its treatment of mobile code exposes a difficult boundary in the source-level API. Remote processes must be expressed as static closures, messages must satisfy serialisation constraints, and participating nodes are assumed to share the relevant code.


title: What Have We Learned about Dependently Typed Programming from Haskell? (Keynote)

abstract: Dependent type theory is having a moment as the foundation for interactive provers, such as Lean, Rocq, and Agda. But what does dependent type theory offer to programmers, who just want to get work done? While Haskell is not a full spectrum dependently-typed language, its type system draws inspiration from its features, and provides a playground for experimentation. In this talk, I will use the "rebound" library to demonstrate and reflect on the current capabilities of dependently-typed programming in Haskell. This library supports working with well-scoped de Bruijn indices in abstract syntax trees. Because ASTs statically track their scope depths, type checking program transformations ensures that scopes are properly maintained, a source of subtle bugs in language implementation.


venue: hopl

title: Transcript of question and answer session

abstract: No abstract available.


title: Full text of all questions submitted

abstract: No abstract available.


title: Biography of Douglas T. Ross

abstract: No abstract available.


abstract: chapter Free Access Share on Transcript of question and answer session Author: John Goodenough View Profile Authors Info & Claims History of programming languagesJune 1978 Pages 397–399https://doi.org/10.1145/800025.1198382Published:01 June 1978Publication History 0citation184DownloadsMetricsTotal Citations0Total Downloads184Last 12 Months19Last 6 weeks7 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Biography of Jules I. Schwartz

abstract: No abstract available.


title: Transcript of discussant's remarks

abstract: chapter Free Access Share on Transcript of discussant's remarks Author: Paul Abrahams View Profile Authors Info & Claims History of programming languagesJune 1978 Pages 191–194https://doi.org/10.1145/800025.1198362Published:01 June 1978Publication History 0citation234DownloadsMetricsTotal Citations0Total Downloads234Last 12 Months15Last 6 weeks4 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: The history of Fortran I, II, and III

abstract: chapter Free Access Share on The history of Fortran I, II, and III Author: John Backus IBM Corporation, Research Division IBM Corporation, Research DivisionView Profile Authors Info & Claims History of programming languagesJune 1978 Pages 25–74https://doi.org/10.1145/800025.1198345Published:01 June 1978Publication History 14citation1,518DownloadsMetricsTotal Citations14Total Downloads1,518Last 12 Months222Last 6 weeks29 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Transcript of presentation

abstract: chapter Free Access Share on Transcript of presentation Author: John Backus IBM Corporation IBM CorporationView Profile Authors Info & Claims History of programming languagesJune 1978 Pages 45–66https://doi.org/10.1145/800025.1198346Published:01 June 1978Publication History 0citation418DownloadsMetricsTotal Citations0Total Downloads418Last 12 Months72Last 6 weeks6 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: JOSS: JOHNNIAC open-shop system

abstract: chapter Free Access Share on JOSS: JOHNNIAC open-shop system Author: Charles L. Baker Ocean Data Systems, Inc. Ocean Data Systems, Inc.View Profile Authors Info & Claims History of programming languagesJune 1978 Pages 495–508https://doi.org/10.1145/800025.1198400Published:01 June 1978Publication History 1citation313DownloadsMetricsTotal Citations1Total Downloads313Last 12 Months48Last 6 weeks8 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Transcript of discussant's remarks

abstract: chapter Free Access Share on Transcript of discussant's remarks Author: Frederick Brooks View Profile Authors Info & Claims History of programming languagesJune 1978 Pages 683–685https://doi.org/10.1145/800025.1198425Published:01 June 1978Publication History 0citation188DownloadsMetricsTotal Citations0Total Downloads188Last 12 Months12Last 6 weeks4 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


abstract: chapter Free Access Share on Transcript of question and answer session Author: Thomas Cheatham View Profile Authors Info & Claims History of programming languagesJune 1978 Pages 161–167https://doi.org/10.1145/800025.1198355Published:01 June 1978Publication History 0citation239DownloadsMetricsTotal Citations0Total Downloads239Last 12 Months18Last 6 weeks3 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Full text of all questions submitted

abstract: chapter Free Access Share on Full text of all questions submitted Author: Thomas Cheatham View Profile Authors Info & Claims History of programming languagesJune 1978 Pages 167–170https://doi.org/10.1145/800025.1198356Published:01 June 1978Publication History 0citation203DownloadsMetricsTotal Citations0Total Downloads203Last 12 Months17Last 6 weeks4 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Biography of Alan J. Perlis

abstract: No abstract available.


title: Biography of Peter Naur

abstract: No abstract available.


title: Full text of all questions submitted

abstract: chapter Free Access Share on Full text of all questions submitted Author: Thomas Cheatham View Profile Authors Info & Claims History of programming languagesJune 1978 Pages 508–511https://doi.org/10.1145/800025.1198401Published:01 June 1978Publication History 0citation153DownloadsMetricsTotal Citations0Total Downloads153Last 12 Months13Last 6 weeks4 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Biography of Charles L. Baker

abstract: No abstract available.


abstract: chapter Free Access Share on Transcript of question and answer session Author: Thomas Cheatham View Profile Authors Info & Claims History of programming languagesJune 1978 Pages 546–548https://doi.org/10.1145/800025.1198406Published:01 June 1978Publication History 0citation198DownloadsMetricsTotal Citations0Total Downloads198Last 12 Months21Last 6 weeks3 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Biography of Thomas E. Kurtz

abstract: No abstract available.


title: Transcript of discussant's remarks

abstract: chapter Free Access Share on Transcript of discussant's remarks Author: Ole-Johan Dahl View Profile Authors Info & Claims History of programming languagesJune 1978 Pages 488–490https://doi.org/10.1145/800025.1198394Published:01 June 1978Publication History 0citation211DownloadsMetricsTotal Citations0Total Downloads211Last 12 Months16Last 6 weeks4 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: The evolution of APL

authors:
Adin D. Falkoff
Kenneth E. Iverson

abstract: chapter Free Access Share on The evolution of APL Authors: Adin D. Falkoff IBM Corporation, Research Division IBM Corporation, Research DivisionView Profile , Kenneth E. Iverson IBM Corporation, Research Division IBM Corporation, Research DivisionView Profile Authors Info & Claims History of programming languagesJune 1978 Pages 661–674https://doi.org/10.1145/800025.1198423Published:01 June 1978Publication History 3citation447DownloadsMetricsTotal Citations3Total Downloads447Last 12 Months53Last 6 weeks6 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


abstract: chapter Free Access Share on The development of the General Purpose Simulation System (GPSS) Author: Geoffrey Gordon IBM Corporation, Data Processing Division IBM Corporation, Data Processing DivisionView Profile Authors Info & Claims History of programming languagesJune 1978 Pages 403–426https://doi.org/10.1145/800025.1198386Published:01 June 1978Publication History 12citation807DownloadsMetricsTotal Citations12Total Downloads807Last 12 Months169Last 6 weeks59 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Transcript of presentation

abstract: chapter Free Access Share on Transcript of presentation Author: Geoffrey Gordon View Profile Authors Info & Claims History of programming languagesJune 1978 Pages 426–434https://doi.org/10.1145/800025.1198387Published:01 June 1978Publication History 2citation186DownloadsMetricsTotal Citations2Total Downloads186Last 12 Months17Last 6 weeks4 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


abstract: chapter Free Access Share on A history of the SNOBOL programming languages Author: Ralph E. Griswold The University of Arizona The University of ArizonaView Profile Authors Info & Claims History of programming languagesJune 1978 Pages 601–645https://doi.org/10.1145/800025.1198417Published:01 June 1978Publication History 2citation1,273DownloadsMetricsTotal Citations2Total Downloads1,273Last 12 Months360Last 6 weeks70 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Transcript of presentation

abstract: chapter Free Access Share on Transcript of presentation Author: Ralph E. Griswold View Profile Authors Info & Claims History of programming languagesJune 1978 Pages 645–657https://doi.org/10.1145/800025.1198418Published:01 June 1978Publication History 0citation197DownloadsMetricsTotal Citations0Total Downloads197Last 12 Months19Last 6 weeks4 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Transcript of discussant's remarks

abstract: chapter Free Access Share on Transcript of discussant's remarks Author: Betty Holberton View Profile Authors Info & Claims History of programming languagesJune 1978 Pages 260–263https://doi.org/10.1145/800025.1198369Published:01 June 1978Publication History 0citation264DownloadsMetricsTotal Citations0Total Downloads264Last 12 Months67Last 6 weeks37 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF