It is our great pleasure to welcome you to Nara, Japan for the 21st ACM SIGPLAN International Conference on Functional Programming: ICFP 2016.
This year’s conference continues its tradition as a forum for researchers, developers, and students to discuss the latest work on the design, implementation, principles, and use of functional programming. The conference covers the entire spectrum of work on functional programming, from theory to practice.
TensorFlow is a machine learning system that operates at large scale and in heterogeneous environments. Its computational model is based on dataflow graphs with mutable state. Graph nodes may be mapped to different machines in a cluster, and within each machine to CPUs, GPUs, and other devices. TensorFlow supports a variety of applications, but it particularly targets training and inference with deep neural networks. It serves as a platform for research and for deploying machine learning systems across many areas, such as speech recognition, computer vision, robotics, information retrieval, and natural language processing.
In this talk, we describe TensorFlow and outline some of its applications. We also discuss the question of what TensorFlow and deep learning may have to do with functional programming. Although TensorFlow is not purely functional, many of its uses are concerned with optimizing functions (during training), then with applying those functions (during inference). These functions are defined as compositions of simple primitives (as is common in functional programming), with internal data representations that are learned rather than manually designed.
TensorFlow is joint work with many other people in the Google Brain team and elsewhere. More information is available at tensorflow.org.
@InProceedings{ICFP16p1,
author = {Martín Abadi},
title = {TensorFlow: Learning Functions at Scale},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {1--1},
doi = {10.1145/2951913.2976746},
year = {2016},
}
Publisher's Version Article Search
Analyzing real-world JavaScript web applications is a challenging task. On top of understanding the semantics of JavaScript, it requires modeling of web documents, platform objects, and interactions between them. Not only the JavaScript language itself but also its usage patterns are extremely dynamic. JavaScript can generate code and run it during evaluation, and most web applications load JavaScript code dynamically. Such dynamic characteristics of JavaScript web applications make pure static analysis approaches inapplicable.
In this talk, we present our attempts to analyze JavaScript web applications in the wild mostly statically using various approaches. From pure JavaScript programs to JavaScript web applications using platform-specific libraries and dynamic code loading, we explain technical challenges in analyzing each of them and how we built an open-source analysis framework for JavaScript, SAFE, that addresses the challenges incrementally.
In spite of active research accomplishments in analysis of JavaScript web applications, many issues still remain to be resolved such as events, callback functions, and hybrid web applications. We discuss possible future research directions and open challenges.
@InProceedings{ICFP16p2,
author = {Sukyoung Ryu},
title = {Journey to Find Bugs in JavaScript Web Applications in the Wild},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {2--2},
doi = {10.1145/2951913.2976747},
year = {2016},
}
Publisher's Version Article Search
Dependent type theories are functional programming languages with types rich enough to do computer-checked mathematics and software verification. Homotopy type theory is a recent area of work that connects dependent type theory to the mathematical disciplines of homotopy theory and higher-dimensional category theory. From a programming point of view, these connections have revealed that all types in dependent type theory support a certain generic program that had not previously been exploited. Specifically, each type can be equipped with computationally relevant witnesses of equality of elements of that type, and all types support a generic program that transports elements along these equalities. One mechanism for equipping types with non-trivial witnesses of equality is Voevodsky’s univalence axiom, which implies that equality of types themselves is witnessed by type isomorphism. Another is higher inductive types, an extended datatype schema that allows identifications between different datatype constructors. While these new mechanisms were originally formulated as axiomatic extensions of type theory, recent work has investigated their computational meaning, leading to the development of new programming languages that better support them. In this talk, I will illustrate what univalence and higher inductive types mean in programming terms. I will also discuss how studying some related semantic settings can reveal additional structure on types; for example, moving from groupoids (categories where all maps are invertible) to general categories yields an account of coercions instead of equalities. Overall, I hope to convey some of the beauty and richness of these connections between disciplines, which we are just beginning to understand.
@InProceedings{ICFP16p3,
author = {Dan Licata},
title = {A Functional Programmer's Guide to Homotopy Type Theory},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {3--3},
doi = {10.1145/2951913.2976748},
year = {2016},
}
Publisher's Version Article Search
The increasing importance of parallelism has motivated the creation of better abstractions for writing parallel software, including structured parallelism using nested algorithmic skeletons. Such approaches provide high-level abstractions that avoid common problems, such as race conditions, and often allow strong cost models to be defined. However, choosing a combination of algorithmic skeletons that yields good parallel speedups for a program on some specific parallel architecture remains a difficult task. In order to achieve this, it is necessary to simultaneously reason both about the costs of different parallel structures and about the semantic equivalences between them. This paper presents a new type-based mechanism that enables strong static reasoning about these properties. We exploit well-known properties of a very general recursion pattern, hylomorphisms, and give a denotational semantics for structured parallel processes in terms of these hylomorphisms. Using our approach, it is possible to determine formally whether it is possible to introduce a desired parallel structure into a program without altering its functional behaviour, and also to choose a version of that parallel structure that minimises some given cost model.
@InProceedings{ICFP16p4,
author = {David Castro and Kevin Hammond and Susmit Sarkar},
title = {Farms, Pipes, Streams and Reforestation: Reasoning about Structured Parallel Processes using Types and Hylomorphisms},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {4--17},
doi = {10.1145/2951913.2951920},
year = {2016},
}
Publisher's Version Article Search
Increasing availability of multicore systems has led to greater focus on the design and implementation of languages for writing parallel programs. Such languages support various abstractions for parallelism, such as fork-join, async-finish, futures. While they may seem similar, these abstractions lead to different semantics, language design and implementation decisions, and can significantly impact the performance of end-user applications.
In this paper, we consider the question of whether it would be possible to unify various paradigms of parallel computing. To this end, we propose a calculus, called dag calculus, that can encode fork-join, async-finish, and futures, and possibly others. We describe dag calculus and its semantics, establish translations from the aforementioned paradigms into dag calculus. These translations establish that dag calculus is sufficiently powerful for encoding programs written in prevailing paradigms of parallelism. We present concurrent algorithms and data structures for realizing dag calculus on multicore hardware and prove that the proposed techniques are consistent with the semantics. Finally, we present an implementation of the calculus and evaluate it empirically by comparing its performance to highly optimized code from prior work. The results show that the calculus is expressive and that it competes well with, and sometimes outperforms, the state of the art.
@InProceedings{ICFP16p18,
author = {Umut A. Acar and Arthur Charguéraud and Mike Rainey and Filip Sieczkowski},
title = {Dag-Calculus: A Calculus for Parallel Computation},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {18--32},
doi = {10.1145/2951913.2951946},
year = {2016},
}
Publisher's Version Article Search
We develop the operational semantics of an untyped probabilistic λ-calculus with continuous distributions, and both hard and soft constraints,as a foundation for universal probabilistic programming languages such as Church, Anglican, and Venture. Our first contribution is to adapt the classic operational semantics of λ-calculus to a continuous setting via creating a measure space on terms and defining step-indexed approximations. We prove equivalence of big-step and small-step formulations of this distribution-based semantics. To move closer to inference techniques, we also define the sampling-based semantics of a term as a function from a trace of random samples to a value. We show that the distribution induced by integration over the space of traces equals the distribution-based semantics. Our second contribution is to formalize the implementation technique of trace Markov chain Monte Carlo (MCMC) for our calculus and to show its correctness. A key step is defining sufficient conditions for the distribution induced by trace MCMC to converge to the distribution-based semantics. To the best of our knowledge, this is the first rigorous correctness proof for trace MCMC for a higher-order functional language, or for a language with soft constraints.
@InProceedings{ICFP16p33,
author = {Johannes Borgström and Ugo Dal Lago and Andrew D. Gordon and Marcin Szymczak},
title = {A Lambda-Calculus Foundation for Universal Probabilistic Programming},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {33--46},
doi = {10.1145/2951913.2951942},
year = {2016},
}
Publisher's Version Article Search
Given an expression that denotes a probability distribution, often we want a corresponding density function, to use in probabilistic inference. Fortunately, the task of finding a density has been automated. It turns out that we can derive a compositional procedure for finding a density, by equational reasoning about integrals, starting with the mathematical specification of what a density is. Moreover, the density found can be run as an estimation algorithm, as well as simplified as an exact formula to improve the estimate.
@InProceedings{ICFP16p47,
author = {Wazim Mohammed Ismail and Chung-chieh Shan},
title = {Deriving a Probability Density Calculator (Functional Pearl)},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {47--59},
doi = {10.1145/2951913.2951922},
year = {2016},
}
Publisher's Version Article Search
Session 2
A New Verified Compiler Backend for CakeML
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, and Michael Norrish (IHPC at A*STAR, Singapore; Chalmers University of Technology, Sweden; Data61 at CSIRO, Australia; UNSW, Australia; University of Cambridge, UK; University of Kent, UK; Australian National University, Australia)
We have developed and mechanically verified a new compiler backend for CakeML.
Our new compiler features a sequence of intermediate languages that allows it to incrementally compile away high-level features and enables verification at the right levels of semantic detail.
In this way, it resembles mainstream (unverified) compilers for strict functional languages.
The compiler supports efficient curried multi-argument functions, configurable data representations, exceptions that unwind the call stack, register allocation, and more.
The compiler targets several architectures: x86-64, ARMv6, ARMv8, MIPS-64, and RISC-V.
In this paper, we present the overall structure of the compiler, including its 12 intermediate languages, and explain how everything fits together.
We focus particularly on the interaction between the verification of the register allocator and the garbage collector, and memory representations.
The entire development has been carried out within the HOL4 theorem prover.
@InProceedings{ICFP16p60,
author = {Yong Kiam Tan and Magnus O. Myreen and Ramana Kumar and Anthony Fox and Scott Owens and Michael Norrish},
title = {A New Verified Compiler Backend for CakeML},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {60--73},
doi = {10.1145/2951913.2951924},
year = {2016},
}
Publisher's Version Article Search
The λ-calculus is popular as an intermediate language for practical compilers. But in the world of logic it has a lesser-known twin, born at the same time, called the sequent calculus. Perhaps that would make for a good intermediate language, too? To explore this question we designed Sequent Core, a practically-oriented core calculus based on the sequent calculus, and used it to re-implement a substantial chunk of the Glasgow Haskell Compiler.
@InProceedings{ICFP16p74,
author = {Paul Downen and Luke Maurer and Zena M. Ariola and Simon Peyton Jones},
title = {Sequent Calculus as a Compiler Intermediate Language},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {74--88},
doi = {10.1145/2951913.2951931},
year = {2016},
}
Publisher's Version Article Search Info
Refinement through Restraint: Bringing Down the Cost of Verification
Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell, and Gerwin Klein (UNSW, Australia; Data61, Australia; University of Pennsylvania, USA; University of Melbourne, Australia)
We present a framework aimed at significantly reducing the cost of verifying certain classes of systems software, such as file systems. Our framework allows for equational reasoning about systems code written in our new language, Cogent. Cogent is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. Linear types allow us to assign two semantics to the language: one imperative, suitable for efficient C code generation; and one functional, suitable for equational reasoning and verification. As Cogent is a restricted language, it is designed to easily interoperate with existing C functions and to connect to existing C verification frameworks.
Our framework is based on certifying compilation: For a well-typed Cogent program, our compiler produces C code, a high-level shallow embedding of its semantics in Isabelle/HOL, and a proof that the C code correctly refines this embedding. Thus one can reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C. The compiler certificate is a series of language-level proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL.
@InProceedings{ICFP16p89,
author = {Liam O'Connor and Zilin Chen and Christine Rizkallah and Sidney Amani and Japheth Lim and Toby Murray and Yutaka Nagashima and Thomas Sewell and Gerwin Klein},
title = {Refinement through Restraint: Bringing Down the Cost of Verification},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {89--102},
doi = {10.1145/2951913.2951940},
year = {2016},
}
Publisher's Version Article Search Info
A fully abstract compiler guarantees that two source components are observationally equivalent in the source language if and only if their translations are observationally equivalent in the target. Full abstraction implies the translation is secure: target-language attackers can make no more observations of a compiled component than a source-language attacker interacting with the original source component. Proving full abstraction for realistic compilers is challenging because realistic target languages contain features (such as control effects) unavailable in the source, while proofs of full abstraction require showing that every target context to which a compiled component may be linked can be back-translated to a behaviorally equivalent source context.
We prove the first full abstraction result for a translation whose target language contains exceptions, but the source does not. Our translation---specifically, closure conversion of simply typed λ-calculus with recursive types---uses types at the target level to ensure that a compiled component is never linked with attackers that have more distinguishing power than source-level attackers. We present a new back-translation technique based on a shallow embedding of the target language into the source language at a dynamic type. Then boundaries are inserted that mediate terms between the untyped embedding and the strongly-typed source. This technique allows back-translating non-terminating programs, target features that are untypeable in the source, and well-bracketed effects.
@InProceedings{ICFP16p103,
author = {Max S. New and William J. Bowman and Amal Ahmed},
title = {Fully Abstract Compilation via Universal Embedding},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {103--116},
doi = {10.1145/2951913.2951941},
year = {2016},
}
Publisher's Version Article Search Info
Contracts feel misunderstood, especially those with a higher-order soul. While software engineers appreciate contracts as tools for articulating the interface between components, functional programmers desperately search for their types and meaning, completely forgetting about their pragmatics.
This gem presents a novel analysis of contract systems. Applied to the higher-order kind, this analysis reveals their large and clearly unappreciated software engineering potential. Three sample applications illustrate where this kind of exploration may lead.
@InProceedings{ICFP16p117,
author = {Christos Dimoulas and Max S. New and Robert Bruce Findler and Matthias Felleisen},
title = {Oh Lord, Please Don't Let Contracts Be Misunderstood (Functional Pearl)},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {117--131},
doi = {10.1145/2951913.2951930},
year = {2016},
}
Publisher's Version Article Search
Incremental computation aims to speed up re-runs of a program after
its inputs have been modified slightly. It works by recording a trace
of the program's first run and propagating changes through the trace
in incremental runs, trying to re-use as much of the original trace as
possible. The recent work CostIt is a type and effect system to
establish the time complexity of incremental runs of a program, as a
function of input changes. However, CostIt is limited in two
ways. First, it prohibits input changes that influence control
flow. This makes it impossible to type programs that, for instance,
branch on inputs that may change. Second, the soundness of CostIt
is proved relative to an abstract cost semantics, but it is unclear
how the semantics can be realized.
In this paper, we address both these limitations. We present DuCostIt,
a re-design of CostIt, that combines reasoning about costs of
change propagation and costs of from-scratch evaluation. The latter
lifts the restriction on control flow changes. To obtain the type
system, we refine Flow Caml, a type system for information flow
analysis, with cost effects. Additionally, we inherit from CostIt
index refinements to track data structure sizes and a co-monadic
type. Using a combination of binary and unary step-indexed logical
relations, we prove DuCostIt's cost analysis sound relative to not
only an abstract cost semantics, but also a concrete semantics, which
is obtained by translation to an ML-like language.
@InProceedings{ICFP16p132,
author = {Ezgi Çiçek and Zoe Paraskevopoulou and Deepak Garg},
title = {A Type Theory for Incremental Computational Complexity with Control Flow Changes},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {132--145},
doi = {10.1145/2951913.2951950},
year = {2016},
}
Publisher's Version Article Search
We consider the problem of how to compactly encode simply-typed λ-terms into bit strings. The work has been motivated by Kobayashi et al.’s recent work on higher-order data compression, where data are encoded as functional programs (or, λ-terms) that generate them. To exploit its good compression power, the compression scheme has to come with a method for compactly encoding the λ-terms into bit strings. To this end, we propose two type-based bit-encoding schemes; the first one encodes a λ-term into a sequence of symbols by using type information, and then applies arithmetic coding to convert the sequence to a bit string. The second one is more sophisticated; we prepare a context-free grammar (CFG) that describes only well-typed terms, and then use a variation of arithmetic coding specialized for the CFG. We have implemented both schemes and confirmed that they often output more compact codes than previous bit encoding schemes for λ-terms.
@InProceedings{ICFP16p146,
author = {Kotaro Takeda and Naoki Kobayashi and Kazuya Yaguchi and Ayumi Shinohara},
title = {Compact Bit Encoding Schemes for Simply-Typed Lambda-Terms},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {146--157},
doi = {10.1145/2951913.2951918},
year = {2016},
}
Publisher's Version Article Search
The queueing-glueing algorithm is the nickname we give to an algorithmic pattern
that provides amortised linear time solutions to a number of optimal list
partition problems that have a peculiar property: at various moments we know that
two of three candidate solutions could be optimal. The algorithm works by
keeping a queue of lists, glueing them from one end, while chopping from the
other end, hence the name. We give a formal derivation of the algorithm, and
demonstrate it with several non-trivial examples.
@InProceedings{ICFP16p158,
author = {Shin-Cheng Mu and Yu-Hsi Chiang and Yu-Han Lyu},
title = {Queueing and Glueing for Optimal Partitioning (Functional Pearl)},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {158--167},
doi = {10.1145/2951913.2951923},
year = {2016},
}
Publisher's Version Article Search Info
The combination of non-determinism and sorting is mostly associated with permutation sort, a sorting algorithm that is not very useful for sorting and has an awful running time.
In this paper we look at the combination of non-determinism and sorting in a different light: given a sorting function, we apply it to a non-deterministic predicate to gain a function that enumerates permutations of the input list. We get to the bottom of necessary properties of the sorting algorithms and predicates in play as well as discuss variations of the modelled non-determinism.
On top of that, we formulate and prove a theorem stating that no matter which sorting function we use, the corresponding permutation
function enumerates all permutations of the input list. We use free theorems, which are derived from the type of a function
alone, to prove the statement.
@InProceedings{ICFP16p168,
author = {Jan Christiansen and Nikita Danilenko and Sandra Dylus},
title = {All Sorts of Permutations (Functional Pearl)},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {168--179},
doi = {10.1145/2951913.2951949},
year = {2016},
}
Publisher's Version Article Search
Hop.js is a multitier programming environment for JavaScript. It
allows a single JavaScript program to describe the client-side and the
server-side components of a web application. Its runtime environment
ensures consistent executions of the application on the server and on
the client.
This paper overviews the Hop.js design. It shows the JavaScript
extensions that makes it possible to conceive web applications
globally. It presents how Hop.js interacts with the outside world. It
also briefly presents the Hop.js implementation. It presents the
Hop.js web server implementation, the handling of server-side
parallelism, and the JavaScript and HTML compilers.
@InProceedings{ICFP16p180,
author = {Manuel Serrano and Vincent Prunet},
title = {A Glimpse of Hopjs},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {180--192},
doi = {10.1145/2951913.2951916},
year = {2016},
}
Publisher's Version Article Search Info
This paper documents our experience of adapting and using the QuickCheck-style approach for extensive randomised property-based testing of computational geometry algorithms.
The need in rigorous evaluation of computational geometry procedures has naturally arisen in our quest of organising a medium-size programming contest for second year university students—an experiment we conducted as an attempt to introduce them to computational geometry. The main effort in organising the event was implementation of a solid infrastructure for testing and ranking solutions. For this, we employed functional programming techniques. The choice of the language and the paradigm made it possible for us to engineer, from scratch and in a very short period of time, a series of robust geometric primitives and algorithms, as well as implement a scalable framework for their randomised testing.
We describe the main insights, enabling efficient random testing of geometric procedures, and report on our experience of using the testing framework, which helped us to detect and fix a number of issues not just in our programming artefacts, but also in the published algorithms we had implemented.
@InProceedings{ICFP16p193,
author = {Ilya Sergey},
title = {Experience Report: Growing and Shrinking Polygons for Random Testing of Computational Geometry Algorithms},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {193--199},
doi = {10.1145/2951913.2951927},
year = {2016},
}
Publisher's Version Article Search Info
The vertex-centric programming model, known as “think like a vertex”, is being used more and more to support various big graph processing methods through iterative supersteps that execute in parallel a user-defined vertex program over each vertex of a graph. However, the imperative and message-passing style of existing systems makes defining a vertex program unintuitive. In this paper, we show that one can benefit more from “Thinking like a vertex” by “Behaving like a function” rather than “Acting like a procedure” with full use of side effects and explicit control of message passing, state, and termination. We propose a functional approach to vertex-centric graph processing in which the computation at every vertex is abstracted as a higher-order function and present Fregel, a new domain-specific language. Fregel has clear functional semantics, supports declarative description of vertex computation, and can be automatically translated into Pregel, an emerging imperative-style distributed graph processing framework, and thereby achieve promising performance. Experimental results for several typical examples show the promise of this functional approach.
@InProceedings{ICFP16p200,
author = {Kento Emoto and Kiminori Matsuzaki and Zhenjiang Hu and Akimasa Morihata and Hideya Iwasaki},
title = {Think Like a Vertex, Behave Like a Function! A Functional DSL for Vertex-Centric Big Graph Processing},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {200--213},
doi = {10.1145/2951913.2951938},
year = {2016},
}
Publisher's Version Article Search
Datalog may be considered either an unusually powerful query language or a
carefully limited logic programming language. Datalog is declarative,
expressive, and optimizable, and has been applied successfully in a wide
variety of problem domains. However, most use-cases require extending Datalog
in an application-specific manner. In this paper we define Datafun, an
analogue of Datalog supporting higher-order functional programming. The key
idea is to track monotonicity with types.
@InProceedings{ICFP16p214,
author = {Michael Arntzenius and Neelakantan R. Krishnaswami},
title = {Datafun: A Functional Datalog},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {214--227},
doi = {10.1145/2951913.2951948},
year = {2016},
}
Publisher's Version Article Search
Static type errors are a common stumbling block for newcomers to typed functional languages. We present a dynamic approach to explaining type errors by generating counterexample witness inputs that illustrate how an ill-typed program goes wrong. First, given an ill-typed function, we symbolically execute the body to synthesize witness values that make the program go wrong. We prove that our procedure synthesizes general witnesses in that if a witness is found, then for all inhabited input types, there exist values that can make the function go wrong. Second, we show how to extend the above procedure to produce a reduction graph that can be used to interactively visualize and debug witness executions. Third, we evaluate the coverage of our approach on two data sets comprising over 4,500 ill-typed student programs. Our technique is able to generate witnesses for 88% of the programs, and our reduction graph yields small counterexamples for 81% of the witnesses. Finally, we evaluate whether our witnesses help students understand and fix type errors, and find that students presented with our witnesses show a greater understanding of type errors than those presented with a standard error message.
@InProceedings{ICFP16p228,
author = {Eric L. Seidel and Ranjit Jhala and Westley Weimer},
title = {Dynamic Witnesses for Static Type Errors (or, Ill-Typed Programs Usually Go Wrong)},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {228--242},
doi = {10.1145/2951913.2951915},
year = {2016},
}
Publisher's Version Article Search
We propose an automated method for disproving fair termination of higher-order functional programs, which is complementary to Murase et al.’s recent method for proving fair termination. A program is said to be fair terminating if it has no infinite execution trace that satisfies a given fairness constraint. Fair termination is an important property because program verification problems for arbitrary ω-regular temporal properties can be transformed to those of fair termination. Our method reduces the problem of disproving fair termination to higher-order model checking by using predicate abstraction and CEGAR. Given a program, we convert it to an abstract program that generates an approximation of the (possibly infinite) execution traces of the original program, so that the original program has a fair infinite execution trace if the tree generated by the abstract program satisfies a certain property. The method is a non-trivial extension of Kuwahara et al.’s method for disproving plain termination.
@InProceedings{ICFP16p243,
author = {Keiichi Watanabe and Ryosuke Sato and Takeshi Tsukada and Naoki Kobayashi},
title = {Automatically Disproving Fair Termination of Higher-Order Functional Programs},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {243--255},
doi = {10.1145/2951913.2951919},
year = {2016},
}
Publisher's Version Article Search
The development of concurrent separation logic (CSL) has
sparked a long line of work on modular verification of sophisticated
concurrent programs. Two of the most important features supported by
several existing extensions to CSL are higher-order
quantification and custom ghost state. However, none of the
logics that support both of these features reap the full potential of
their combination. In particular, none of them provide general
support for a feature we dub "higher-order ghost state": the
ability to store arbitrary higher-order separation-logic predicates in
ghost variables.
In this paper, we propose higher-order ghost state as a interesting
and useful extension to CSL, which we formalize in the framework of
Jung et al.'s recently developed Iris logic. To justify its soundness,
we develop a novel algebraic structure called CMRAs ("cameras"),
which can be thought of as "step-indexed partial commutative
monoids". Finally, we show that Iris proofs utilizing higher-order
ghost state can be effectively formalized in Coq, and discuss the
challenges we faced in formalizing them.
@InProceedings{ICFP16p256,
author = {Ralf Jung and Robbert Krebbers and Lars Birkedal and Derek Dreyer},
title = {Higher-Order Ghost State},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {256--269},
doi = {10.1145/2951913.2951943},
year = {2016},
}
Publisher's Version Article Search Info
Dependently typed languages such as Agda, Coq and Idris use a syntactic first-order unification algorithm to check definitions by dependent pattern matching. However, these algorithms don’t adequately consider the types of the terms being unified, leading to various unintended results. As a consequence, they require ad hoc restrictions to preserve soundness, but this makes them very hard to prove correct, modify, or extend.
This paper proposes a framework for reasoning formally about unification in a dependently typed setting. In this framework, unification rules compute not just a unifier but also a corresponding correctness proof in the form of an equivalence between two sets of equations. By rephrasing the standard unification rules in a proof-relevant manner, they are guaranteed to preserve soundness of the theory. In addition, it enables us to safely add new rules that can exploit the dependencies between the types of equations.
Using our framework, we reimplemented the unification algorithm used by Agda. As a result, we were able to replace previous ad hoc restrictions with formally verified unification rules, fixing a number of bugs in the process. We are convinced this will also enable the addition of new and interesting unification rules in the future, without compromising soundness along the way.
@InProceedings{ICFP16p270,
author = {Jesper Cockx and Dominique Devriese and Frank Piessens},
title = {Unifiers as Equivalences: Proof-Relevant Unification of Dependently Typed Data},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {270--283},
doi = {10.1145/2951913.2951917},
year = {2016},
}
Publisher's Version Article Search
Many programming languages and proof assistants are defined by elaboration from a high-level language with a great deal of implicit information to a highly explicit core language. In many advanced languages, these elaboration facilities contain powerful tools for program construction, but these tools are rarely designed to be repurposed by users. We describe elaborator reflection, a paradigm for metaprogramming in which the elaboration machinery is made directly available to metaprograms, as well as a concrete realization of elaborator reflection in Idris, a functional language with full dependent types. We demonstrate the applicability of Idris’s reflected elaboration framework to a number of realistic problems, we discuss the motivation for the specific features of its design, and we explore the broader meaning of elaborator reflection as it can relate to other languages.
@InProceedings{ICFP16p284,
author = {David Christiansen and Edwin Brady},
title = {Elaborator Reflection: Extending Idris in Idris},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {284--297},
doi = {10.1145/2951913.2951932},
year = {2016},
}
Publisher's Version Article Search
Full-spectrum dependent types promise to enable the development of correct-by-construction software. However, even certified software needs to interact with simply-typed or untyped programs, be it to perform system calls, or to use legacy libraries. Trading static guarantees for runtime checks, the dependent interoperability framework provides
a mechanism by which simply-typed values can safely be coerced to dependent types and, conversely, dependently-typed programs can defensively be exported to a simply-typed application. In this paper, we give a semantic account of dependent interoperability. Our presentation relies on and is guided by a pervading notion of type equivalence, whose importance has been emphasized in recent work on homotopy type theory. Specifically, we develop the notion of partial type equivalences as a key foundation for dependent interoperability. Our framework is developed in Coq; it is thus constructive and verified in the strictest sense of the terms. Using our library, users can specify domain-specific partial equivalences between data structures. Our library then takes care of the (sometimes, heavy) lifting that leads to interoperable programs. It thus becomes possible, as we shall illustrate, to internalize and hand-tune the extraction of dependently-typed programs to interoperable OCaml programs within Coq itself.
@InProceedings{ICFP16p298,
author = {Pierre-Evariste Dagand and Nicolas Tabareau and Éric Tanter},
title = {Partial Type Equivalences for Verified Dependent Interoperability},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {298--310},
doi = {10.1145/2951913.2951933},
year = {2016},
}
Publisher's Version Article Search Info
Galois connections are a foundational tool for structuring abstraction in
semantics and their use lies at the heart of the theory of abstract
interpretation. Yet, mechanization of Galois connections remains limited to
restricted modes of use, preventing their general application in mechanized
metatheory and certified programming.
This paper presents constructive Galois connections, a variant of Galois
connections that is effective both on paper and in proof assistants; is
complete with respect to a large subset of classical Galois connections; and
enables more general reasoning principles, including the "calculational" style
advocated by Cousot.
To design constructive Galois connection we identify a restricted mode of use
of classical ones which is both general and amenable to mechanization in
dependently-typed functional programming languages. Crucial to our metatheory
is the addition of monadic structure to Galois connections to control a
"specification effect". Effectful calculations may reason classically, while
pure calculations have extractable computational content. Explicitly moving
between the worlds of specification and implementation is enabled by our
metatheory.
To validate our approach, we provide two case studies in mechanizing existing
proofs from the literature: one uses calculational abstract interpretation to
design a static analyzer, the other forms a semantic basis for gradual typing.
Both mechanized proofs closely follow their original paper-and-pencil
counterparts, employ reasoning principles not captured by previous
mechanization approaches, support the extraction of verified algorithms, and
are novel.
@InProceedings{ICFP16p311,
author = {David Darais and David Van Horn},
title = {Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {311--324},
doi = {10.1145/2951913.2951934},
year = {2016},
}
Publisher's Version Article Search
Abstract interpretation provides advanced techniques to infer numerical invariants on programs. There is an abundant literature about numerical abstract domains that operate on scalar variables. This work deals with lifting these techniques to a realistic C memory model. We present an abstract memory functor that takes as argument any standard numerical abstract domain, and builds a memory abstract domain that finely tracks properties about memory contents, taking into account union types, pointer arithmetic and type casts. This functor is implemented and verified inside the Coq proof assistant with respect to the CompCert compiler memory model. Using the Coq extraction mechanism, it is fully executable and used by the Verasco C static analyzer.
@InProceedings{ICFP16p325,
author = {Sandrine Blazy and Vincent Laporte and David Pichardie},
title = {An Abstract Memory Functor for Verified C Static Analyzers},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {325--337},
doi = {10.1145/2951913.2951937},
year = {2016},
}
Publisher's Version Article Search Info
Generalized Algebraic Dataypes, or simply GADTs, can encode non-trivial properties in the types of the constructors. Once such properties are encoded in a datatype, however, all code manipulating that datatype must provide proof that it maintains these properties in order to typecheck. In this paper, we take a step towards gradualizing these obligations. We introduce a tool, Ghostbuster, that produces simplified versions of GADTs which elide selected type parameters, thereby weakening the guarantees of the simplified datatype in exchange for reducing the obligations necessary to manipulate it. Like ornaments, these simplified datatypes preserve the recursive structure of the original, but unlike ornaments we focus on information-preserving bidirectional transformations. Ghostbuster generates type-safe conversion functions between the original and simplified datatypes, which we prove are the identity function when composed. We evaluate a prototype tool for Haskell against thousands of GADTs found on the Hackage package database, generating simpler Haskell'98 datatypes and round-trip conversion functions between the two.
@InProceedings{ICFP16p338,
author = {Trevor L. McDonell and Timothy A. K. Zakian and Matteo Cimini and Ryan R. Newton},
title = {Ghostbuster: A Tool for Simplifying and Converting GADTs},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {338--350},
doi = {10.1145/2951913.2951914},
year = {2016},
}
Publisher's Version Article Search Artifacts Available
Indexed data types allow us to specify and verify many interesting invariants about finite data in a general purpose programming language. In this paper we investigate the dual idea: indexed codata types, which allow us to describe data-dependencies about infinite data structures. Unlike finite data which is defined by constructors, we define infinite data by observations. Dual to pattern matching on indexed data which may refine the type indices, we define copattern matching on indexed codata where type indices guard observations we can make.
Our key technical contributions are three-fold: first, we extend Levy's call-by-push value language with support for indexed (co)data and deep (co)pattern matching; second, we provide a clean foundation for dependent (co)pattern matching using equality constraints; third, we describe a small-step semantics using a continuation-based abstract machine, define coverage for indexed (co)patterns, and prove type safety. This is an important step towards building a foundation where (co)data type definitions and dependent types can coexist.
@InProceedings{ICFP16p351,
author = {David Thibodeau and Andrew Cave and Brigitte Pientka},
title = {Indexed Codata Types},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {351--363},
doi = {10.1145/2951913.2951929},
year = {2016},
}
Publisher's Version Article Search
Dunfield showed that a simply typed core calculus with intersection types and a merge operator is able to capture various programming language features. While his calculus is type-safe, it is not coherent: different derivations for the same expression can elaborate to expressions that evaluate to different values. The lack of coherence is an important disadvantage for adoption of his core calculus in implementations of programming languages, as the semantics of the programming language becomes implementation-dependent.
This paper presents λ_i: a coherent and type-safe calculus with a form of intersection types and a merge operator. Coherence is achieved by ensuring that intersection types are disjoint and programs are sufficiently annotated to avoid type ambiguity. We propose a definition of disjointness where two types A and B are disjoint only if certain set of types are common supertypes of A and B. We investigate three different variants of λ_i, with three variants of disjointness. In the simplest variant, which does not allow ⊤ types, two types are disjoint if they do not share any common supertypes at all. The other two variants introduce ⊤ types and refine the notion of disjointness to allow two types to be disjoint when the only the set of common supertypes are top-like. The difference between the two variants with ⊤ types is on the definition of top-like types, which has an impact on which types are allowed on intersections. We present a type system that prevents intersection types that are not disjoint, as well as an algorithmic specifications to determine whether two types are disjoint for all three variants.
@InProceedings{ICFP16p364,
author = {Bruno C. d. S. Oliveira and Zhiyuan Shi and João Alpuim},
title = {Disjoint Intersection Types},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {364--377},
doi = {10.1145/2951913.2951945},
year = {2016},
}
Publisher's Version Article Search
Set-Theoretic Types for Polymorphic Variants
Giuseppe Castagna, Tommaso Petrucciani, and Kim Nguyễn (University of Paris Diderot, France; University of Genoa, Italy; University of Paris-Sud, France)
Polymorphic variants are a useful feature of the OCaml language whose
current definition and implementation rely on kinding constraints to
simulate a subtyping relation via unification. This yields an awkward
formalization and results in a type system whose behaviour is in some
cases unintuitive and/or unduly restrictive.
In this work, we present an alternative formalization of polymorphic
variants, based on set-theoretic types and subtyping, that yields
a cleaner and more streamlined system. Our formalization is more
expressive than the current one (it types more programs while preserving
type safety), it can internalize some meta-theoretic properties, and it
removes some pathological cases of the current implementation resulting
in a more intuitive and, thus, predictable type system.
More generally, this work shows how to add full-fledged union types to
functional languages of the ML family that usually rely on the
Hindley-Milner type system. As an aside, our system also improves
the theory of semantic subtyping, notably by proving completeness for
the type reconstruction algorithm.
@InProceedings{ICFP16p378,
author = {Giuseppe Castagna and Tommaso Petrucciani and Kim Nguyễn},
title = {Set-Theoretic Types for Polymorphic Variants},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {378--391},
doi = {10.1145/2951913.2951928},
year = {2016},
}
Publisher's Version Article Search Info
An important feature of functional programs is that they are parallel by default. Implementing an efficient parallel functional language, however, is a major challenge, in part because the high rate of allocation and freeing associated with functional programs requires an efficient and scalable memory manager.
In this paper, we present a technique for parallel memory management for strict functional languages with nested parallelism. At the highest level of abstraction, the approach consists of a technique to organize memory as a hierarchy of heaps, and an algorithm for performing automatic memory reclamation by taking advantage of a disentanglement property of parallel functional programs. More specifically, the idea is to assign to each parallel task its own heap in memory and organize the heaps in a hierarchy/tree that mirrors the hierarchy of tasks.
We present a nested-parallel calculus that specifies hierarchical heaps and prove in this calculus a disentanglement property, which prohibits a task from accessing objects allocated by another task that might execute in parallel. Leveraging the disentanglement property, we present a garbage collection technique that can operate on any subtree in the memory hierarchy concurrently as other tasks (and/or other collections) proceed in parallel. We prove the safety of this collector by formalizing it in the context of our parallel calculus. In addition, we describe how the proposed techniques can be implemented on modern shared-memory machines and present a prototype implementation as an extension to MLton, a high-performance compiler for the Standard ML language. Finally, we evaluate the performance of this implementation on a number of parallel benchmarks.
@InProceedings{ICFP16p392,
author = {Ram Raghunathan and Stefan K. Muller and Umut A. Acar and Guy Blelloch},
title = {Hierarchical Memory Management for Parallel Programs},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {392--406},
doi = {10.1145/2951913.2951935},
year = {2016},
}
Publisher's Version Article Search
The polyvariance of a static analysis is the degree to which it structurally differentiates approximations of program values. Polyvariant techniques come in a number of different flavors that represent alternative heuristics for managing the trade-off an analysis strikes between precision and complexity. For example, call sensitivity supposes that values will tend to correlate with recent call sites, object sensitivity supposes that values will correlate with the allocation points of related objects, the Cartesian product algorithm supposes correlations between the values of arguments to the same function, and so forth.
In this paper, we describe a unified methodology for implementing and understanding polyvariance in a higher-order setting (i.e., for control-flow analyses). We do this by extending the method of abstracting abstract machines (AAM), a systematic approach to producing an abstract interpretation of abstract-machine semantics. AAM eliminates recursion within a language’s semantics by passing around an explicit store, and thus places importance on the strategy an analysis uses for allocating abstract addresses within the abstract heap or store. We build on AAM by showing that the design space of possible abstract allocators exactly and uniquely corresponds to the design space of polyvariant strategies. This allows us to both unify and generalize polyvariance as tunings of a single function. Changes to the behavior of this function easily recapitulate classic styles of analysis and produce novel variations, combinations of techniques, and fundamentally new techniques.
@InProceedings{ICFP16p407,
author = {Thomas Gilray and Michael D. Adams and Matthew Might},
title = {Allocation Characterizes Polyvariance: A Unified Methodology for Polyvariant Control-Flow Analysis},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {407--420},
doi = {10.1145/2951913.2951936},
year = {2016},
}
Publisher's Version Article Search
This paper presents a concurrent garbage collection method
for functional programs running on a multicore processor.
It is a concurrent extension of our bitmap-marking non-moving
collector with Yuasa's snapshot-at-the-beginning strategy.
Our collector is unobtrusive in the sense of
the Doligez-Leroy-Gonthier collector;
the collector does not stop any mutator thread nor does it
force them to synchronize globally.
The only critical sections between a mutator and the collector are
the code to enqueue/dequeue a 32 kB allocation segment to/from a global
segment list and the write barrier code to push an object pointer onto
the collector's stack.
Most of these data structures can be implemented in standard
lock-free data structures.
This achieves both efficient allocation and unobtrusive collection
in a multicore system.
The proposed method has been implemented in SML#, a
full-scale Standard ML compiler supporting multiple native threads on
multicore CPUs.
Our benchmark tests show a drastically short pause time
with reasonably low overhead compared to the sequential bitmap-marking
collector.
@InProceedings{ICFP16p421,
author = {Katsuhiro Ueno and Atsushi Ohori},
title = {A Fully Concurrent Garbage Collector for Functional Programs on Multicore Processors},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {421--433},
doi = {10.1145/2951913.2951944},
year = {2016},
}
Publisher's Version Article Search
Session types provide static guarantees that concurrent programs respect communication protocols. We give a novel account of recursive session types in the context of GV, a small concurrent extension of the linear λ-calculus. We extend GV with recursive types and catamorphisms, following the initial algebra semantics of recursion, and show that doing so naturally gives rise to recursive session types. We show that this principled approach to recursion resolves long-standing problems in the treatment of duality for recursive session types.
We characterize the expressiveness of GV concurrency by giving a CPS translation to (non-concurrent) λ-calculus and proving that reduction in GV is simulated by full reduction in λ-calculus. This shows that GV remains terminating in the presence of positive recursive types, and that such arguments extend to other extensions of GV, such as polymorphism or non-linear types, by appeal to normalization results for sequential λ-calculi. We also show that GV remains deadlock free and deterministic in the presence of recursive types.
Finally, we extend CP, a session-typed process calculus based on linear logic, with recursive types, and show that doing so preserves the connection between reduction in GV and cut elimination in CP.
@InProceedings{ICFP16p434,
author = {Sam Lindley and J. Garrett Morris},
title = {Talking Bananas: Structural Recursion for Session Types},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {434--447},
doi = {10.1145/2951913.2951921},
year = {2016},
}
Publisher's Version Article Search
We present a linear functional calculus with both the safety guarantees expressible with linear types and the rich language of combinators and composition provided by functional programming. Unlike previous combinations of linear typing and functional programming, we compromise neither the linear side (for example, our linear values are first-class citizens of the language) nor the functional side (for example, we do not require duplicate definitions of compositions for linear and unrestricted functions). To do so, we must generalize abstraction and application to encompass both linear and unrestricted functions. We capture the typing of the generalized constructs with a novel use of qualified types. Our system maintains the metatheoretic properties of the theory of qualified types, including principal types and decidable type inference. Finally, we give a formal basis for our claims of expressiveness, by showing that evaluation respects linearity, and that our language is a conservative extension of existing functional calculi.
@InProceedings{ICFP16p448,
author = {J. Garrett Morris},
title = {The Best of Both Worlds: Linear Functional Programming without Compromise},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {448--461},
doi = {10.1145/2951913.2951925},
year = {2016},
}
Publisher's Version Article Search
Context-Free Session Types
Peter Thiemann and Vasco T. Vasconcelos (University of Freiburg, Germany; University of Lisbon, Portugal)
Session types describe structured communication on heterogeneously
typed channels at a high level.
Their tail-recursive structure imposes a protocol that can be
described by a regular language.
The types of transmitted values are drawn from the underlying
functional language, abstracting from the
details of serializing values of structured data types.
Context-free session types extend session types by allowing nested
protocols that are not restricted to tail recursion. Nested protocols
correspond to deterministic context-free languages. Such protocols are
interesting in their own right, but they are particularly suited to
describe the low-level serialization of tree-structured data in a
type-safe way.
We establish the metatheory of context-free session types, prove that
they properly generalize standard (two-party) session
types, and take first steps towards type checking by showing
that type equivalence is decidable.
@InProceedings{ICFP16p462,
author = {Peter Thiemann and Vasco T. Vasconcelos},
title = {Context-Free Session Types},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {462--475},
doi = {10.1145/2951913.2951926},
year = {2016},
}
Publisher's Version Article Search
Session 12
Combining Effects and Coeffects via Grading
Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, and Tarmo Uustalu (SUNY Buffalo, USA; Kyoto University, Japan; University of Cambridge, UK; University of Kent, UK; Inria, France; Tallinn University of Technology, Estonia)
Effects and coeffects are two general, complementary aspects of program behaviour. They roughly correspond to computations which change the execution context (effects) versus computations which make demands on the context (coeffects). Effectful features include partiality, non-determinism, input-output, state, and exceptions. Coeffectful features include resource demands, variable access, notions of linearity, and data input requirements.
The effectful or coeffectful behaviour of a program can be captured and described via type-based analyses, with fine grained information provided by monoidal effect annotations and semiring coeffects. Various recent work has proposed models for such typed calculi in terms of graded (strong) monads for effects and graded (monoidal) comonads for coeffects.
Effects and coeffects have been studied separately so far, but in practice many computations are both effectful and coeffectful, e.g., possibly throwing exceptions but with resource requirements. To remedy this, we introduce a new general calculus with a combined effect-coeffect system. This can describe both the changes and requirements that a program has on its context, as well as interactions between these effectful and coeffectful features of computation. The effect-coeffect system has a denotational model in terms of effect-graded monads and coeffect-graded comonads where interaction is expressed via the novel concept of graded distributive laws. This graded semantics unifies the syntactic type theory with the denotational model. We show that our calculus can be instantiated to describe in a natural way various different kinds of interaction between a program and its evaluation context.
@InProceedings{ICFP16p476,
author = {Marco Gaboardi and Shin-ya Katsumata and Dominic Orchard and Flavien Breuvart and Tarmo Uustalu},
title = {Combining Effects and Coeffects via Grading},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {476--489},
doi = {10.1145/2951913.2951939},
year = {2016},
}
Publisher's Version Article Search
We show how one can reason about free monads using their universal properties rather than any concrete implementation. We introduce a graphical, two-dimensional calculus tailor-made to accommodate these properties.
@InProceedings{ICFP16p490,
author = {Maciej Piróg and Nicolas Wu},
title = {String Diagrams for Free Monads (Functional Pearl)},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {490--501},
doi = {10.1145/2951913.2951947},
year = {2016},
}
Publisher's Version Article Search