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)
Artifacts Reusable
Testing and Debugging Functional Reactive Programming
Ivan Perez and Henrik Nilsson
(University of Nottingham, UK)
Lock-Step Simulation Is Child's Play (Experience Report)
Joachim Breitner and Chris Smith
(University of Pennsylvania, USA; Google, USA)
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)

Functional Programming Techniques

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

Applications

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

Effects

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

Low-Level and Systems Programming

Persistence for the Masses: RRB-Vectors in a Systems Language
Juan Pedro Bolívar Puente
Info Artifacts Functional
Verified Low-Level Programming Embedded in F*
Jonathan ProtzenkoORCID logo, Jean-Karim Zinzindohoué, Aseem Rastogi ORCID logo, Tahina Ramananandro ORCID logo, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud ORCID logo, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet ORCID logo, and Nikhil Swamy ORCID logo
(Microsoft Research, USA; Inria, France; Massachusetts Institute of Technology, USA)
Artifacts Reusable
Verifying Efficient Function Calls in CakeML
Scott Owens ORCID logo, Michael Norrish ORCID logo, Ramana Kumar, Magnus O. MyreenORCID logo, 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)
Artifacts Reusable
Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols
Geoffrey Mainland
(Drexel University, USA)
Artifacts Reusable

Foundations of Higher-Order Programming

Foundations of Strong Call by Need
Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, and Delia KesnerORCID logo
(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)
A Relational Logic for Higher-Order Programs
Alejandro Aguirre ORCID logo, Gilles Barthe, Marco Gaboardi, Deepak GargORCID logo, and Pierre-Yves Strub ORCID logo
(IMDEA Software Institute, Spain; University at Buffalo, USA; SUNY, USA; MPI-SWS, Germany; École Polytechnique, France)
Artifacts Functional
How to Prove Your Calculus Is Decidable: Practical Applications of Second-Order Algebraic Theories and Computation
Makoto Hamana
(Gunma University, Japan)
No-Brainer CPS Conversion (Functional Pearl)
Milo Davis, William Meehan, and Olin Shivers ORCID logo
(Northeastern University, USA)

Tools for Verification

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

Program Construction

Compiling to Categories
Conal ElliottORCID logo
(Target, USA)
Visitors Unchained
François PottierORCID logo
(Inria, France)
Staged Generic Programming
Jeremy YallopORCID logo
(University of Cambridge, UK)

Domain-Specific Languages

Super 8 Languages for Making Movies (Functional Pearl)
Leif AndersenORCID logo, Stephen Chang, and Matthias Felleisen ORCID logo
(Northeastern University, USA)
Artifacts Reusable

Dependently Typed Programming

A Specification for Dependent Types in Haskell
Stephanie Weirich ORCID logo, 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)
Info Artifacts Reusable
Parametric Quantifiers for Dependent Type Theory
Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese
(KU Leuven, Belgium; Chalmers University of Technology, Sweden)
Artifacts Reusable
Normalization by Evaluation for Sized Dependent Types
Andreas Abel ORCID logo, Andrea Vezzosi, and Theo Winterhalter
(University of Gothenburg, Sweden; Chalmers University of Technology, Sweden; ENS Paris-Saclay, France)
Artifacts Reusable
A Metaprogramming Framework for Formal Verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy AvigadORCID logo, and Leonardo de Moura ORCID logo
(Vienna University of Technology, Austria; KIT, Germany; University of Washington, USA; Carnegie Mellon University, USA; Microsoft Research, USA)
Artifacts Reusable

Contracts and Sessions

Chaperone Contracts for Higher-Order Sessions
Hernán Melgratti and Luca PadovaniORCID logo
(University of Buenos Aires, Argentina; University of Turin, Italy)
Artifacts Reusable
Whip: Higher-Order Contracts for Modern Services
Lucas Waye, Stephen Chong ORCID logo, and Christos Dimoulas
(Harvard University, USA)
Info Artifacts Reusable
Manifest Sharing with Session Types
Stephanie BalzerORCID logo and Frank Pfenning ORCID logo
(Carnegie Mellon University, USA)
Gradual Session Types
Atsushi IgarashiORCID logo, Peter ThiemannORCID logo, Vasco T. Vasconcelos, and Philip Wadler ORCID logo
(Kyoto University, Japan; University of Freiburg, Germany; University of Lisbon, Portugal; University of Edinburgh, UK)
Info Artifacts Reusable

Integrating Static and Dynamic Typing

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

Inference and Analysis

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

proc time: 0.04