ICFP – Journal Issue

Artifacts Functional Article: icfp20main-p18-p doi:10.1145/3408974

Compiling Effect Handlers in Capability-Passing Style
Philipp Schuster, Jonathan Immanuel Brachthäuser, and Klaus Ostermann
(University of Tübingen, Germany)

Publisher's Version Article: icfp20main-p43-p doi:10.1145/3408975

Composing and Decomposing Op-Based CRDTs with Semidirect Products
Matthew Weidner, Heather Miller, and Christopher Meiklejohn
(Carnegie Mellon University, USA)

Publisher's Version Article: icfp20main-p87-p doi:10.1145/3408976

Computation Focusing
Nick Rioux and Steve Zdancewic
(University of Pennsylvania, USA)

Publisher's Version Article: icfp20main-p75-p doi:10.1145/3408977

Cosmo: A Concurrent Separation Logic for Multicore OCaml
Glen Mével, Jacques-Henri Jourdan, and François Pottier
(Inria, France; University of Paris-Saclay, France; CNRS, France; LRI, France)

Artifacts Functional Article: icfp20main-p48-p doi:10.1145/3408978

Denotational Recurrence Extraction for Amortized Analysis
Joseph W. Cutler, Daniel R. Licata, and Norman Danner
(Wesleyan University, USA)

Publisher's Version Article: icfp20main-p7-p doi:10.1145/3408979

Duplo: A Framework for OCaml Post-Link Optimisation
Nandor Licker and Timothy M. Jones
(University of Cambridge, UK)

Artifacts Functional Article: icfp20main-p13-p doi:10.1145/3408980

Effect Handlers, Evidently
Ningning Xie, Jonathan Immanuel Brachthäuser, Daniel Hillerström, Philipp Schuster, and Daan Leijen
(Microsoft Research, USA; University of Tübingen, Germany; University of Edinburgh, UK)

Publisher's Version Article: icfp20main-p62-p doi:10.1145/3408981

Effects for Efficiency: Asymptotic Speedup with First-Class Control
Daniel Hillerström, Sam Lindley, and John Longley
(University of Edinburgh, UK; Imperial College London, UK; Heriot-Watt University, UK)

Artifacts Functional Article: icfp20main-p71-p doi:10.1145/3408982

Elaboration with First-Class Implicit Function Types
András Kovács
(Eötvös Loránd University, Hungary)

Artifacts Functional Article: icfp20main-p21-p doi:10.1145/3408983

Higher-Order Demand-Driven Symbolic Evaluation
Zachary Palmer, Theodore Park, Scott Smith, and Shiwei Weng
(Swarthmore College, USA; Johns Hopkins University, USA)

Artifacts Functional Article: icfp20main-p69-p doi:10.1145/3408984

Kindly Bent to Free Us
Gabriel Radanne, Hannes Saffrich, and Peter Thiemann
(Inria, France; University of Freiburg, Germany)

Artifacts Functional Article: icfp20main-p74-p doi:10.1145/3408985

Kinds Are Calling Conventions
Paul Downen, Zena M. Ariola, Simon Peyton Jones, and Richard A. Eisenberg
(University of Oregon, USA; Microsoft Research, UK; Bryn Mawr College, USA; Tweag I/O, USA)

Publisher's Version Article: icfp20main-p93-p doi:10.1145/3408986

Liquid Information Flow Control
Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, and Armando Solar-Lezama
(University of California at San Diego, USA; Carnegie Mellon University, USA; Technion, Israel; Massachusetts Institute of Technology, USA)

Artifacts Functional Article: icfp20main-p86-p doi:10.1145/3408987

Liquid Resource Types
Tristan Knoth, Di Wang, Adam Reynolds, Jan Hoffmann, and Nadia Polikarpova
(University of California at San Diego, USA; Carnegie Mellon University, USA)

Artifacts Functional Article: icfp20main-p83-p doi:10.1145/3408988

Lower Your Guards: A Compositional Pattern-Match Coverage Checker
Sebastian Graf, Simon Peyton Jones, and Ryan G. Scott
(KIT, Germany; Microsoft Research, UK; Indiana University, USA)

Artifacts Functional Article: icfp20main-p57-p doi:10.1145/3408989

Parsing with Zippers (Functional Pearl)
Pierce Darragh and Michael D. Adams
(University of Utah, USA; University of Michigan, USA)

Artifacts Functional Article: icfp20main-p101-p doi:10.1145/3408990

Program Sketching with Live Bidirectional Evaluation
Justin Lubin, Nick Collins, Cyrus Omar, and Ravi Chugh
(University of Chicago, USA; University of Michigan, USA)

Artifacts Functional Article: icfp20main-p104-p doi:10.1145/3408991

Raising Expectations: Automating Expected Cost Analysis with Types
Di Wang, David M. Kahn, and Jan Hoffmann
(Carnegie Mellon University, USA)

Artifacts Functional Article: icfp20main-p78-p doi:10.1145/3408992

Recovering Purity with Comonads and Capabilities
Vikraman Choudhury and Neel Krishnaswami
(Indiana University, USA; University of Cambridge, UK)

Publisher's Version Article: icfp20main-p73-p doi:10.1145/3408993

Regular Language Type Inference with Term Rewriting
Timothée Haudebourg, Thomas Genet, and Thomas Jensen
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France)

Artifacts Functional Article: icfp20main-p15-p doi:10.1145/3408994

Retrofitting Parallelism onto OCaml
KC Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, and Anil Madhavapeddy
(IIT Madras, India; OCaml Labs, UK; Jane Street, UK; Opsian, UK; University of Cambridge, UK)

Artifacts Functional Article: icfp20main-p65-p doi:10.1145/3408995

Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers
(Delft University of Technology, Netherlands; IRIF, France; University of Paris, France; CNRS, France; Aarhus University, Denmark)

Artifacts Functional Article: icfp20main-p32-p doi:10.1145/3408996

Sealing Pointer-Based Optimizations behind Pure Functions
Daniel Selsam, Simon Hudon, and Leonardo de Moura
(Microsoft Research, USA; Carnegie Mellon University, USA)

Publisher's Version Article: icfp20main-p38-p doi:10.1145/3408997

Separation Logic for Sequential Programs (Functional Pearl)
Arthur Charguéraud
(Inria, France; University of Strasbourg, France; CNRS, France; ICube, France)

Publisher's Version Article: icfp20main-p46-p doi:10.1145/3408998

Signature Restriction for Polymorphic Algebraic Effects
Taro Sekiyama, Takeshi Tsukada, and Atsushi Igarashi
(National Institute of Informatics, Japan; SOKENDAI, Japan; University of Tokyo, Japan; Kyoto University, Japan)

Artifacts Functional Article: icfp20main-p98-p doi:10.1145/3408999

Sparcl: A Language for Partially-Invertible Computation
Kazutaka Matsuda and Meng Wang
(Tohoku University, Japan; University of Bristol, UK)

Artifacts Functional Article: icfp20main-p79-p doi:10.1145/3409000

Stable Relations and Abstract Interpretation of Higher-Order Programs
Benoît Montagu and Thomas Jensen
(Inria, France)

Artifacts Functional Article: icfp20main-p8-p doi:10.1145/3409001

Staged Selective Parser Combinators
Jamie Willis, Nicolas Wu, and Matthew Pickering
(Imperial College London, UK; University of Bristol, UK)

Publisher's Version Article: icfp20main-p63-p doi:10.1145/3409002

SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, and Guido Martínez
(Microsoft Research, USA; Microsoft Research, India; Carnegie Mellon University, USA; Inria, France; University of Ljubljana, Slovenia; CIFASIS-CONICET, Argentina)

Artifacts Functional Article: icfp20main-p102-p doi:10.1145/3409003

Strong Functional Pearl: Harper’s Regular-Expression Matcher in Cedille
Aaron Stump, Christopher Jenkins, Stephan Spahn, and Colin McDonald
(University of Iowa, USA; University of Notre Dame, USA)

Publisher's Version Article: icfp20main-p34-p doi:10.1145/3409004

TLC: Temporal Logic of Distributed Components
Jeremiah Griffin, Mohsen Lesani, Narges Shadab, and Xizhe Yin
(University of California at Riverside, USA)

Publisher's Version Article: icfp20main-p11-p doi:10.1145/3409005

The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl)
Lionel Parreaux
(EPFL, Switzerland)