ICFP 2017
Proceedings of the ACM on Programming Languages, Volume 1, Number ICFP
Powered by
Conference Publishing Consulting

Proceedings of the ACM on Programming Languages, Volume 1, Number ICFP, September 3–9, 2017, Oxford, UK

ICFP – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message

Art and Education

Herbarium Racketensis: A Stroll through the Woods (Functional Pearl)
Vincent St-Amour, Daniel Feltey, Spencer P. Florence, Shu-Hung You, and Robert Bruce Findler
(Northwestern University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
Testing and Debugging Functional Reactive Programming
Ivan Perez and Henrik Nilsson
(University of Nottingham, UK)
Publisher's Version Article Search
Lock-Step Simulation Is Child's Play (Experience Report)
Joachim Breitner and Chris Smith
(University of Pennsylvania, USA; Google, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Scaling up Functional Programming Education: Under the Hood of the OCaml MOOC
Benjamin Canou, Roberto Di Cosmo, and Grégoire Henry
(OCamlPro, France; Inria, France; University of Paris Diderot, France)
Publisher's Version Article Search

Functional Programming Techniques

Faster Coroutine Pipelines
Michael Spivey
(University of Oxford, UK)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
A Pretty But Not Greedy Printer (Functional Pearl)
Jean-Philippe Bernardy
(University of Gothenburg, Sweden)
Publisher's Version Article Search
Generic Functional Parallel Algorithms: Scan and FFT
Conal Elliott
(Target, USA)
Publisher's Version Article Search
A Unified Approach to Solving Seven Programming Problems (Functional Pearl)
William E. Byrd, Michael Ballantyne, Gregory Rosenblatt, and Matthew Might
(University of Utah, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable

Applications

Prototyping a Query Compiler using Coq (Experience Report)
Joshua S. Auerbach, Martin Hirzel, Louis Mandel, Avraham Shinnar, and Jérôme Siméon
(IBM Research, USA)
Publisher's Version Article Search Info Artifacts Available Artifacts Functional
A Framework for Adaptive Differential Privacy
Daniel Winograd-Cort, Andreas Haeberlen, Aaron Roth, and Benjamin C. Pierce
(University of Pennsylvania, USA)
Publisher's Version Article Search Info Artifacts Available Artifacts Functional
Symbolic Conditioning of Arrays in Probabilistic Programs
Praveen Narayanan and Chung-chieh Shan
(Indiana University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable

Effects

Abstracting Definitional Interpreters (Functional Pearl)
David Darais, Nicholas Labich, Phúc C. Nguyen, and David Van Horn
(University of Maryland, USA)
Publisher's Version Article Search Info Artifacts Available Artifacts Reusable
On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control
Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar
(Saarland University, Germany; University of Cambridge, UK; University of Oxford, UK; University of Edinburgh, UK; University of Ljubljana, Slovenia)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Imperative Functional Programs That Explain Their Work
Wilmer Ricciotti, Jan Stolarek, Roly Perera, and James Cheney
(University of Edinburgh, UK)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Effect-Driven QuickChecking of Compilers
Jan Midtgaard, Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, and Hanne Riis Nielson
(DTU, Denmark)
Publisher's Version Article Search Artifacts Functional

Low-Level and Systems Programming

Persistence for the Masses: RRB-Vectors in a Systems Language
Juan Pedro Bolívar Puente
Publisher's Version Article Search Info Artifacts Available Artifacts Functional
Verified Low-Level Programming Embedded in F*
Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy
(Microsoft Research, USA; Inria, France; Massachusetts Institute of Technology, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
Verifying Efficient Function Calls in CakeML
Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, and Yong Kiam Tan
(University of Kent, UK; Data61 at CSIRO, Australia; Australian National University, Australia; UNSW, Australia; Chalmers University of Technology, Sweden; Carnegie Mellon University, USA)
Publisher's Version Article Search Artifacts Reusable
Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols
Geoffrey Mainland
(Drexel University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable

Foundations of Higher-Order Programming

Foundations of Strong Call by Need
Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, and Delia Kesner
(LRI, France; University of Paris-Sud, France; CNRS, France; University of Paris-Saclay, France; University of Buenos Aires, Argentina; IRIF, France; University of Paris Diderot, France; CONICET, Argentina; Universidad Nacional de Quilmes, Argentina; Stevens Institute of Technology, USA)
Publisher's Version Article Search
A Relational Logic for Higher-Order Programs
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Pierre-Yves Strub
(IMDEA Software Institute, Spain; University at Buffalo, USA; SUNY, USA; MPI-SWS, Germany; École Polytechnique, France)
Publisher's Version Article Search Artifacts Available Artifacts Functional
How to Prove Your Calculus Is Decidable: Practical Applications of Second-Order Algebraic Theories and Computation
Makoto Hamana
(Gunma University, Japan)
Publisher's Version Article Search
No-Brainer CPS Conversion (Functional Pearl)
Milo Davis, William Meehan, and Olin Shivers
(Northeastern University, USA)
Publisher's Version Article Search

Tools for Verification

Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification
Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind
(Massachusetts Institute of Technology, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
SpaceSearch: A Library for Building and Verifying Solver-Aided Tools
Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, and Zachary Tatlock
(University of Washington, USA; Stanford University, USA)
Publisher's Version Article Search Artifacts Reusable
Local Refinement Typing
Benjamin Cosman and Ranjit Jhala
(University of California at San Diego, USA)
Publisher's Version Article Search Artifacts Reusable

Program Construction

Compiling to Categories
Conal Elliott
(Target, USA)
Publisher's Version Article Search
Visitors Unchained
François Pottier
(Inria, France)
Publisher's Version Article Search
Staged Generic Programming
Jeremy Yallop
(University of Cambridge, UK)
Publisher's Version Article Search

Domain-Specific Languages

Super 8 Languages for Making Movies (Functional Pearl)
Leif Andersen, Stephen Chang, and Matthias Felleisen
(Northeastern University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable

Dependently Typed Programming

A Specification for Dependent Types in Haskell
Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, and Richard A. Eisenberg
(University of Pennsylvania, USA; École Polytechnique, France; University of Campinas, Brazil; Bryn Mawr College, USA)
Publisher's Version Article Search Info Artifacts Available Artifacts Reusable
Parametric Quantifiers for Dependent Type Theory
Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese
(KU Leuven, Belgium; Chalmers University of Technology, Sweden)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
Normalization by Evaluation for Sized Dependent Types
Andreas Abel, Andrea Vezzosi, and Theo Winterhalter
(University of Gothenburg, Sweden; Chalmers University of Technology, Sweden; ENS Paris-Saclay, France)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
A Metaprogramming Framework for Formal Verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura
(Vienna University of Technology, Austria; KIT, Germany; University of Washington, USA; Carnegie Mellon University, USA; Microsoft Research, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable

Contracts and Sessions

Chaperone Contracts for Higher-Order Sessions
Hernán Melgratti and Luca Padovani
(University of Buenos Aires, Argentina; University of Turin, Italy)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
Whip: Higher-Order Contracts for Modern Services
Lucas Waye, Stephen Chong, and Christos Dimoulas
(Harvard University, USA)
Publisher's Version Article Search Info Artifacts Available Artifacts Reusable
Manifest Sharing with Session Types
Stephanie Balzer and Frank Pfenning
(Carnegie Mellon University, USA)
Publisher's Version Article Search
Gradual Session Types
Atsushi Igarashi, Peter Thiemann, Vasco T. Vasconcelos, and Philip Wadler
(Kyoto University, Japan; University of Freiburg, Germany; University of Lisbon, Portugal; University of Edinburgh, UK)
Publisher's Version Article Search Info Artifacts Available Artifacts Reusable

Integrating Static and Dynamic Typing

Theorems for Free for Free: Parametricity, With and Without Types
Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler
(Northeastern University, USA; Indiana University, USA; University of Edinburgh, UK)
Publisher's Version Article Search Artifacts Available Artifacts Functional
On Polymorphic Gradual Typing
Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi
(Kyoto University, Japan; IBM Research, Japan)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Gradual Typing with Union and Intersection Types
Giuseppe Castagna and Victor Lanvin
(CNRS, France; University of Paris Diderot, France; ENS Cachan, France)
Publisher's Version Article Search Artifacts Available

Inference and Analysis

Constrained Type Families
J. Garrett Morris and Richard A. Eisenberg
(University of Edinburgh, UK; Bryn Mawr College, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Automating Sized-Type Inference for Complexity Analysis
Martin Avanzini and Ugo Dal Lago
(University of Innsbruck, Austria; University of Bologna, Italy; Inria, France)
Publisher's Version Article Search
Inferring Scope through Syntactic Sugar
Justin Pombrio, Shriram Krishnamurthi, and Mitchell Wand
(Brown University, USA; Northeastern University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable

proc time: 0.35