title: Implicit phasing for R6RS libraries

authors:
Abdulaziz Ghuloum
R. Kent Dybvig

abstract: The forthcoming Revised6 Report on Scheme differs from previous reports in that the language it describes is structured as a set of libraries. It also provides a syntax for defining new portable libraries. The same library may export both procedure and hygienic macro definitions, which allows procedures and syntax to be freely intermixed, hidden, and exported.


venue: icfp

title: A generic usage analysis with subeffect qualifiers

authors:
Jurriaan Hage
Stefan Holdermans
Arie Middelkoop

abstract: Sharing analysis and uniqueness typing are static analyses that aim at determining which of a program's objects are to be used at most once. There are many commonalities between these two forms of usage analysis. We make their connection precise by developing an expressive generic analysis that can be instantiated to both sharing analysis and uniqueness typing. The resulting system, which combines parametric polymorphism with effect subsumption, is specified within the general framework of qualified types, so that readily available tools and techniques can be used for the development of implementations and metatheory.


title: Feedback directed implicit parallelism

authors:
Tim Harris
Satnam Singh

abstract: In this paper we present an automated way of using spare CPU resources within a shared memory multi-processor or multi-core machine. Our approach is (i) to profile the execution of a program, (ii) from this to identify pieces of work which are promising sources of parallelism, (iii) recompile the program with this work being performed speculatively via a work-stealing system and then (iv) to detect at run-time any attempt to perform operations that would reveal the presence of speculation.


title: Functional pearl: the great escape or, how to jump the border without getting caught

abstract: Filinski showed that callcc and a single mutable reference cell are sufficient to express the delimited control operators shift and reset. However, this implementation interacts poorly with dynamic bindings like exception handlers. We present a variation on Filinski's encoding of delimited continuations that behaves appropriately in the presence of exceptions and give an implementation in Standard ML of New Jersey. We prove the encoding correct with respect to the semantics of delimited dynamic binding.


title: Relating complexity and precision in control flow analysis

authors:
David Van Horn
Harry G. Mairson

abstract: We analyze the computational complexity of kCFA, a hierarchy of control flow analyses that determine which functions may be applied at a given call-site. This hierarchy specifies related decision problems, quite apart from any algorithms that may implement their solutions. We identify a simple decision problem answered by this analysis and prove that in the 0CFA case, the problem is complete for polynomial time. The proof is based on a nonstandard, symmetric implementation of Boolean logic within multiplicative linear logic (MLL). We also identify a simpler version of 0CFA related to η-expansion, and prove that it is complete for logarithmic space, using arguments based on computing paths and permutations.


title: Call-pattern specialisation for haskell programs

abstract: User-defined data types, pattern-matching, and recursion are ubiquitous features of Haskell programs. Sometimes a function is called with arguments that are statically known to be in constructor form, so that the work of pattern-matching is wasted. Even worse, the argument is sometimes freshly-allocated, only to be immediately decomposed by the function.


title: Compiling with continuations, continued

abstract: We present a series of CPS-based intermediate languages suitable for functional language compilation, arguing that they have practical benefits over direct-style languages based on A-normal form (ANF) or monads. Inlining of functions demonstrates the benefits most clearly: in ANF-based languages, inlining involves a re-normalization step that rearranges let expressions and possibly introduces a new 'join point' function, and in monadic languages, commuting conversions must be applied; in contrast, inlining in our CPS language is a simple substitution of variables for variables.


title: A type directed translation of MLF to system F

abstract: The MLF type system by Le Botlan and Rémy is a natural extension of Hindley-Milner type inference that supports full first-class polymorphism, where types can be of higher-rank and impredicatively instantiated. Even though MLF is theoretically very attractive, it has not seen widespread adoption. We believe that this partly because it is unclear how the rich language of MLF types relate to standard System F types. In this article we give the first type directed translation of MLF terms to System F terms. Based on insight gained from this translation, we also define "Rigid MLF" (MLF=), a restriction of MLF where all bound values have a System F type. The expressiveness of MLF= is the same as that of boxy types, but MLF= needs fewer annotations and we give a detailed comparison between them.


title: Declarative programming for artificial intelligence applications

abstract: In this talk, I will consider some possible extensions to existing functional programming languages that would make them more suitable for the important and growing class of artificial intelligence applications. First, I will motivate the need for these language extensions. Then I will give some technical detail about these extensions that provide the logic programming idioms, probabilistic computation, and modal computation. Some examples will be given to illustrate these ideas which have been implemented in the Bach programming language that is an extension of Haskell.


title: Faster laziness using dynamic pointer tagging

authors:
Simon Marlow
Alexey Rodriguez Yakushev
Simon L. Peyton Jones

abstract: In the light of evidence that Haskell programs compiled by GHC exhibit large numbers of mispredicted branches on modern processors, we re-examine the "tagless" aspect of the STG-machine that GHC uses as its evaluation model.


title: Bidirectionalization transformation based on automatic derivation of view complement functions

authors:
Kazutaka Matsuda
Zhenjiang Hu
Keisuke Nakano
Makoto Hamana
Masato Takeichi

abstract: Bidirectional transformation is a pair of transformations: a view function and a backward transformation. A view function maps one data structure called source onto another called view. The corresponding backward transformation reflects changes in the view to the source. Its practically useful applications include replicated data synchronization, presentation-oriented editor development, tracing software development, and view updating in the database community. However, developing a bidirectional transformation is hard, because one has to give two mappings that satisfy the bidirectional properties for system consistency.


title: Evaluating high-level distributed language constructs

authors:
Jan Henry Nyström
Philip W. Trinder
David J. King

abstract: The paper investigates the impact of high level distributed programming language constructs on the engineering of realistic software components. Based on reengineering two non-trivial telecoms components, we compare two high-level distributed functional languages, Erlang and GdH, with conventional distributed technologies C++/CORBA and C++/UDP.


title: Type-safe higher-order channels in ML-like languages

abstract: As a means of transmitting not only data but also code encapsulated within functions, higher-order channels provide an advanced form of task parallelism in parallel computations. In the presence of mutable references, however, they pose a safety problem because references may be transmitted to remote threads where they are no longer valid.


title: Subtyping and intersection types revisited

abstract: Church's system of simple types has proven to be remarkably robust: call-by-name, call-by-need, and call-by-value languages, with or without effects, and even logical frameworks can be based on the same typing rules. When type systems become more expressive, this unity fractures. An early example is the value restriction for parametric polymorphism which is necessary for ML but not Haskell; a later manifestation is the lack of distributivity of function types over intersections in call-by-value languages with effects.


title: iTasks: executable specifications of interactive work flow systems for the web

authors:
Rinus Plasmeijer
Peter Achten
Pieter W. M. Koopman

abstract: In this paper we introduce the iTask system: a set of combinators to specify work flows in a pure functional language at a very high level of abstraction. Work flow systems are automated systems in which tasks are coordinated that have to be executed by humans and computers. The combinators that we propose support work flow patterns commonly found in commercial work flow systems. Compared with most of these commercial systems, the iTask system offers several advantages: tasks are statically typed, tasks can be higher order, the combinators are fully compositional, dynamic and recursive work flows can be specified, and last but not least, the specification is used to generate an executable web-based multi-user work flow application. With the iTask system, useful work flows can be defined which cannot be expressed in other systems: work can be interrupted and subsequently directed to other workers for further processing.The implementation is special as well. It is based on the Clean iData toolkit which makes it possible to create fully dynamic, interactive, thin client web applications. Thanks to the generic programming techniques used in the iData toolkit, the programming effort is reduced significantly: state handling, form rendering, user interaction, and storage management is handled automatically. The iTask system allows a task to be regarded as a special kind of persistent redex being reduced by the application user via task completion. The combinators control the order in which these redexes are made available to the application user. The system rewrites the persistent task redexes in a similar way as functions are rewritten in lazy functional languages.


title: Termination analysis and call graph construction for higher-order functional programs

abstract: The analysis and verification of higher-order programs raises the issue of control-flow analysis for higher-order languages. The problem of constructing an accurate call graph for a higher-order program has been the topic of extensive research, and numerous methods for flow analysis, varying in complexity and precision, have been suggested.


title: Ott: effective tool support for the working semanticist

authors:
Peter Sewell
Francesco Zappa Nardelli
Scott Owens
Gilles Peskine
Tom Ridge
Susmit Sarkar
Rok Strnisa

abstract: It is rare to give a semantic definition of a full-scale programming language, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics - usually either LaTEX for informal mathematics, or the formal mathematics of a proof assistant - make it much harder than necessary to work with large definitions.We present a metalanguage specifically designed for this problem, and a tool, ott, that sanity-checks such definitions and compiles them into proof assistant code for Coq, HOL, Isabelle, and (in progress) Twelf, together with LaTEX code for production-quality typesetting, and OCaml boilerplate. The main innovations are:(1) metalanguage design to make definitions concise, and easy to read and edit;(2) an expressive but intuitive metalanguage for specifying binding structures; and (3) compilation to proof assistant code.This has been tested in substantial case studies, including modular specifications of calculi from the TAPL text, a Lightweight Java with Java JSR 277/294 module system proposals, and a large fragment of OCaml (around 306 rules), with machine proofs of various soundness results. Our aim with this work is to enable a phase change: making it feasible to work routinely, without heroic effort, with rigorous semantic definitions of realistic languages.

awards: Most Influential ICFP Paper (awarded 2017)


title: Experience report: the reactis validation tool

authors:
Steve Sims
Daniel C. DuVarney

abstract: Reactis is a commercially successful testing and validation tool which is implemented almost entirely in Standard ML. Our experience using a functional language to develop a commercial product has led us to the conclusion that while functional languages have some disadvantages, in the case of Reactis the benefits of a functional language substantially outweigh the drawbacks.


title: Program-ing finger trees in Coq

abstract: International audience


title: Extensible pattern matching via a lightweight language extension

authors:
Don Syme
Gregory Neverov
James Margetson

abstract: Pattern matching of algebraic data types (ADTs) is a standard feature in typed functional programming languages, but it is well known that it interacts poorly with abstraction. While several partial solutions to this problem have been proposed, few have been implemented or used. This paper describes an extension to the .NET language F# called active patterns, which supports pattern matching over abstract representations of generic heterogeneous data such as XML and term structures, including where these are represented via object models in other .NET languages. Our design is the first to incorporate both ad hoc pattern matching functions for partial decompositions and "views" for total decompositions, and yet remains a simple and lightweight extension. We give a description of the language extension along with numerous motivating examples. Finally we describe how this feature would interact with other reasonable and related language extensions: existential types quantified at data discrimination tags, GADTs, and monadic generalizations of pattern matching.


title: Experience report: functional programming in c-rules

abstract: C-Rules is a business rules management system developed by Constraint Technologies International1 (CTI), designed for use in transportation problems. Users define rules describing various aspects of a problem, such as solution costs and legality, which are then queried from a host application, typically an optimising solver. At its core, C-Rules provides a functional expression language which affords users both power and flexibility when formulating rules. In this paper we will describe our experiences of using functional programming both at the end-user level, as well as at the implementation level. We highlight some of the benefits we, and the product's users, have enjoyed from the decision to base our rule system on features such as: higher-order functions, referential transparency, and static, polymorphic typing. We also outline some of our experiences in using Haskell to build an efficient compiler for the core language.


title: Experience report: scheme in commercial web application development

authors:
Noel Welsh
David Gurnell

abstract: Over the past year Untyped has developed some 40'000 lines of Scheme code for a variety of web-based applications, which receive over 10'000 hits a day. This is, to our knowledge, the largest web-based application deployment of PLT Scheme. Our experiences developing with PLT Scheme show that deficiencies in the existing infrastructure can be easily overcome, and we can exploit advanced language features to improve productivity. We conclude that PLT Scheme makes an excellent platform for developing web-based applications, and is competitive with more mainstream choices.


title: Efficient nondestructive equality checking for trees and graphs

authors:
Michael D. Adams
R. Kent Dybvig

abstract: The Revised6 Report on Scheme requires its generic equivalence predicate, equal?, to terminate even on cyclic inputs. While the terminating equal? can be implemented via a DFA-equivalence or union-find algorithm, these algorithms usually require an additional pointer to be stored in each object, are not suitable for multithreaded code due to their destructive nature, and may be unacceptably slow for the small acyclic values that are the most likely inputs to the predicate.


title: Typed closure conversion preserves observational equivalence

authors:
Amal Ahmed
Matthias Blume

abstract: Language-based security relies on the assumption that all potential attacks are bound by the rules of the language in question. When programs are compiled into a different language, this is true only if the translation process preserves observational equivalence.


title: Paradise: a two-stage DSL embedded in Haskell

authors:
Lennart Augustsson
Howard Mansell
Ganesh Sittampalam

abstract: We have implemented a two-stage language, Paradise, for building reusable components which are used to price financial products. Paradise is embedded in Haskell and makes heavy use of type-class based overloading, allowing the second stage to be compiled into a variety of backend platforms.


title: Typed iterators for XML

authors:
Giuseppe Castagna
Kim Nguyen

abstract: International audience


title: Functional translation of a calculus of capabilities

authors:
Arthur Charguéraud
François Pottier

abstract: Reasoning about imperative programs requires the ability to track aliasing and ownership properties. We present a type system that provides this ability, by using regions, capabilities, and singleton types. It is designed for a high-level calculus with higher-order functions, algebraic data structures, and references (mutable memory cells). The type system has polymorphism, yet does not require a value restriction, because capabilities act as explicit store typings.


title: FLUX: functional updates for XML

abstract: XML database query languages have been studied extensively, but XML database updates have received relatively little attention, and pose many challenges to language design. We are developing an XML update language called FLUX, which stands for FunctionaL Updates for XML, drawing upon ideas from functional programming languages. In prior work, we have introduced a core language for FLUX with a clear operational semantics and a sound, decidable static type system based on regular expression types.


title: Parametric higher-order abstract syntax for mechanized semantics

awards: Most Influential ICFP Paper (awarded 2018)


title: Experience report: erlang in acoustic ray tracing

authors:
Christian Convey
Andrew Fredricks
Christopher Gagner
Douglas Maxwell
Lutz Hamel

abstract: We investigated the relative merits of C++ and Erlang in the implementation of a parallel acoustic ray tracing algorithm for the U.S. Navy. We found a much smaller learning curve and better debugging environment for parallel Erlang than for pthreads-based C++ programming. Our C++ implementation outperformed the Erlang program by at least 12x. Attempts to use Erlang on the IBM Cell BE microprocessor were frustrated by Erlang's memory footprint.


title: Defunctionalized interpreters for programming languages

abstract: This document illustrates how functional implementations of formal semantics (structural operational semantics, reduction semantics, small-step and big-step abstract machines, natural semantics, and denotational semantics) can be transformed into each other. These transformations were foreshadowed by Reynolds in "Definitional Interpreters for Higher-Order Programming Languages" for functional implementations of denotational semantics, natural semantics, and big-step abstract machines using closure conversion, CPS transformation, and defunctionalization. Over the last few years, the author and his students have further observed that functional implementations of small-step and of big-step abstract machines are related using fusion by fixed-point promotion and that functional implementations of reduction semantics and of small-step abstract machines are related using refocusing and transition compression. It furthermore appears that functional implementations of structural operational semantics and of reduction semantics are related as well, also using CPS transformation and defunctionalization. This further relation provides an element of answer to Felleisen's conjecture that any structural operational semantics can be expressed as a reduction semantics: for deterministic languages, a reduction semantics is a structural operational semantics in continuation style, where the reduction context is a defunctionalized continuation. As the defunctionalized counterpart of the continuation of a one-step reduction function, a reduction context represents the rest of the reduction, just as an evaluation context represents the rest of the evaluation since it is the defunctionalized counterpart of the continuation of an evaluation function.


title: Report on the tenth ICFP programming contest

authors:
Eelco Dolstra
Jurriaan Hage
Bastiaan Heeren
Stefan Holdermans
Johan Jeuring
Andres Löh
Clara Löh
Arie Middelkoop
Alexey Rodriguez
John van Schie

abstract: The ICFP programming contest is a 72-hour contest, which attracts thousands of contestants from all over the world. In this report we describe what it takes to organise this contest, the main ideas behind the contest we organised, the task, how to solve it, how we created it, and how well the contestants did.


title: NixOS: a purely functional Linux distribution

authors:
Eelco Dolstra
Andres Löh

abstract: Existing package and system configuration management tools suffer from an imperative model, where system administration actions such as upgrading packages or changes to system configuration files are stateful: they destructively update the state of the system. This leads to many problems, such as the inability to roll back changes easily, to run multiple versions of a package side-by-side, to reproduce a configuration deterministically on another machine, or to reliably upgrade a system. In this paper we show that we can overcome these problems by moving to a purely functional system configuration model. This means that all static parts of a system (such as software packages, configuration files and system startup scripts) are built by pure functions and are immutable, stored in a way analogously to a heap in a purely function language. We have implemented this model in NixOS, a non-trivial Linux distribution that uses the Nix package manager to build the entire system configuration from a purely functional specification.


title: Mixin' up the ML module system

authors:
Derek Dreyer
Andreas Rossberg

abstract: ML modules provide hierarchical namespace management, as well as fine-grained control over the propagation of type information, but they do not allow modules to be broken up into mutually recursive, separately compilable components. Mixin modules facilitate recursive linking of separately compiled components, but they are not hierarchically composable and typically do not support type abstraction. We synthesize the complementary advantages of these two mechanisms in a novel module system design we call MixML.


title: Experience report: visualizing data through functional pipelines

authors:
David J. Duke
Rita Borgo
Colin Runciman
Malcolm Wallace


title: Transactional events for ML

authors:
Laura Effinger-Dean
Matthew Kehrt
Dan Grossman

abstract: Transactional events (TE) are an approach to concurrent programming that enriches the first-class synchronous message-passing of Concurrent ML (CML) with a combinator that allows multiple messages to be passed as part of one all-or-nothing synchronization. Donnelly and Fluet (2006) designed and implemented TE as a Haskell library and demonstrated that it enables elegant solutions to programming patterns that are awkward or impossible in CML. However, both the definition and the implementation of TE relied fundamentally on the code in a synchronization not using mutable memory, an unreasonable assumption for mostly functional languages like ML where functional interfaces may have impure implementations.


title: Data-flow testing of declarative programs

authors:
Sebastian Fischer
Herbert Kuchen


title: A scheduling framework for general-purpose parallel languages

authors:
Matthew Fluet
Mike Rainey
John H. Reppy

abstract: The trend in microprocessor design toward multicore and manycore processors means that future performance gains in software will largely come from harnessing parallelism. To realize such gains, we need languages and implementations that can enable parallelism at many different levels. For example, an application might use both explicit threads to implement course-grain parallelism for independent tasks and implicit threads for fine-grain data-parallel computation over a large array. An important aspect of this requirement is supporting a wide range of different scheduling mechanisms for parallel computation.


title: Implicitly-threaded parallelism in Manticore

authors:
Matthew Fluet
Mike Rainey
John H. Reppy
Adam Shaw


title: Quotient lenses

authors:
J. Nathan Foster
Alexandre Pilkiewicz
Benjamin C. Pierce

abstract: There are now a number of BIDIRECTIONAL PROGRAMMING LANGUAGES, where every program can be read both as a forward transformation mapping one data structure to another and as a reverse transformation mapping an edited output back to a correspondingly edited input. Besides parsimony - the two related transformations are described by just one expression - such languages are attractive because they promise strong behavioral laws about how the two transformations fit together - e.g., their composition is the identity function. It has repeatedly been observed, however, that such laws are actually a bit too strong: in practice, we do not want them "on the nose," but only up to some equivalence, allowing inessential details, such as whitespace, to be modified after a round trip. Some bidirectional languages loosen their laws in this way, but only for specific, baked-in equivalences.


title: A type-preserving compiler in Haskell

authors:
Louis-Julien Guillemette
Stefan Monnier

abstract: There has been a lot of interest of late for programming languages that incorporate features from dependent type systems and proof assistants, in order to capture important invariants of the program in the types. This allows type-based program verification and is a promising compromise between plain old types and full blown Hoare logic proofs. The introduction of GADTs in GHC (and more recently type families) made such dependent typing available in an industry-quality implementation, making it possible to consider its use in large scale programs.


title: Generic discrimination: sorting and paritioning unshared data in linear time

abstract: We introduce the notion of discrimination as a generalization of both sorting and partitioning and show that worst-case linear-time discrimination functions (discriminators) can be defined generically, by (co-)induction on an expressive language of order denotations. The generic definition yields discriminators that generalize both distributive sorting and multiset discrimination. The generic discriminator can be coded compactly using list comprehensions, with order denotations specified using Generalized Algebraic Data Types (GADTs). A GADT-free combinator formulation of discriminators is also given.


title: Functional pearl: streams and unique fixed points

abstract: Streams, infinite sequences of elements, live in a coworld: they are given by a coinductive data type, operations on streams are implemented by corecursive programs, and proofs are conducted using coinduction. But there is more to it: suitably restricted, stream equations possess unique solutions, a fact that is not very widely appreciated. We show that this property gives rise to a simple and attractive proof technique essentially bringing equational reasoning to the coworld. In fact, we redevelop the theory of recurrences, finite calculus and generating functions using streams and stream operators building on the cornerstone of unique solutions. The development is constructive: streams and stream operators are implemented in Haskell, usually by one-liners. The resulting calculus or library, if you wish, is elegant and fun to use. Finally, we rephrase the proof of uniqueness using generalised algebraic data types.


title: Deciding kCFA is complete for EXPTIME

authors:
David Van Horn
Harry G. Mairson

abstract: We give an exact characterization of the computational complexity of the kCFA hierarchy. For any k> 0, we prove that the con-trol flow decision problem is complete for deterministic exponen-tial time. This theorem validates empirical observations that such control flow analysis is intractable. It also provides more general insight into the complexity of abstract interpretation.


title: AURA: a programming language for authorization and audit

authors:
Limin Jia
Jeffrey A. Vaughan
Karl Mazurak
Jianzhou Zhao
Luke Zarko
Joseph Schorr
Steve Zdancewic

abstract: This paper presents AURA, a programming language for access control that treats ordinary programming constructs (e.g., integers and recursive functions) and authorization logic constructs (e.g., principals and access control policies) in a uniform way. AURA is based on polymorphic DCC and uses dependent types to permit assertions that refer directly to AURA values while keeping computation out of the assertion level to ensure tractability. The main technical results of this paper include fully mechanically verified proofs of the decidability and soundness for AURA's type system, and a prototype typechecker and interpreter.


title: Experience report: playing the DSL card

abstract: This paper describes our experience using a functional language, Haskell, to build an embedded, domain-specific language (DSL) for component configuration in large-scale, real-time, embedded systems. Prior to the introduction of the DSL, engineers would describe the steps needed to configure a particular system in a handwritten XML document. In this paper, we outline the application domain, give a brief overview of the DSL that we developed, and provide concrete data to demonstrate its effectiveness. In particular, we show that the DSL has several significant benefits over the original, XML-based approach including reduced code size, increased modularity and scalability, and detection and prevention of common defects. For example, using the DSL, we were able to produce clear and intuitive descriptions of component configurations that were sometimes less than 1/30 of the size of the original XML.


title: Polymorphism and page tables: systems programming from a functional programmer's perspective

abstract: With features that include lightweight syntax, expressive type systems, and deep semantic foundations, functional languages are now being used to develop an increasingly broad range of complex, real-world applications. In the area of systems software, however, where performance and interaction with low-level aspects of hardware are central concerns, many practitioners still eschew the advantages of higher-level languages for the potentially unsafe but predictable behavior of traditional imperative languages like C. It is ironic that critical applications such as operating systems kernels, device drivers, and VMMs - where a single bug could compromise the reliability or security of a whole system - are among the least likely to benefit from the abstractions and safety guarantees of modern language designs.


title: Pattern minimization problems over recursive data types

abstract: In the context of program verification in an interactive theorem prover, we study the problem of transforming function definitions with ML-style (possibly overlapping) pattern matching into minimal sets of independent equations. Since independent equations are valid unconditionally, they are better suited for the equational proof style using induction and rewriting, which is often found in proofs in theorem provers or on paper.


title: Lazy and speculative execution in computer systems


title: HMF: simple type inference for first-class polymorphism

abstract: HMF is a conservative extension of Hindley-Milner type inference with first-class polymorphism. In contrast to other proposals, HML uses regular System F types and has a simple type inference algorithm that is just a small extension of the usual Damas-Milner algorithm W. Given the relative simplicity and expressive power, we feel that HMF can be an attractive type system in practice. There is a reference implementation of the type system available online together with a technical report containing proofs (Leijen 2007a,b).


title: Compiling self-adjusting programs with continuations

authors:
Ruy Ley-Wild
Matthew Fluet
Umut A. Acar

abstract: Self-adjusting programs respond automatically and efficiently to input changes by tracking the dynamic data dependences of the computation and incrementally updating the output as needed. In order to identify data dependences, previously proposed approaches require the user to make use of a set of monadic primitives. Rewriting an ordinary program into a self-adjusting program with these primitives, however, can be difficult and error-prone due to various monadic and proper-usage restrictions, some of which cannot be enforced statically. Previous work therefore suggests that self-adjusting computation would benefit from direct language and compiler support.


title: Flask: staged functional programming for sensor networks

authors:
Geoffrey Mainland
Greg Morrisett
Matt Welsh


title: Write it recursively: a generic framework for optimal path queries

authors:
Akimasa Morihata
Kiminori Matsuzaki
Masato Takeichi


title: Experience report: a pure shirt fits

abstract: Bluespec is a hardware-design tools startup whose core technology is developed using Haskell. Haskell is an unusual choice for a startup because it adds technical risk to the inherent business risk. In the years since Bluespec's founding, we have discovered that Haskell's purity is an unexpected match for the development needs of a startup. Based on Bluespec's experience, we conclude that pure programming languages can be the source of a competitive advantage for startup software companies.


title: Ynot: dependent types for imperative programs

authors:
Aleksandar Nanevski
Greg Morrisett
Avraham Shinnar
Paul Govereau
Lars Birkedal

abstract: We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. Coq already includes a powerful functional language that supports dependent types, but that language is limited to pure, total functions. The key contribution of our extension, which we call Ynot, is the added support for computations that may have effects such as non-termination, accessing a mutable store, and throwing/catching exceptions.


title: The power of Pi

authors:
Nicolas Oury
Wouter Swierstra

abstract: This paper exhibits the power of programming with dependent types by dint of embedding three domain-specific languages: Cryptol, a language for cryptographic protocols; a small data description language; and relational algebra. Each example demonstrates particular design patterns inherent to dependently-typed programming. Documenting these techniques paves the way for further research in domain-specific embedded type systems.


title: Functional netlists

authors:
Sungwoo Park
Jinha Kim
Hyeonseung Im

abstract: In efforts to overcome the complexity of the syntax and the lack of formal semantics of conventional hardware description languages, a number of functional hardware description languages have been developed. Like conventional hardware description languages, however, functional hardware description languages eventually convert all source programs into netlists, which describe wire connections in hardware circuits at the lowest level and conceal all high-level descriptions written into source programs.


title: From ML to MLF: graphic type constraints with efficient type inference

authors:
Didier Rémy
Boris Yakobowski

abstract: MLF is a type system that seamlessly merges ML-style type inference with System-F polymorphism. We propose a system of graphic (type) constraints that can be used to perform type inference in both ML or MLF. We show that this constraint system is a small extension of the formalism of graphic types, originally introduced to represent MLF types. We give a few semantic preserving transformations on constraints and propose a strategy for applying them to solve constraints. We show that the resulting algorithm has optimal complexity for MLF type inference, and argue that, as for ML, this complexity is linear under reasonable assumptions.


title: Type checking with open type functions

authors:
Tom Schrijvers
Simon L. Peyton Jones
Manuel M. T. Chakravarty
Martin Sulzmann

abstract: We report on an extension of Haskell with open type-level functions and equality constraints that unifies earlier work on GADTs, functional dependencies, and associated types. The contribution of the paper is that we identify and characterise the key technical challenge of entailment checking; and we give a novel, decidable, sound, and complete algorithm to solve it, together with some practically-important variants. Our system is implemented in GHC, and is already in active use.


title: Space profiling for parallel functional programs

authors:
Daniel Spoonhower
Guy E. Blelloch
Robert Harper
Phillip B. Gibbons

abstract: This paper presents a semantic space profiler for parallel functional programs. Building on previous work in sequential profiling, our tools help programmers to relate runtime resource use back to program source code. Unlike many profiling tools, our profiler is based on a cost semantics. This provides a means to reason about performance without requiring a detailed understanding of the compiler or runtime system. It also provides a specification for language implementers. This is critical in that it enables us to separate cleanly the performance of the application from that of the language implementation.


title: FPH: first-class polymorphism for Haskell

authors:
Dimitrios Vytiniotis
Stephanie Weirich
Simon L. Peyton Jones

abstract: Languages supporting polymorphism typically have ad-hoc restrictions on where polymorphic types may occur. Supporting "firstclass" polymorphism, by lifting those restrictions, is obviously desirable, but it is hard to achieve this without sacrificing type inference. We present a new type system for higher-rank and impredicative polymorphism that improves on earlier proposals: it is an extension of Damas-Milner; it relies only on System F types; it has a simple, declarative specification; it is robust to program transformations; and it enjoys a complete and decidable type inference algorithm.


title: Experience report: ocsigen, a web programming framework

authors:
Vincent Balat
Jérôme Vouillon
Boris Yakobowski

abstract: The evolution of Web sites towards very dynamic applications makes it necessary to reconsider current Web programming technologies. We believe that Web development would benefit greatly from more abstract paradigms and that a more semantical approach would result in huge gains in expressiveness. In particular, functional programming provides a really elegant solution to some important Web interaction problems, but few frameworks take advantage of it.


title: Biorthogonality, step-indexing and compiler correctness

authors:
Nick Benton
Chung-Kil Hur

abstract: We define logical relations between the denotational semantics of a simply typed functional language with recursion and the operational behaviour of low-level programs in a variant SECD machine. The relations, which are defined using biorthogonality and stepindexing, capture what it means for a piece of low-level code to implement a mathematical, domain-theoretic function and are used to prove correctness of a simple compiler. The results have been formalized in the Coq proof assistant.


title: A concurrent ML library in concurrent Haskell

abstract: In Concurrent ML, synchronization abstractions can be defined and passed as values, much like functions in ML. This mechanism admits a powerful, modular style of concurrent programming, called higher-order concurrent programming. Unfortunately, it is not clear whether this style of programming is possible in languages such as Concurrent Haskell, that support only first-order message passing. Indeed, the implementation of synchronization abstractions in Concurrent ML relies on fairly low-level, language-specific details. In this paper we show, constructively, that synchronization abstractions can be supported in a language that supports only first-order message passing. Specifically, we implement a library that makes Concurrent ML-style programming possible in Concurrent Haskell. We begin with a core, formal implementation of synchronization abstractions in the π-calculus. Then, we extend this implementation to encode all of Concurrent ML's concurrency primitives (and more!) in Concurrent Haskell. Our implementation is surprisingly efficient, even without possible optimizations. In several small, informal experiments, our library seems to outperform OCaml's standard library of Concurrent ML-style primitives. At the heart of our implementation is a new distributed synchronization protocol that we prove correct. Unlike several previous translations of synchronization abstractions in concurrent languages, we remain faithful to the standard semantics for Concurrent ML's concurrency primitives. For example, we retain the symmetry of choose, which can express selective communication. As a corollary, we establish that implementing selective communication on distributed machines is no harder than implementing first-order message passing on such machines.


title: Effective interactive proofs for higher-order imperative programs

authors:
Adam Chlipala
J. Gregory Malecha
Greg Morrisett
Avraham Shinnar
Ryan Wisnesky

abstract: We present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type Theory. That original system was a proof of concept, where every program verification was accomplished via laborious manual proofs, with much code devoted to uninteresting low-level details. In this paper, we present a re-implementation of Ynot which makes it possible to implement fully-verified, higher-order imperative programs with reasonable proof burden. At the same time, our new system is implemented entirely in Coq source files, showcasing the versatility of that proof assistant as a platform for research on language design and verification. Both versions of the system have been evaluated with case studies in the verification of imperative data structures, such as hash tables with higher-order iterators. The verification burden in our new system is reduced by at least an order of magnitude compared to the old system, by replacing manual proof with automation. The core of the automation is a simplification procedure for implications in higher-order separation logic, with hooks that allow programmers to add domain-specific simplification rules.


title: Finding race conditions in Erlang with QuickCheck and PULSE

authors:
Koen Claessen
Michal H. Palka
Nicholas Smallbone
John Hughes
Hans Svensson
Thomas Arts
Ulf T. Wiger

abstract: We address the problem of testing and debugging concurrent, distributed Erlang applications. In concurrent programs, race conditions are a common class of bugs and are very hard to find in practice. Traditional unit testing is normally unable to help finding all race conditions, because their occurrence depends so much on timing. Therefore, race conditions are often found during system testing, where due to the vast amount of code under test, it is often hard to diagnose the error resulting from race conditions. We present three tools (QuickCheck, PULSE, and a visualizer) that in combination can be used to test and debug concurrent programs in unit testing with a much better possibility of detecting race conditions. We evaluate our method on an industrial concurrent case study and illustrate how we find and analyze the race conditions.


title: Experience report: OCaml for an industrial-strength static analysis framework

authors:
Pascal Cuoq
Julien Signoles
Patrick Baudin
Richard Bonichon
Géraud Canet
Loïc Correnson
Benjamin Monate
Virgile Prevosto
Armand Puccetti

abstract: This experience report describes the choice of OCaml as the implementation language for Frama-C, a framework for the static analysis of C programs. OCaml became the implementation language for Frama-C because it is expressive. Most of the reasons listed in the remaining of this article are secondary reasons, features which are not specific to OCaml (modularity, availability of a C parser, control over the use of resources...) but could have prevented the use of OCaml for this project if they had been missing.


title: Beautiful differentiation

abstract: Automatic differentiation (AD) is a precise, efficient, and convenient method for computing derivatives of functions. Its forward-mode implementation can be quite simple even when extended to compute all of the higher-order derivatives as well. The higher-dimensional case has also been tackled, though with extra complexity. This paper develops an implementation of higher-dimensional, higher-order, forward-mode AD in the extremely general and elegant setting of calculus on manifolds and derives that implementation from a simple and precise specification. In order to motivate and discover the implementation, the paper poses the question "What does AD mean, independently of implementation?" An answer arises in the form of naturality of sampling a function and its derivative. Automatic differentiation flows out of this naturality condition, together with the chain rule. Graduating from first-order to higher-order AD corresponds to sampling all derivatives instead of just one. Next, the setting is expanded to arbitrary vector spaces, in which derivative values are linear maps. The specification of AD adapts to this elegant and very general setting, which even simplifies the development.


title: A functional I/O system or, fun for freshman kids

authors:
Matthias Felleisen
Robert Bruce Findler
Matthew Flatt
Shriram Krishnamurthi

abstract: Functional programming languages ought to play a central role in mathematics education for middle schools (age range: 10-14). After all, functional programming is a form of algebra and programming is a creative activity about problem solving. Introducing it into mathematics courses would make pre-algebra course come alive. If input and output were invisible, students could implement fun simulations, animations, and even interactive and distributed games all while using nothing more than plain mathematics. We have implemented this vision with a simple framework for purely functional I/O. Using this framework, students design, implement, and test plain mathematical functions over numbers, booleans, string, and images. Then the framework wires them up to devices and performs all the translation from external information to internal data (and vice versa)--just like every other operating system. Once middle school students are hooked on this form of programming, our curriculum provides a smooth path for them from pre-algebra to freshman courses in college on object-oriented design and theorem proving.


title: Purely functional lazy non-deterministic programming

authors:
Sebastian Fischer
Oleg Kiselyov
Chung-chieh Shan

abstract: Functional logic programming and probabilistic programming have demonstrated the broad benefits of combining laziness (non-strict evaluation with sharing of the results) with non-determinism. Yet these benefits are seldom enjoyed in functional programming, because the existing features for non-strictness, sharing, and non-determinism in functional languages are tricky to combine.


title: Scribble: closing the book on ad hoc documentation tools

authors:
Matthew Flatt
Eli Barzilay
Robert Bruce Findler

abstract: Scribble is a system for writing library documentation, user guides, and tutorials. It builds on PLT Scheme's technology for language extension, and at its heart is a new approach to connecting prose references with library bindings. Besides the base system, we have built Scribble libraries for JavaDoc-style API documentation, literate programming, and conference papers. We have used Scribble to produce thousands of pages of documentation for PLT Scheme; the new documentation is more complete, more accessible, and better organized, thanks in large part to Scribble's flexibility and the ease with which we cross-reference information across levels. This paper reports on the use of Scribble and on its design as both an extension and an extensible part of PLT Scheme.


title: OXenstored: an efficient hierarchical and transactional database using functional programming with reference cell comparisons

authors:
Thomas Gazagnaire
Vincent Hanquez

abstract: We describe in this paper our implementation of the Xenstored service which is part of the Xen architecture. Xenstored maintains a hierarchical and transactional database, used for storing and managing configuration values.


title: Identifying query incompatibilities with evolving XML schemas

authors:
Pierre Genevès
Nabil Layaïda
Vincent Quint

abstract: During the life cycle of an XML application, both schemas and queries may change from one version to another. Schema evolutions may affect query results and potentially the validity of produced data. Nowadays, a challenge is to assess and accommodate the impact of these changes in evolving XML applications. Such questions arise naturally in XML static analyzers. These analyzers often rely on decision procedures such as inclusion between XML schemas, query containment and satisfiability. However, existing decision procedures cannot be used directly in this context. The reason is that they are unable to distinguish information related to the evolution from information corresponding to bugs. This paper proposes a predicate language within a logical framework that can be used to make this distinction.


title: Functional pearl: la tour d'Hanoï

abstract: This pearl aims to demonstrate the ideas of wholemeal and projective programming using the Towers of Hanoi puzzle as a running example. The puzzle has its own beauty, which we hope to expose along the way.


title: Experience report: seL4: formally verifying a high-performance microkernel

authors:
Gerwin Klein
Philip Derrin
Kevin Elphinstone

abstract: We report on our experience using Haskell as an executable specification language in the formal verification of the seL4 microkernel. The verification connects an abstract operational specification in the theorem prover Isabelle/HOL to a C implementation of the microkernel. We describe how this project differs from other efforts, and examine the effect of using Haskell in a large-scale formal verification. The kernel comprises 8,700 lines of C code; the verification more than 150,000 lines of proof script.


title: A universe of binding and computation

authors:
Daniel R. Licata
Robert Harper

abstract: We construct a logical framework supporting datatypes that mix binding and computation, implemented as a universe in the dependently typed programming language Agda 2. We represent binding pronominally, using well-scoped de Bruijn indices, so that types can be used to reason about the scoping of variables. We equip our universe with datatype-generic implementations of weakening, substitution, exchange, contraction, and subordination-based strengthening, so that programmers need not reimplement these operations for each individual language they define. In our mixed, pronominal setting, weakening and substitution hold only under some conditions on types, but we show that these conditions can be discharged automatically in many cases. Finally, we program a variety of standard difficult test cases from the literature, such as normalization-by-evaluation for the untyped lambda-calculus, demonstrating that we can express detailed invariants about variable usage in a program's type while still writing clean and clear code.


title: Causal commutative arrows and their optimization

authors:
Hai Liu
Eric Cheng
Paul Hudak

abstract: Arrows are a popular form of abstract computation. Being more general than monads, they are more broadly applicable, and in particular are a good abstraction for signal processing and dataflow computations. Most notably, arrows form the basis for a domain specific language called Yampa, which has been used in a variety of concrete applications, including animation, robotics, sound synthesis, control systems, and graphical user interfaces. Our primary interest is in better understanding the class of abstract computations captured by Yampa. Unfortunately, arrows are not concrete enough to do this with precision. To remedy this situation we introduce the concept of commutative arrows that capture a kind of non-interference property of concurrent computations. We also add an init operator, and identify a crucial law that captures the causal nature of arrow effects. We call the resulting computational model causal commutative arrows. To study this class of computations in more detail, we define an extension to the simply typed lambda calculus called causal commutative arrows (CCA), and study its properties. Our key contribution is the identification of a normal form for CCA called causal commutative normal form (CCNF). By defining a normalization procedure we have developed an optimization strategy that yields dramatic improvements in performance over conventional implementations of arrows. We have implemented this technique in Haskell, and conducted benchmarks that validate the effectiveness of our approach. When combined with stream fusion, the overall methodology can result in speed-ups of greater than two orders of magnitude.


title: Runtime support for multicore Haskell

authors:
Simon Marlow
Simon L. Peyton Jones
Satnam Singh

abstract: Purely functional programs should run well on parallel hardware because of the absence of side effects, but it has proved hard to realise this potential in practice. Plenty of papers describe promising ideas, but vastly fewer describe real implementations with good wall-clock performance. We describe just such an implementation, and quantitatively explore some of the complex design tradeoffs that make such implementations hard to build. Our measurements are necessarily detailed and specific, but they are reproducible, and we believe that they offer some general insights.

awards: Most Influential ICFP Paper (awarded 2019)


title: Automatically RESTful web applications: marking modular serializable continuations

abstract: Continuation-based Web servers provide distinct advantages over traditional Web application development: expressive power and modularity. This power leads to fewer errors and more interesting applications. Furthermore, these Web servers are more than prototypes; they are used in some real commercial applications. Unfortunately, they pay a heavy price for the additional power in the form of lack of scalability.


title: Control-flow analysis of function calls and returns by abstract interpretation

authors:
Jan Midtgaard
Thomas P. Jensen

abstract: We derive a control-flow analysis that approximates the interprocedural control-flow of both function calls and returns in the presence of first-class functions and tail-call optimization. In addition to an abstract environment, our analysis computes for each expression an abstract control stack, effectively approximating where function calls return across optimized tail calls. The analysis is systematically calculated by abstract interpretation of the stack-based CaEK abstract machine of Flanagan et al. using a series of Galois connections. Abstract interpretation provides a unifying setting in which we 1) prove the analysis equivalent to the composition of a continuation-passing style (CPS) transformation followed by an abstract interpretation of a stack-less CPS machine, and 2) extract an equivalent constraint-based formulation, thereby providing a rational reconstruction of a constraint-based control-flow analysis from abstract interpretation principles.


title: Non-parametric parametricity

authors:
Georg Neis
Derek Dreyer
Andreas Rossberg

abstract: Type abstraction and intensional type analysis are features seemingly at odds-type abstraction is intended to guarantee parametricity and representation independence, while type analysis is inherently non-parametric. Recently, however, several researchers have proposed and implemented "dynamic type generation" as a way to reconcile these features. The idea is that, when one defines an abstract type, one should also be able to generate at run time a fresh type name, which may be used as a dynamic representative of the abstract type for purposes of type analysis. The question remains: in a language with non-parametric polymorphism, does dynamic type generation provide us with the same kinds of abstraction guarantees that we get from parametric polymorphism?


title: Experience report: embedded, parallel computer-vision with a functional DSL

authors:
Ryan Newton
Teresa Ko

abstract: This paper presents our experience using a domain-specific functional language, WaveScript, to build embedded sensing applications used in scientific research. We focus on a recent computervision application for detecting birds in their natural environment. The application was ported from a prototype in C++. In reimplementing the application, we gained a much cleaner factoring of its functionality (through higher-order functions and better interfaces to libraries) and a near-linear parallel speed-up with no additional effort. These benefits are offset by one substantial downside: the lack of familiarity with the language of the original vision researchers, who understandably tried to use the language in the familiar way they use C++ and thus ran into various problems.


title: Experience report: using objective caml to develop safety-critical embedded tools in a certification framework

authors:
Bruno Pagano
Olivier Andrieu
Thomas Moniot
Benjamin Canou
Emmanuel Chailloux
Philippe Wang
Pascal Manoury
Jean-Louis Colaço

abstract: High-level tools have become unavoidable in industrial software development processes. Safety-critical embedded programs don't escape this trend. In the context of safety-critical embedded systems, the development processes follow strict guidelines and requirements. The development quality assurance applies as much to the final embedded code, as to the tools themselves. The French company Esterel Technologies decided in 2006 to base its new SCADE SUITE 6TM certifiable code generator on Objective Caml. This paper outlines how it has been challenging in the context of safety critical software development by the rigorous norms DO-178B, IEC 61508, EN 50128 and such.


title: Lambda, the ultimate TA: using a proof assistant to teach programming language foundations

abstract: Ambitious experiments using proof assistants for programming language research and teaching are all the rage. In this talk, I'll report on one now underway at the University of Pennsylvania and several other sites: a one-semester graduate course in the theory of programming languages presented entirely - every lecture, every homework assignment - in Coq. I'll try to give a sense of what the course is like for both instructors and students, describe some of the most interesting challenges in developing it, and explain why I now believe such machine-assisted courses are the way of the future.


title: Commutative monads, diagrams and knots

abstract: There is certain diverse class of diagram that is found in a variety of branches of mathematics and which all share this property: there is a common scheme for translating all of these diagrams into useful functional code. These diagrams include Bayesian networks, quantum computer circuits [1], trace diagrams for multilinear algebra [2], Feynman diagrams and even knot diagrams [3]. I will show how a common thread lying behind these diagrams is the presence of a commutative monad and I will show how we can use this fact to translate these diagrams directly into Haskell code making use of do-notation for monads. I will also show a number of examples of such translated code at work and use it to solve problems ranging from Bayesian inference to the topological problem of untangling tangled strings. Along the way I hope to give a little insight into the subjects mentioned above and illustrate how a functional programming language can be a valuable tool in mathematical research and experimentation.


title: Parallel concurrent ML

authors:
John H. Reppy
Claudio V. Russo
Yingqi Xiao

abstract: Concurrent ML (CML) is a high-level message-passing language that supports the construction of first-class synchronous abstractions called events. This mechanism has proven quite effective over the years and has been incorporated in a number of other languages. While CML provides a concurrent programming model, its implementation has always been limited to uniprocessors. This limitation is exploited in the implementation of the synchronization protocol that underlies the event mechanism, but with the advent of cheap parallel processing on the desktop (and laptop), it is time for Parallel CML.


title: Implementing first-class polymorphic delimited continuations by a type-directed selective CPS-transform

authors:
Tiark Rompf
Ingo Maier
Martin Odersky

abstract: We describe the implementation of first-class polymorphic delimited continuations in the programming language Scala. We use Scala's pluggable typing architecture to implement a simple type and effect system, which discriminates expressions with control effects from those without and accurately tracks answer type modification incurred by control effects. To tackle the problem of implementing first-class continuations under the adverse conditions brought upon by the Java VM, we employ a selective CPS transform, which is driven entirely by effect-annotated types and leaves pure code in direct style. Benchmarks indicate that this high-level approach performs competitively.


title: Experience report: Haskell in the 'real world': writing a commercial application in a lazy functional lanuage

abstract: I describe the initial attempt of experienced business software developers with minimal functional programming background to write a non-trivial, business-critical application entirely in Haskell. Some parts of the application domain are well suited to a mathematically-oriented language; others are more typically done in languages such as C++.


title: Complete and decidable type inference for GADTs

authors:
Tom Schrijvers
Simon L. Peyton Jones
Martin Sulzmann
Dimitrios Vytiniotis

abstract: GADTs have proven to be an invaluable language extension, for ensuring data invariants and program correctness among others. Unfortunately, they pose a tough problem for type inference: we lose the principal-type property, which is necessary for modular type inference.


title: Safe functional reactive programming through dependent types

authors:
Neil Sculthorpe
Henrik Nilsson

abstract: Functional Reactive Programming (FRP) is an approach to reactive programming where systems are structured as networks of functions operating on signals. FRP is based on the synchronous data-flow paradigm and supports both continuous-time and discrete-time signals (hybrid systems). What sets FRP apart from most other languages for similar applications is its support for systems with dynamic structure and for higher-order reactive constructs.


title: Organizing functional code for parallel execution or, foldl and foldr considered slightly harmful

abstract: Alan Perlis, inverting OscarWilde's famous quip about cynics, once suggested, decades ago, that a Lisp programmer is one who knows the value of everything and the cost of nothing. Now that the conference on Lisp and Functional Programming has become ICFP, some may think that OCaml and Haskell programmers have inherited this (now undeserved) epigram.


title: A theory of typed coercions and its applications

authors:
Nikhil Swamy
Michael W. Hicks
Gavin M. Bierman

abstract: A number of important program rewriting scenarios can be recast as type-directed coercion insertion. These range from more theoretical applications such as coercive subtyping and supporting overloading in type theories, to more practical applications such as integrating static and dynamically typed code using gradual typing, and inlining code to enforce security policies such as access control and provenance tracking. In this paper we give a general theory of type-directed coercion insertion. We specifically explore the inherent tradeoff between expressiveness and ambiguity--the more powerful the strategy for generating coercions, the greater the possibility of several, semantically distinct rewritings for a given program. We consider increasingly powerful coercion generation strategies, work out example applications supported by the increased power (including those mentioned above), and identify the inherent ambiguity problems of each setting, along with various techniques to tame the ambiguities.


title: Attribute grammars fly first-class: how to do aspect oriented programming in Haskell

authors:
Marcos Viera
S. Doaitse Swierstra
Wouter Swierstra

abstract: Attribute Grammars (AGs), a general-purpose formalism for describing recursive computations over data types, avoid the trade-off which arises when building software incrementally: should it be easy to add new data types and data type alternatives or to add new operations on existing data types? However, AGs are usually implemented as a pre-processor, leaving e.g. type checking to later processing phases and making interactive development, proper error reporting and debugging difficult. Embedding AG into Haskell as a combinator library solves these problems.


title: Free theorems involving type constructor classes: functional pearl

abstract: Free theorems are a charm, allowing the derivation of useful statements about programs from their (polymorphic) types alone. We show how to reap such theorems not only from polymorphism over ordinary types, but also from polymorphism over type constructors restricted by class constraints. Our prime application area is that of monads, which form the probably most popular type constructor class of Haskell. To demonstrate the broader scope, we also deal with a transparent way of introducing difference lists into a program, endowed with a neat and general correctness proof.


title: Generic programming with fixed points for mutually recursive datatypes

authors:
Alexey Rodriguez Yakushev
Stefan Holdermans
Andres Löh
Johan Jeuring

abstract: Many datatype-generic functions need access to the recursive positions in the structure of the datatype, and therefore adopt a fixed point view on datatypes. Examples include variants of fold that traverse the data following the recursive structure, or the Zipper data structure that enables navigation along the recursive positions. However, Hindley-Milner-inspired type systems with algebraic datatypes make it difficult to express fixed points for anything but regular datatypes. Many real-life examples such as abstract syntax trees are in fact systems of mutually recursive datatypes and therefore excluded. Using Haskell's GADTs and type families, we describe a technique that allows a fixed-point view for systems of mutually recursive datatypes. We demonstrate that our approach is widely applicable by giving several examples of generic functions for this view, most prominently the Zipper.


title: Partial memoization of concurrency and communication

authors:
Lukasz Ziarek
K. C. Sivaramakrishnan
Suresh Jagannathan

abstract: Memoization is a well-known optimization technique used to eliminate redundant calls for pure functions. If a call to a function f with argument v yields result r, a subsequent call to f with v can be immediately reduced to r without the need to re-evaluate f's body. Understanding memoization in the presence of concurrency and communication is significantly more challenging. For example, if f communicates with other threads, it is not sufficient to simply record its input/output behavior; we must also track inter-thread dependencies induced by these communication actions. Subsequent calls to f can be elided only if we can identify an interleaving of actions from these call-sites that lead to states in which these dependencies are satisfied. Similar issues arise if f spawns additional threads. In this paper, we consider the memoization problem for a higher-order concurrent language whose threads may communicate through synchronous message-based communication. To avoid the need to perform unbounded state space search that may be necessary to determine if all communication dependencies manifest in an earlier call can be satisfied in a later one, we introduce a weaker notion of memoization called partial memoization that gives implementations the freedom to avoid performing some part, if not all, of a previously memoized call. To validate the effectiveness of our ideas, we consider the benefits of memoization for reducing the overhead of recomputation for streaming, server-based, and transactional applications executed on a multi-core machine. We show that on a variety of workloads, memoization can lead to substantial performance improvements without incurring high memory costs.


title: Specifying and verifying sparse matrix codes

authors:
Gilad Arnold
Johannes Hölzl
Ali Sinan Köksal
Rastislav Bodík
Mooly Sagiv

abstract: Sparse matrix formats are typically implemented with low-level imperative programs. The optimized nature of these implementations hides the structural organization of the sparse format and complicates its verification. We define a variable-free functional language (LL) in which even advanced formats can be expressed naturally, as a pipeline-style composition of smaller construction steps. We translate LL programs to Isabelle/HOL and describe a proof system based on parametric predicates for tracking relationship between mathematical vectors and their concrete representations. This proof theory automatically verifies full functional correctness of many formats. We show that it is reusable and extensible to hierarchical sparse formats.


title: Matching lenses: alignment and view update

authors:
Davi M. J. Barbosa
Julien Cretin
Nate Foster
Michael Greenberg
Benjamin C. Pierce

abstract: Bidirectional programming languages are a practical approach to the view update problem. Programs in these languages, called lenses, define both a view and an update policy - i.e., every program can be read as a function mapping sources to views as well as one mapping updated views back to updated sources.


title: Lazy tree splitting

authors:
Lars Bergstrom
Mike Rainey
John H. Reppy
Adam Shaw
Matthew Fluet

abstract: Nested data-parallelism (NDP) is a declarative style for programming irregular parallel applications. NDP languages provide language features favoring the NDP style, efficient compilation of NDP programs, and various common NDP operations like parallel maps, filters, and sum-like reductions. In this paper, we describe the implementation of NDP in Parallel ML (PML), part of the Manticore project. Managing the parallel decomposition of work is one of the main challenges of implementing NDP. If the decomposition creates too many small chunks of work, performance will be eroded by too much parallel overhead. If, on the other hand, there are too few large chunks of work, there will be too much sequential processing and processors will sit idle.


title: Parametricity and dependent types

authors:
Jean-Philippe Bernardy
Patrik Jansson
Ross Paterson

abstract: Reynolds' abstraction theorem shows how a typing judgement in System F can be translated into a relational statement (in second order predicate logic) about inhabitants of the type. We (in second order predicate logic) about inhabitants of the type. We obtain a similar result for a single lambda calculus (a pure type system), in which terms, types and their relations are expressed. Working within a single system dispenses with the need for an interpretation layer, allowing for an unusually simple presentation. While the unification puts some constraints on the type system (which we spell out), the result applies to many interesting cases, including dependently-typed ones.


title: Semantic subtyping with an SMT solver

authors:
Gavin M. Bierman
Andrew D. Gordon
Catalin Hritcu
David E. Langworthy

abstract: We study a first-order functional language with the novel combination of the ideas of refinement type (the subset of a type to satisfy a Boolean expression) and type-test (a Boolean expression testing whether a value belongs to a type). Our core calculus can express a rich variety of typing idioms; for example, intersection, union, negation, singleton, nullable, variant, and algebraic types are all derivable. We formulate a semantics in which expressions denote terms, and types are interpreted as first-order logic formulas. Subtyping is defined as valid implication between the semantics of types. The formulas are interpreted in a specific model that we axiomatize using standard first-order theories. On this basis, we present a novel type-checking algorithm able to eliminate many dynamic tests and to detect many errors statically. The key idea is to rely on an SMT solver to compute subtyping efficiently. Moreover, interpreting types as formulas allows us to call the SMT solver at run-time to compute instances of types.


title: Functional parallel algorithms

abstract: Functional programming presents several important advantages in the design, analysis and implementation of parallel algorithms:


title: Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation

authors:
Edwin C. Brady
Kevin Hammond

abstract: Partial evaluation aims to improve the efficiency of a program by specialising it with respect to some known inputs. In this paper, we show that partial evaluation can be an effective and, unusually, easy to use technique for the efficient implementation of embedded domain-specific languages. We achieve this by exploiting dependent types and by following some simple rules in the definition of the interpreter for the domain-specific language. We present experimental evidence that partial evaluation of programs in domain-specific languages can yield efficient residual programs whose performance is competitive with their Java and C equivalents and which are also, through the use of dependent types, verifiably resource-safe. Using our technique, it follows that a verifiably correct and resource-safe program can also be an efficient program


title: ReCaml: execution state as the cornerstone of reconfigurations

authors:
Jérémy Buisson
Fabien Dagnat

abstract: To fix bugs or to enhance a software system without service disruption, one has to update it dynamically during execution. Most prior dynamic software updating techniques require that the code to be changed is not running at the time of the update. However, this restriction precludes any change to the outermost loops of servers, OS scheduling loops and recursive functions. Permitting a dynamic update to more generally manipulate the program's execution state, including the runtime stack, alleviates this restriction but increases the likelihood of type errors. In this paper we present ReCaml, a language for writing dynamic updates to running programs that views execution state as a delimited continuation. ReCaml includes a novel feature for introspecting continuations called match_cont which is sufficiently powerful to implement a variety of updating policies. We have formalized the core of ReCaml and proved it sound (using the Coq proof assistant), thus ensuring that state-manipulating updates preserve type-safe execution of the updated program. We have implemented ReCaml as an extension to the Caml bytecode interpreter and used it for several examples.


title: The gentle art of levitation

authors:
James Chapman
Pierre-Évariste Dagand
Conor McBride
Peter Morris

abstract: We present a closed dependent type theory whose inductive types are given not by a scheme for generative declarations, but by encoding in a universe. Each inductive datatype arises by interpreting its description - a first-class value in a datatype of descriptions. Moreover, the latter itself has a description. Datatype-generic programming thus becomes ordinary programming. We show some of the resulting generic operations and deploy them in particular, useful ways on the datatype of datatype descriptions itself. Simulations in existing systems suggest that this apparently self-supporting setup is achievable without paradox or infinite regress.


title: Program verification through characteristic formulae

abstract: This paper describes CFML, the first program verification tool based on characteristic formulae. Given the source code of a pure Caml program, this tool generates a logical formula that implies any valid post-condition for that program. One can then prove that the program satisfies a given specification by reasoning interactively about the characteristic formula using a proof assistant such as Coq. Our characteristic formulae improve over Honda et al's total characteristic assertion pairs in that they are expressible in standard higher-order logic, allowing to exploit them in practice to verify programs using existing proof assistants. Our technique has been applied to formally verify more than half of the content of Okasaki's Purely Functional Data Structures reference book


title: Higher-order representation of substructural logics

abstract: We present a technique for higher-order representation of substructural logics such as linear or modal logic. We show that such logics can be encoded in the (ordinary) Logical Framework, without any linear or modal extensions. Using this encoding, metatheoretic proofs about such logics can easily be developed in the Twelf proof assistant.


title: Experience report: growing programming languages for beginning students

authors:
Marcus Crestani
Michael Sperber

abstract: A student learning how to program learns best when the programming language and programming environment cater to her specific needs. These needs are different from the requirements of a professional programmer. Consequently, the design of teaching languages poses challenges different from the design of professional languages. Using a functional language by itself gives advantages over more popular, professional languages, but fully exploiting these advantages requires careful adaptation to the needs of the students' as-is, these languages do not support the students nearly as well as they could. This paper describes our experience adopting the didactic approach of How to Design Programs, focussing on the design process for our own set of teaching languages. We have observed students as they try to program as part of our introductory course, and used these observations to significantly improve the design of these languages. This paper describes the changes we have made, and the journey we took to get there.


title: Fortifying macros

authors:
Ryan Culpepper
Matthias Felleisen

abstract: Existing macro systems force programmers to make a choice between clarity of specification and robustness. If they choose clarity, they must forgo validating significant parts of the specification and thus produce low-quality language extensions. If they choose robustness, they must write in a style that mingles the implementation with the specification and therefore obscures the latter.


title: Total parser combinators

abstract: A monadic parser combinator library which guarantees termination of parsing, while still allowing many forms of left recursion, is described. The library's interface is similar to those of many other parser combinator libraries, with two important differences: one is that the interface clearly specifies which parts of the constructed parsers may be infinite, and which parts have to be finite, using dependent types and a combination of induction and coinduction; and the other is that the parser type is unusually informative.


title: The impact of higher-order state and control effects on local relational reasoning

authors:
Derek Dreyer
Georg Neis
Lars Birkedal

abstract: Reasoning about program equivalence is one of the oldest problems in semantics. In recent years, useful techniques have been developed, based on bisimulations and logical relations, for reasoning about equivalence in the setting of increasingly realistic languages - languages nearly as complex as ML or Haskell. Much of the recent work in this direction has considered the interesting representation independence principles enabled by the use of local state, but it is also important to understand the principles that powerful features like higher-order state and control effects disable. This latter topic has been broached extensively within the framework of game semantics, resulting in what Abramsky dubbed the "semantic cube": fully abstract game-semantic characterizations of various axes in the design space of ML-like languages. But when it comes to reasoning about many actual examples, game semantics does not yet supply a useful technique for proving equivalences.


title: TeachScheme!: a checkpoint

abstract: In 1995, my team and I decided to create an outreach project that would use our research on functional programming to change the K-12 computer science curriculum. We had two different goals in mind. On the one hand, our curriculum should rely on mathematics to teach programming, and it d exploit programming to teach mathematics. All students - not just those who major in computer science - should benefit. On the other hand, our course should demonstrate that introductory programming can focus on program design, not just a specific syntax. We also wished to create a smooth path from a design-oriented introductory course all the way to courses on large software projects.


title: A play on regular expressions: functional pearl

authors:
Sebastian Fischer
Frank Huch
Thomas Wilke

abstract: Cody, Hazel, and Theo, two experienced Haskell programmers and an expert in automata theory, develop an elegant Haskell program for matching regular expressions: (i) the program is purely functional; (ii) it is overloaded over arbitrary semirings, which not only allows to solve the ordinary matching problem but also supports other applications like computing leftmost longest matchings or the number of matchings, all with a single algorithm; (iii) it is more powerful than other matchers, as it can be used for parsing every context-free language by taking advantage of laziness.


title: ML: metalanguage or object language?

abstract: My talk will celebrate Robin Milner's contribution to functional programming via a combination of reminiscences about the early days of ML and speculations about its future.


title: Bidirectionalizing graph transformations

authors:
Soichiro Hidaka
Zhenjiang Hu
Kazuhiro Inaba
Hiroyuki Kato
Kazutaka Matsuda
Keisuke Nakano

abstract: Bidirectional transformations provide a novel mechanism for syn-chronizing and maintaining the consistency of information between input and output. Despite many promising results on bidirectional transformations, these have been limited to the context of relational or XML (tree-like) databases. We challenge the problem of bidirec-tional transformations within the context of graphs, by proposing a formal definition of a well-behaved bidirectional semantics for UnCAL, i.e., a graph algebra for the known UnQL graph query language. The key to our successful formalization is full utiliza-tion of both the recursive and bulk semantics of structural recur-sion on graphs. We carefully refine the existing forward evaluation of structural recursion so that it can produce sufficient trace infor-mation for later backward evaluation. We use the trace information for backward evaluation to reflect in-place updates and deletions on the view to the source, and adopt the universal resolving algorithm for inverse computation and the narrowing technique to tackle the difficult problem with insertion. We prove our bidirectional evalu-ation is well-behaved. Our current implementation is available on-line and confirms the usefulness of our approach with nontrivial applications.


title: Polyvariant flow analysis with higher-ranked polymorphic types and higher-order effect operators

authors:
Stefan Holdermans
Jurriaan Hage

abstract: We present a type and effect system for flow analysis that makes essential use of higher-ranked polymorphism. We show that, for higher-order functions, the expressiveness of higher-ranked types enables us to improve on the precision of conventional let-polymorphic analyses. Modularity and decidability of the analysis are guaranteed by making the analysis of each program parametric in the analyses of its inputs; in particular, we have that higher-order functions give rise to higher-order operations on effects. As flow typing is archetypical to a whole class of type and effect systems, our approach can be used to boost the precision of a wide range of type-based program analyses for higher-order languages.


title: Abstracting abstract machines

authors:
David Van Horn
Matthew Might

abstract: We describe a derivational approach to abstract interpretation that yields novel and transparently sound static analyses when applied to well-established abstract machines. To demonstrate the technique and support our claim, we transform the CEK machine of Felleisen and Friedman, a lazy variant of Krivine's machine, and the stack-inspecting CM machine of Clements and Felleisen into abstract interpretations of themselves. The resulting analyses bound temporal ordering of program events; predict return-flow and stack-inspection behavior; and approximate the flow and evaluation of by-need parameters. For all of these machines, we find that a series of well-known concrete machine refactorings, plus a technique we call store-allocated continuations, leads to machines that abstract into static analyses simply by bounding their stores. We demonstrate that the technique scales up uniformly to allow static analysis of realistic language features, including tail calls, conditionals, side effects, exceptions, first-class continuations, and even garbage collection.

awards: Most Influential ICFP Paper (awarded 2020)


title: Regular, shape-polymorphic, parallel arrays in Haskell

authors:
Gabriele Keller
Manuel M. T. Chakravarty
Roman Leshchinskiy
Simon L. Peyton Jones
Ben Lippmeier

abstract: We present a novel approach to regular, multi-dimensional arrays in Haskell. The main highlights of our approach are that it (1) is purely functional, (2) supports reuse through shape polymorphism, (3) avoids unnecessary intermediate structures rather than relying on subsequent loop fusion, and (4) supports transparent parallelisation.


title: Lolliproc: to concurrency from classical linear logic via curry-howard and control

authors:
Karl Mazurak
Steve Zdancewic

abstract: While many type systems based on the intuitionistic fragment of linear logic have been proposed, applications in programming languages of the full power of linear logic - including double-negation elimination - have remained elusive. Meanwhile, linearity has been used in many type systems for concurrent programs - e.g., session types - which suggests applicability to the problems of concurrent programming, but the ways in which linearity has interacted with concurrency primitives in lambda calculi have remained somewhat ad-hoc. In this paper we connect classical linear logic and concurrent functional programming in the language Lolliproc, which provides simple primitives for concurrency that have a direct logical interpretation and that combine to provide the functionality of session types. Lolliproc features a simple process calculus "under the hood" but hides the machinery of processes from programmers. We illustrate Lolliproc by example and prove soundness, strong normalization, and confluence results, which, among other things, guarantees freedom from deadlocks and race conditions.


title: A certified framework for compiling and executing garbage-collected languages

authors:
Andrew McCreight
Tim Chevalier
Andrew P. Tolmach

abstract: We describe the design, implementation, and use of a machine-certified framework for correct compilation and execution of programs in garbage-collected languages. Our framework extends Leroy's Coq-certified Compcert compiler and Cminor intermediate language. We add: (i) a new intermediate language, GCminor, that includes primitives for allocating memory in a garbage-collected heap and for specifying GC roots; (ii) a precise, low-level specification for a Cminor library for garbage collection; and (iii) a proven semantics-preserving translation from GCminor to Cminor plus the GC library. GCminor neatly encapsulates the interface between mutator and collector code, while remaining simple and flexible enough to be used with a wide variety of source languages and collector styles. Front ends targeting GCminor can be implemented using any compiler technology and any desired degree of verification, including full semantics preservation, type preservation, or informal trust.


title: Rethinking supercompilation

abstract: Supercompilation is a program optimisation technique that is particularly effective at eliminating unnecessary overheads. We have designed a new supercompiler, making many novel choices, including different termination criteria and handling of let bindings. The result is a supercompiler that focuses on simplicity, compiles programs quickly and optimises programs well. We have benchmarked our supercompiler, with some programs running more than twice as fast than when compiled with GHC.


title: Security-typed programming within dependently typed programming

authors:
Jamie Morgenstern
Daniel R. Licata

abstract: Abstract. Several recent security-typed programming languages allow programmers to express and enforce authorization policies governing access to controlled resources. Policies are expressed as propositions in an authorization logic, and enforced by a type system that requires each access to a sensitive resource to be accompanied by a proof. The securitytyped languages described in the literature, such as Aura and PCML5, have been presented as new, stand-alone language designs. In this paper, we instead show how to embed a security-typed programming language within an existing dependently typed programming language, Agda. This language-design strategy allows us to inherit both the metatheoretic results, such as type safety, and the implementation of the host language. Our embedding consists of the following ingredients: First, we represent the syntax and proofs of an authorization logic, Garg and Pfenning’s BL0, using dependent types. Second, we implement a proof search procedure, based on a focused sequent calculus, to ease the burden of constructing proofs. Third, we define an indexed monad of computations on behalf of a principal, with proof-carrying primitive operations. Our work shows that a dependently typed language can be used to prototype a security-typed language, and contributes to the growing body of literature on using dependently typed languages to construct domain-specific type systems. 1


title: Instance chains: type class programming without overlapping instances

authors:
J. Garrett Morris
Mark P. Jones

abstract: Type classes have found a wide variety of uses in Haskell programs, from simple overloading of operators (such as equality or ordering) to complex invariants used to implement type-safe heterogeneous lists or limited subtyping. Unfortunately, many of the richer uses of type classes require extensions to the class system that have been incompletely described in the research literature and are not universally accepted within the Haskell community.


title: The reduceron reconfigured

authors:
Matthew Naylor
Colin Runciman

abstract: The leading implementations of graph reduction all target conventional processors designed for low-level imperative execution. In this paper, we present a processor specially designed to perform graph-reduction. Our processor -- the Reduceron -- is implemented using off-the-shelf reconfigurable hardware. We highlight the low-level parallelism present in sequential graph reduction, and show how parallel memories and dynamic analyses are used in the Reduceron to achieve an average reduction rate of 0.55 function applications per clock-cycle.


title: Experience report: Haskell as a reagent: results and observations on the use of Haskell in a python project

abstract: In system administration, the languages of choice for solving automation tasks are scripting languages, owing to their flexibility, extensive library support and quick development cycle. Functional programming is more likely to be found in software development teams and the academic world.This separation means that system administrators cannot use the most effective tool for a given problem; in an ideal world, we should be able to mix and match different languages, based on the problem at hand.This experience report details our initial introduction and use of Haskell in a mature, medium size project implemented in Python. We also analyse the interaction between the two languages, and show how Haskell has excelled at solving a particular type of real-world problems


title: A fresh look at programming with names and binders

authors:
Nicolas Pouillard
François Pottier

abstract: A wide range of computer programs, including compilers and theorem provers, manipulate data structures that involve names and binding. However, the design of programming idioms which allow performing these manipulations in a safe and natural style has, to a large extent, remained elusive.


title: Distance makes the types grow stronger: a calculus for differential privacy

authors:
Jason Reed
Benjamin C. Pierce

abstract: We want assurances that sensitive information will not be disclosed when aggregate data derived from a database is published. Differential privacy offers a strong statistical guarantee that the effect of the presence of any individual in a database will be negligible, even when an adversary has auxiliary knowledge. Much of the prior work in this area consists of proving algorithms to be differentially private one at a time; we propose to streamline this process with a functional language whose type system automatically guarantees differential privacy, allowing the programmer to write complex privacy-safe query programs in a flexible and compositional way.


title: Using functional programming within an industrial product group: perspectives and perceptions

authors:
David J. Scott
Richard Sharp
Thomas Gazagnaire
Anil Madhavapeddy

abstract: We present a case-study of using OCaml within a large product development project, focussing on both the technical and non-technical issues that arose as a result. We draw comparisons between the OCaml team and the other teams that worked on the project, providing comparative data on hiring patterns and cross-team code contribution.


title: VeriML: typed computation of logical terms inside a language with effects

authors:
Antonis Stampoulis
Zhong Shao

abstract: Modern proof assistants such as Coq and Isabelle provide high degrees of expressiveness and assurance because they support formal reasoning in higher-order logic and supply explicit machine-checkable proof objects. Unfortunately, large scale proof development in these proof assistants is still an extremely difficult and time-consuming task. One major weakness of these proof assistants is the lack of a single language where users can develop complex tactics and decision procedures using a rich programming model and in a typeful manner. This limits the scalability of the proof development process, as users avoid developing domain-specific tactics and decision procedures.


title: Logical types for untyped languages

authors:
Sam Tobin-Hochstadt
Matthias Felleisen

abstract: Programmers reason about their programs using a wide variety of formal and informal methods. Programmers in untyped languages such as Scheme or Erlang are able to use any such method to reason about the type behavior of their programs. Our type system for Scheme accommodates common reasoning methods by assigning variable occurrences a subtype of their declared type based on the predicates prior to the occurrence, a discipline dubbed occurrence typing. It thus enables programmers to enrich existing Scheme code with types, while requiring few changes to the code itself.


title: Combining syntactic and semantic bidirectionalization

authors:
Janis Voigtländer
Zhenjiang Hu
Kazutaka Matsuda
Meng Wang

abstract: Matsuda et al. [2007, ICFP] and Voigtländer [2009, POPL] introduced two techniques that given a source-to-view function provide an update propagation function mapping an original source and an updated view back to an updated source, subject to standard consistency conditions. Being fundamentally different in approach, both techniques have their respective strengths and weaknesses. Here we develop a synthesis of the two techniques to good effect. On the intersection of their applicability domains we achieve more than what a simple union of applying the techniques side by side delivers.


title: Functional pearl: every bit counts

authors:
Dimitrios Vytiniotis
Andrew J. Kennedy

abstract: We show how the binary encoding and decoding of typed data and typed programs can be understood, programmed, and verified with the help of question-answer games. The encoding of a value is determined by the yes/no answers to a sequence of questions about that value; conversely, decoding is the interpretation of binary data as answers to the same question scheme.


title: An equivalence-preserving CPS translation via multi-language semantics

authors:
Amal Ahmed
Matthias Blume

abstract: Language-based security relies on the assumption that all potential attacks follow the rules of the language in question. When programs are compiled into a different language, this is true only if the translation process preserves observational equivalence.