ICFP – Journal Issue

Frontmatter

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 Article: icfp17main-main105-p doi:

Lock-Step Simulation Is Child's Play (Experience Report)
Joachim Breitner and Chris Smith
(University of Pennsylvania, USA; Google, USA)

Artifacts Functional Article: icfp17main-main24-p doi:

Functional Programming Techniques

Faster Coroutine Pipelines
Michael Spivey
(University of Oxford, UK)

Artifacts Reusable Article: icfp17main-main14-p doi:

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 Article: icfp17main-main35-p doi:

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)

Artifacts Functional Article: icfp17main-main75-p doi:

A Framework for Adaptive Differential Privacy
Daniel Winograd-Cort, Andreas Haeberlen, Aaron Roth, and Benjamin C. Pierce
(University of Pennsylvania, USA)

Artifacts Functional Article: icfp17main-main109-p doi:

Symbolic Conditioning of Arrays in Probabilistic Programs
Praveen Narayanan and Chung-chieh Shan
(Indiana University, USA)

Artifacts Reusable Article: icfp17main-main100-p doi:

Effects

Abstracting Definitional Interpreters (Functional Pearl)
David Darais, Nicholas Labich, Phúc C. Nguyen, and David Van Horn
(University of Maryland, USA)

Artifacts Reusable Article: icfp17main-main114-p doi:

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)

Artifacts Functional Article: icfp17main-main39-p doi:

Imperative Functional Programs That Explain Their Work
Wilmer Ricciotti, Jan Stolarek, Roly Perera, and James Cheney
(University of Edinburgh, UK)

Artifacts Functional Article: icfp17main-main64-p doi:

Effect-Driven QuickChecking of Compilers
Jan Midtgaard, Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, and Hanne Riis Nielson
(DTU, Denmark)

Artifacts Functional Article: icfp17main-main67-p doi:

Low-Level and Systems Programming

Persistence for the Masses: RRB-Vectors in a Systems Language
Juan Pedro Bolívar Puente

Artifacts Functional Article: icfp17main-main68-p doi:

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)

Artifacts Reusable Article: icfp17main-main96-p doi:

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)

Artifacts Reusable Article: icfp17main-main86-p doi:

Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols
Geoffrey Mainland
(Drexel University, USA)

Artifacts Reusable Article: icfp17main-main107-p doi:

Foundations of Higher-Order Programming

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)

Artifacts Functional Article: icfp17main-main81-p doi:

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)

Artifacts Functional Article: icfp17main-main16-p doi:

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)

Artifacts Reusable Article: icfp17main-main71-p doi:

Local Refinement Typing
Benjamin Cosman and Ranjit Jhala
(University of California at San Diego, USA)

Artifacts Reusable Article: icfp17main-main8-p doi:

Program Construction

Domain-Specific Languages

Super 8 Languages for Making Movies (Functional Pearl)
Leif Andersen, Stephen Chang, and Matthias Felleisen
(Northeastern University, USA)

Artifacts Reusable Article: icfp17main-main93-p doi:

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)

Artifacts Reusable Article: icfp17main-main82-p doi:

Parametric Quantifiers for Dependent Type Theory
Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese
(KU Leuven, Belgium; Chalmers University of Technology, Sweden)

Artifacts Reusable Article: icfp17main-main41-p doi:

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)

Artifacts Reusable Article: icfp17main-main84-p doi:

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)

Artifacts Reusable Article: icfp17main-main19-p doi:

Contracts and Sessions

Chaperone Contracts for Higher-Order Sessions
Hernán Melgratti and Luca Padovani
(University of Buenos Aires, Argentina; University of Turin, Italy)

Artifacts Reusable Article: icfp17main-main54-p doi:

Whip: Higher-Order Contracts for Modern Services
Lucas Waye, Stephen Chong, and Christos Dimoulas
(Harvard University, USA)

Artifacts Reusable Article: icfp17main-main58-p doi:

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)

Artifacts Reusable Article: icfp17main-main76-p doi:

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)

Artifacts Functional Article: icfp17main-main102-p doi:

On Polymorphic Gradual Typing
Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi
(Kyoto University, Japan; IBM Research, Japan)

Artifacts Functional Article: icfp17main-main50-p doi:

Inference and Analysis

Constrained Type Families
J. Garrett Morris and Richard A. Eisenberg
(University of Edinburgh, UK; Bryn Mawr College, USA)

Artifacts Functional Article: icfp17main-main89-p doi:

Inferring Scope through Syntactic Sugar
Justin Pombrio, Shriram Krishnamurthi, and Mitchell Wand
(Brown University, USA; Northeastern University, USA)

Artifacts Reusable Article: icfp17main-main45-p doi:

proc time: 0.05