ICFP 2018
Proceedings of the ACM on Programming Languages, Volume 2, Number ICFP

Title Page

Article: icfp18foreword-fm000-p (type: Frontmatter) doi:

Versatile Event Correlation with Algebraic Effects
Oliver Bračevac, Nada Amin, Guido Salvaneschi, Sebastian Erdweg, Patrick Eugster, and Mira Mezini
(TU Darmstadt, Germany; University of Cambridge, UK; Delft University of Technology, Netherlands; University of Lugano, Switzerland; Purdue University, USA)

Article: icfp18main-p5-p (type: Full Paper) doi:

Parametric Polymorphism and Operational Improvement
Jennifer Hackett and Graham Hutton
(University of Nottingham, UK)

Publisher's Version Article: icfp18main-p12-p (type: Full Paper) doi:10.1145/3236763

Handling Delimited Continuations with Dependent Types
Youyou Cong and Kenichi Asai
(Ochanomizu University, Japan)

Publisher's Version Article: icfp18main-p13-p (type: Full Paper) doi:10.1145/3236764

The Simple Essence of Automatic Differentiation
Conal Elliott
(Target, USA)

Publisher's Version Article: icfp18main-p18-p (type: Full Paper) doi:10.1145/3236765

A Spectrum of Type Soundness and Performance
Ben Greenman and Matthias Felleisen
(Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p21-p (type: Full Paper) doi:10.1145/3236766

Compositional Soundness Proofs of Abstract Interpreters
Sven Keidel, Casper Bach Poulsen, and Sebastian Erdweg
(Delft University of Technology, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p23-p (type: Full Paper) doi:10.1145/3236767

Graduality from Embedding-Projection Pairs
Max S. New and Amal Ahmed
(Northeastern University, USA; Inria, France)

Publisher's Version Article: icfp18main-p26-p (type: Full Paper) doi:10.1145/3236768

Incremental Relational Lenses
Rudi Horn, Roly Perera, and James Cheney
(University of Edinburgh, UK; University of Glasgow, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p31-p (type: Full Paper) doi:10.1145/3236769

Elaborating Dependent (Co)pattern Matching
Jesper Cockx and Andreas Abel
(Chalmers University of Technology, Sweden; University of Gothenburg, Sweden)

Publisher's Version Article: icfp18main-p34-p (type: Full Paper) doi:10.1145/3236770

Capturing the Future by Replaying the Past (Functional Pearl)
James Koppel, Gabriel Scherer, and Armando Solar-Lezama
(Massachusetts Institute of Technology, USA; Inria, France)

Publisher's Version Artifacts Functional Article: icfp18main-p36-p (type: Full Paper) doi:10.1145/3236771

MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer
(Delft University of Technology, Netherlands; LRI, France; University of Paris-Sud, France; CNRS, France; University of Paris-Saclay, France; MPI-SWS, Germany; Carnegie Mellon University, USA; imec-Distrinet, Belgium; KU Leuven, Belgium; Inria, France; University of Strasbourg, France; ICube, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p41-p (type: Full Paper) doi:10.1145/3236772

Mtac2: Typed Tactics for Backward Reasoning in Coq
Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, and Derek Dreyer
(MPI-SWS, Germany; Universidad Nacional de Córdoba, Argentina; CONICET, Argentina; Delft University of Technology, Netherlands; IRIF, France; CNRS, France; University of Paris Diderot, France; Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p45-p (type: Full Paper) doi:10.1145/3236773

Build Systems à la Carte
Andrey Mokhov, Neil Mitchell, and Simon Peyton Jones
(Newcastle University, UK; Digital Asset, UK; Microsoft Research, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p46-p (type: Full Paper) doi:10.1145/3236774

Synthesizing Quotient Lenses
Solomon Maina, Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Tufts University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p47-p (type: Full Paper) doi:10.1145/3236775

Finitary Polymorphism for Optimizing Type-Directed Compilation
Atsushi Ohori, Katsuhiro Ueno, and Hisayuki Mima
(Tohoku University, Japan)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p50-p (type: Full Paper) doi:10.1145/3236776

Teaching How to Program using Automated Assessment and Functional Glossy Games (Experience Report)
José Bacelar Almeida, Alcino Cunha, Nuno Macedo, Hugo Pacheco, and José Proença
(University of Minho, Portugal; INESC TEC, Portugal)

Publisher's Version Article: icfp18main-p52-p (type: Full Paper) doi:10.1145/3236777

Functional Programming for Modular Bayesian Inference
Adam Ścibior, Ohad Kammar, and Zoubin Ghahramani
(University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; Uber AI Labs, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p53-p (type: Full Paper) doi:10.1145/3236778

What You Needa Know about Yoneda: Profunctor Optics and the Yoneda Lemma (Functional Pearl)
Guillaume Boisseau and Jeremy Gibbons
(University of Oxford, UK)

Publisher's Version Article: icfp18main-p54-p (type: Full Paper) doi:10.1145/3236779

Generic Deriving of Generic Traversals
Csongor Kiss, Matthew Pickering, and Nicolas Wu
(Imperial College London, UK; University of Bristol, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p55-p (type: Full Paper) doi:10.1145/3236780

Relational Algebra by Way of Adjunctions
Jeremy Gibbons, Fritz Henglein, Ralf Hinze, and Nicolas Wu
(University of Oxford, UK; University of Copenhagen, Denmark; University of Kaiserslautern, Germany; University of Bristol, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p56-p (type: Full Paper) doi:10.1145/3236781

Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion
Mitchell Wand, Ryan Culpepper, Theophilos Giannakopoulos, and Andrew Cobb
(Northeastern University, USA; Czech Technical University, Czechia; BAE Systems, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p60-p (type: Full Paper) doi:10.1145/3236782

Strict and Lazy Semantics for Effects: Layering Monads and Comonads
Andrew K. Hirsch and Ross Tate
(Cornell University, USA)

Publisher's Version Article: icfp18main-p63-p (type: Full Paper) doi:10.1145/3236783

Ready, Set, Verify! Applying hs-to-coq to Real-World Haskell Code (Experience Report)
Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, and Stephanie Weirich
(University of Pennsylvania, USA; UNSW, Australia; BAE Systems, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p71-p (type: Full Paper) doi:10.1145/3236784

A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna
(Radboud University Nijmegen, Netherlands; University of Strathclyde, UK; University of Edinburgh, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p75-p (type: Full Paper) doi:10.1145/3236785

Parallel Complexity Analysis with Temporal Session Types
Ankush Das, Jan Hoffmann, and Frank Pfenning
(Carnegie Mellon University, USA)

Publisher's Version Article: icfp18main-p79-p (type: Full Paper) doi:10.1145/3236786

Equivalences for Free: Univalent Parametricity for Effective Transport
Nicolas Tabareau, Éric Tanter, and Matthieu Sozeau
(Inria, France; University of Chile, Chile; IRIF, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p81-p (type: Full Paper) doi:10.1145/3236787

Prototyping a Functional Language using Higher-Order Logic Programming: A Functional Pearl on Learning the Ways of λProlog/Makam
Antonis Stampoulis and Adam Chlipala
(Originate, USA; Massachusetts Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p88-p (type: Full Paper) doi:10.1145/3236788

Tight Typings and Split Bounds
Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner
(Inria, France; École Polytechnique, France; CNRS, France; University of Paris Diderot, France)

Publisher's Version Article: icfp18main-p89-p (type: Full Paper) doi:10.1145/3236789

Competitive Parallelism: Getting Your Priorities Right
Stefan K. Muller, Umut A. Acar, and Robert Harper
(Carnegie Mellon University, USA; Inria, France)

Publisher's Version Artifacts Functional Article: icfp18main-p91-p (type: Full Paper) doi:10.1145/3236790

Fault Tolerant Functional Reactive Programming (Functional Pearl)
Ivan Perez
(National Institute of Aerospace, USA)

Publisher's Version Article: icfp18main-p93-p (type: Full Paper) doi:10.1145/3236791

Static Interpretation of Higher-Order Modules in Futhark: Functional GPU Programming in the Large
Martin Elsman, Troels Henriksen, Danil Annenkov, and Cosmin E. Oancea
(University of Copenhagen, Denmark; Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p94-p (type: Full Paper) doi:10.1145/3236792

Casts and Costs: Harmonizing Safety and Performance in Gradual Typing
John Peter Campora, Sheng Chen, and Eric Walkingshaw
(University of Louisiana at Lafayette, USA; Oregon State University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p101-p (type: Full Paper) doi:10.1145/3236793

Functional Programming for Compiling and Decompiling Computer-Aided Design
Chandrakana Nandi, James R. Wilcox, Pavel Panchekha, Taylor Blau, Dan Grossman, and Zachary Tatlock
(University of Washington, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p103-p (type: Full Paper) doi:10.1145/3236794

Partially-Static Data as Free Extension of Algebras
Jeremy Yallop, Tamara von Glehn, and Ohad Kammar
(University of Cambridge, UK; University of Oxford, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p104-p (type: Full Paper) doi:10.1145/3236795

What’s the Difference? A Functional Pearl on Subtracting Bijections
Brent A. Yorgey and Kenneth Foner
(Hendrix College, USA; University of Pennsylvania, USA)

Publisher's Version Article: icfp18main-p107-p (type: Full Paper) doi:10.1145/3236796

Keep Your Laziness in Check
Kenneth Foner, Hengchu Zhang, and Leonidas Lampropoulos
(University of Pennsylvania, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p108-p (type: Full Paper) doi:10.1145/3236797

Merlin: A Language Server for OCaml (Experience Report)
Frédéric Bour, Thomas Refis, and Gabriel Scherer
(Facebook, France; Jane Street, UK; Inria, France)

Publisher's Version Article: icfp18main-p116-p (type: Full Paper) doi:10.1145/3236798

Generic Zero-Cost Reuse for Dependent Types
Larry Diehl, Denis Firsov, and Aaron Stump
(University of Iowa, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p117-p (type: Full Paper) doi:10.1145/3236799

Refunctionalization of Abstract Abstract Machines: Bridging the Gap between Abstract Abstract Machines and Abstract Definitional Interpreters (Functional Pearl)
Guannan Wei, James Decker, and Tiark Rompf
(Purdue University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p119-p (type: Full Paper) doi:10.1145/3236800

Reasonably Programmable Literal Notation
Cyrus Omar and Jonathan Aldrich
(University of Chicago, USA; Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp18main-p121-p (type: Full Paper) doi:10.1145/3236801