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

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

Artifacts Functional

Functional Programming Techniques

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

Artifacts Reusable

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, Avraham Shinnar, and Jérôme Siméon
(IBM Research, USA)

Artifacts Functional

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

Artifacts Functional

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

Artifacts Reusable

Effects

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

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)

Artifacts Functional

Imperative Functional Programs That Explain Their Work
Wilmer Ricciotti, Jan Stolarek, Roly Perera, and James Cheney
(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

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)

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)

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

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

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

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

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

Artifacts Reusable

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

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

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, 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 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

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

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

Artifacts Reusable

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

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

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

Artifacts Functional

Inference and Analysis

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

Artifacts Functional

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

Artifacts Reusable

proc time: 0.04