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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 Functional Article: icfp18main-p121-p (type: Full Paper) doi:10.1145/3236801