/icfp2020-papers

ICFP 2020 papers. Crowd-sourced

ICFP 2020

https://icfp20.sigplan.org/track/icfp-2020-papers#event-overview


Similar pages for older ICFP (2012, 2013, 2014, 2015, 2016, 2017, 2018 (open access), 2019), POPL (2013, 2014, 2015, 2016), PLDI 2014.


A General Approach to Define Binders Using Matching Logic
Xiaohong Chen, Grigore Rosu
(pdf)

A Quick Look at Impredicativity
Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, Dimitrios Vytiniotis
(pdf)

A Unified View of Modalities in Type Systems
Andreas Abel, Jean-Philippe Bernardy
(pdf) (extended)

A dependently typed calculus with pattern matching and erasure inference
Matúš Tejiščák

Achieving High-Performance the Functional Way — A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies
Bastian Hagedorn, Johannes Lenfers, Thomas Koehler, Xueying Qin, Sergei Gorlatch, Michel Steuwer

Compiling Effect Handlers in Capability-Passing Style
Philipp Schuster, Jonathan Immanuel Brachthäuser, Klaus Ostermann
(pdf)

Composing and Decomposing Op-Based CRDTs with Semidirect Products
Matthew Weidner, Christopher Meiklejohn, Heather Miller
(arXiv)

Computation Focusing
Nick Rioux, Steve Zdancewic

Cosmo: A Concurrent Separation Logic for Multicore OCaml
Glen Mével, Jacques-Henri Jourdan, François Pottier
(pdf)

Denotational Recurrence Extraction for Amortized Analysis
Joe Cutler, Dan Licata, Norman Danner
(pdf)

Duplo: A Framework for OCaml Post-Link Optimisation
Nandor Licker, Timothy M. Jones

Effect Handlers, Evidently
Ningning Xie, Jonathan Immanuel Brachthäuser, Daniel Hillerström, Philipp Schuster, Daan Leijen
(pdf)

Effects for Efficiency: Asymptotic Speedup with First-Class Control
Daniel Hillerström, Sam Lindley, John Longley
(pdf)

Elaboration with First-Class Implicit Function Types
András Kovács
(pdf)

Higher-Order Demand-Driven Symbolic Evaluation
Zachary Palmer, Theodore Park, Scott F. Smith, Shiwei Weng
(pdf)

Kindly Bent to Free Us
Gabriel Radanne, Hannes Saffrich, Peter Thiemann
(arXiv)

Kinds are Calling Conventions
Paul Downen, Zena M. Ariola, Simon Peyton Jones, Richard A. Eisenberg
(pdf)

Liquid Information Flow Control
Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, Armando Solar-Lezama
(pdf)

Liquid Resource Types
Di Wang, Tristan Knoth, Adam Reynolds, Nadia Polikarpova, Jan Hoffmann
(pdf)

Lower Your Guards
Sebastian Graf, Simon Peyton Jones, Ryan G. Scott
(pdf)

Parsing with Zippers (Functional Pearl)
Pierce Darragh, Michael D. Adams
(artifact)

Program Sketching with Live Bidirectional Evaluation
Justin Lubin, Nick Collins, Cyrus Omar, Ravi Chugh
(arXiv)

Raising Expectations: Automating Expected Cost Analysis with Types
Di Wang, David M. Kahn, Jan Hoffmann

Recovering Purity with Comonads and Capabilities
Vikraman Choudhury, Neel Krishnaswami
(arXiv)

Regular Language Type Inference with Term Rewriting
Timothée Haudebourg, Thomas Genet, Thomas P. Jensen
(pdf)

Retrofitting Parallelism onto OCaml
KC Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, Anil Madhavapeddy
(arXiv)

Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris
Paolo G. Giarrusso, Leo Stefanesco, Amin Timany, Lars Birkedal, Robbert Krebbers
(pdf)

Sealing Pointer-Based Optimizations Behind Pure Functions
Daniel Selsam, Simon Hudon, Leonardo De Moura
(arXiv)

Separation Logic for Sequential Programs
Arthur Charguéraud
(pdf)

Signature restriction for polymorphic algebraic effects
Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi
(arXiv)

Sparcl: A Language for Partially-Invertible Computation
Kazutaka Matsuda, Meng Wang

Stable Relations and Abstract Interpretation of Higher-Order Programs
Benoit Montagu, Thomas P. Jensen

Staged Selective Parser Combinators
Jamie Willis, Nicolas Wu, Matthew Pickering
(pdf)

SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martínez
(pdf)

Strong Functional Pearl: Harper's Regular-Expression Matcher in Cedille
Aaron Stump, Chris Jenkins, Stephan Spahn, Colin McDonald

Temporal Logic of Composable Distributed Components
Jeremiah Griffin, Mohsen Lesani, Narges Shadab, Xizhe Yin
(arXiv)

The Simple Essence of Algebraic Subtyping (Functional Pearl)
Lionel Parreaux
(html)