ICFP 2020
as the organisers put it
ICFP 2020 is the 25th ACM SIGPLAN International Conference on Functional Programming. The conference was a virtual event during the dates of August 23-26, 2020 and all activities took place online. The main program featured two keynotes, technical presentations for papers appearing in PACMPL Vol 4: Issue ICFP, as well as an awards session, and a special session of papers recently appearing in the Journal of Functional Programming. The two invited speakers for 2020 were: Evan Czaplicki, covering the Elm programming language and hard lessons learned on driving adoption of new programming la ...
who it's for
programming language researchers, type theorists, formal methods researchers, proof engineers, language designers, compiler engineers, OCaml developers, distributed systems researchers
topics
effect handlers and compilation; polymorphic algebraic effects; concurrent separation logic in F*; temporal logic for distributed components; staged selective parser combinators; OCaml post-link optimisation; linear and affine type systems; stable relations denotational semantics; higher-order demand-driven symbolic evaluation; CRDT composition with semidirect products
| title | author | length |
|---|---|---|
| Stable Relations and Abstract Interpretation of Higher-Order Programs | Benoît Montagu, Thomas P. Jensen | 15m |
Defines a denotational semantics for the untyped call-by-value lambda calculus as stable relations (monotone relations from substitutions to value sets) and… | ||
| Higher-Order Demand-Driven Symbolic Evaluation | Zachary Palmer, Theodore Park, Scott F. Smith, Shiwei Weng | 14m |
Presents DDSE, a demand-driven symbolic evaluator for higher-order functional code that runs backward from a program point; defines a novel DDI interpreter… | ||
| Sparcl: A Language for Partially-Invertible Computation | Kazutaka Matsuda, Meng Wang | 15m |
A new language, SPARCL, implements partially-invertible computation with linear types and proves that composing such pieces yields correct invertibility where… | ||
| SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed ... | Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martínez | 15m |
SteelCore provides a semantics for CSL inside F, deriving Hoare rules from effectful non‑deterministic interleaving; it encodes computations as action trees… | ||
| TLC: Temporal Logic of Distributed Components | Jeremiah Griffin, Mohsen Lesani, Narges Shadab, Xizhe Yin | 15m |
TLC is a temporal program logic that verifies both safety and liveness of layered distributed components and proves soundness against an operational semantics… | ||
| Effect Handlers, Evidently | Ningning Xie, Jonathan Immanuel Brachthäuser, Daniel Hillerström, Philipp Schuster | 15m |
Presents an evidence-passing translation that elaborates polymorphic algebraic effects into polymorphic lambda calculus, with a proof of soundness and… | ||
| Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High... | Bastian Hagedorn, Johannes Lenfers, Thomas Koehler, Xueying Qin, Sergei Gorlatch, Michel Steuwer | 14m |
Functional languages RISE and ELEVATE rewrite high-level data-parallel programs into optimized low-level code, expressing tiling, fusion and loop-permutation… | ||
| Staged Selective Parser Combinators | Jamie Willis, Nicolas Wu, Matthew Pickering | 15m |
Compiler for parser combinators that converts typed combinator trees into a CPS-style instruction machine and partially evaluates it with typed staging… | ||
| Kindly Bent to Free Us | Gabriel Radanne, Hannes Saffrich, Peter Thiemann | 15m |
A new ML extension called Affe enforces linearity and affinity so a database use-after-free example compiles in OCaml but is rejected at compile time here. It… | ||
| Sealing Pointer-Based Optimizations Behind Pure Functions | Daniel Selsam, Simon Hudon, Leonardo de Moura | 15m |
Shows how dependent types seal pointer tricks behind pure interfaces to turn exponential tree traversals into linear-time algorithms, implemented for Lean v4… | ||
| Effects for Efficiency: Asymptotic Speedup with First-Class Control | Daniel Hillerström, Sam Lindley, John Longley | 13m |
Claim: first-class control gives a real asymptotic advantage. The authors implement a generic count with effect handlers that visits each edge of an N-depth… | ||
| Computation Focusing | Nick Rioux, Steve Zdancewic | 13m |
Presents a focused polymorphic call-by-push-value calculus and proves computational completeness: every well-typed term has a βη-equivalent focused… | ||
| Retrofitting Parallelism onto Ocaml | KC Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, Anil Madhavapeddy | 15m |
A mostly-concurrent, non-moving mark-and-sweep GC for multicore OCaml is implemented (major heap based on VCGC, allocator from Streamflow) and extended to… | ||
| Liquid Information Flow Control | Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, Armando Solar-Lezama | 15m |
Claims a new DSL called Lifty domain-specific language that encodes information-flow policies as liquid refinements and enforces them with a TIO-style security… | ||
| A theory of RPC calculi for client–server model | Kwanghoon Choi, Byeong-Mo Chang | 11m |
Extends existing stateless RPC calculi to a stateful calculi family that supports symmetric source-level RPC while implementing asymmetric, trampolined… | ||
| The full-reducing Krivine abstract machine KN simulates pure normal-order reduction i... | Álvaro García Perez, Pablo Nogueira | 11m |
An improved full‑reducing Krivine machine KN is shown to perform the exact same beta reductions, in the same order, as pure normal‑order reduction: a lockstep… | ||
| Local algebraic effect theories | Žiga Lukšič, Matija Pretnar | 11m |
Proposes tracking equational theories inside computation types so code can assume only the equations actually observed, not a single global theory. Claims this… | ||
| Heterogeneous binary random-access lists | Wouter Swierstra | 11m |
Implements heterogeneous binary random-access lists in Agda with the same HList API: nil, cons (via a cons-tree primitive) and lookup that are total and… | ||
| POPLMark reloaded: Mechanizing proofs by logical relations | Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, Kathrin Stark | 11m |
Proposes a benchmark that mechanizes logical-relation proofs by proving strong normalization via Kripke-style logical relations for simply-typed lambda… | ||
| Perturbation confusion in forward automatic differentiation of higher-order functions | Oleksandr Manzyuk, Barak A. Pearlmutter, Alexey Radul, David Rush, Jeffrey Mark Siskind | 11m |
Fielded forward AD systems produce wrong results for derivatives of higher-order functions because tag creation is tied to invoking the derivative operator… | ||
| Elastic Sheet-Defined Functions: Generalising Spreadsheet Functions to Variable-Size ... | Matt McCutchen, Judith W. Borghouts, Andrew D. Gordon, Simon Peyton Jones, Advait Sarkar | 11m |
Automatic algorithm generalises sheet-defined functions to variable-size inputs by inferring length variables, emitting constraints and solving them like type… | ||
| Emerging languages: An alternative approach to teaching programming languages | Saverio Perugini | 14m |
Argues that a programming-languages course centers on emerging languages like Lua, Elixir, Go and Python rather than on abstract principles, and implements a… | ||
| The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Ma... | Lionel Parreaux | 15m |
Proposes Simple-sub, a concrete algorithm that preserves principal types with inclusive subtyping and is implemented as Simple-sub under 500 lines (parser… | ||
| Liquid Resource Types | Tristan Knoth, Di Wang, Adam Reynolds, Nadia Polikarpova, Jan Hoffmann | 15m |
Liquid Resource Types claims an automated refinement-type system that proves precise, value-dependent resource bounds (polynomial, exponential and fine-grained… | ||
| Cosmo: A Concurrent Separation Logic for Multicore Ocaml | Glen Mével, Jacques-Henri Jourdan, François Pottier | 15m |
Cosmo provides a separation logic for Multicore OCaml that exposes the weak memory model yet lets you verify familiar locks: it instantiates Iris and is… | ||
| Composing and Decomposing Op-Based CRDTs with Semidirect Products | Matthew Weidner, Christopher S. Meiklejohn, Heather Miller | 15m |
Construction called the semidirect product composes two op-based CRDTs plus an action function to produce a single CRDT that deterministically resolves… | ||
| A Quick Look at Impredicativity | Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, Dimitrios Vytiniotis | 13m |
A design called Quick Look phase adds a localized instantiation pass to GHC that discovers impredicative instantiations by peeking at arguments and nested… | ||
| A Unified View of Modalities in Type Systems | Andreas Abel, Jean-Philippe Bernardy | 12m |
Proposes a single algebraic structure of modalities embedded in System F that recovers linear, usage-counting, security, sensitivity and belief-style systems… | ||
| Lower Your Guards: A Compositional Pattern-Match Coverage Checker | Sebastian Graf, Simon Peyton Jones, Ryan Scott | 14m |
Pattern-match coverage checking becomes a desugaring to guard trees that reduce all patterns to three constructs, with two simple processors A and U producing… | ||
| Signature restriction for polymorphic algebraic effects | Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi | 15m |
Proposes signature restriction on effect interfaces: require each bound type variable to occur only strictly positively in argument positions and only… | ||
| Denotational Recurrence Extraction for Amortized Analysis | Joseph W. Cutler, Dan Licata, Norman Danner | 15m |
A language-to-language translation extracts recurrences from a credit-annotated source into a cost-bearing simply-typed lambda calculus, using an affine type… | ||
| Separation Logic for Sequential Programs (Functional Pearl) | Arthur Charguéraud | 13m |
A mechanized formalization claims a teachable Separation Logic for sequential programs with all definitions and proofs encoded in Coq formalization and… | ||
| Strong Functional Pearl: Harper's Regular-Expression Matcher in Cedille | Aaron Stump, Chris Jenkins, Stephan Spahn, Colin McDonald | 14m |
Implementation of Harper’s continuation-based regular-expression matcher in Cedille claims static termination on all inputs while using only standard… | ||
| Duplo: A Framework for OCaml Post-Link Optimisation | Nandor Licker, Timothy M. Jones | 15m |
Framework builds a low level SSA IR called LLIR that represents both OCaml and C so optimisations can cross the FFI boundary and the toolchain lowers LLIR… | ||
| Recovering Purity with Comonads and Capabilities | Vikraman Choudhury, Neel Krishnaswami | 14m |
A call-by-value impure lambda calculus is extended with a comonadic safety modality that tags variables as safe or impure and a box comonad that internalizes… | ||
| A General Approach to Define Binders Using Matching Logic | Xiaohong Chen, Grigore Rosu | 15m |
Defines binders by using matching logic’s built‑in exists to form the graph set [X]E and then a constructor to build the binder term, encapsulated as the… | ||
| Parsing with Zippers (Functional Pearl) | Pierce Darragh, Michael D. Adams | 15m |
Generalizes Huet’s zipper to handle CFG features like alternation, sharing, and cycles, suspends traversal state so derivatives resume instead of retraversing… | ||
| Regular Language Type Inference with Term Rewriting | Timothée Haudebourg, Thomas Genet, Thomas P. Jensen | 15m |
Claims fully automatic inference of regular-language types for higher-order, tree-processing programs by modeling semantics as term rewriting and types as tree… | ||
| Compiling Effect Handlers in Capability-Passing Style | Philipp Schuster, Jonathan Immanuel Brachthäuser, Klaus Ostermann | 12m |
A compilation technique translates effect handlers written in capability-passing style into simply-typed lambda calculus using iterated continuation-passing… | ||
| 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 | 14m |
Presents a semantics-first proof that adds guardedness to DOT via a step-indexed logical relation built in Iris, yielding gDOT that models impredicative… | ||
| A dependently typed calculus with pattern matching and erasure inference | Matúš Tejiščák | 14m |
A dependently typed calculus with pattern matching and explicit erasure annotations is presented, with the central claim that erasure commutes with reduction… | ||
| Raising Expectations: Automating Expected Cost Analysis with Types | Di Wang, David M. Kahn, Jan Hoffmann | 15m |
A type-based tool called PRaML automatically infers upper bounds on expected execution cost for probabilistic OCaml-like programs by extending RaML’s AARA… | ||
| Program Sketching with Live Bidirectional Evaluation | Justin Lubin, Nick Collins, Cyrus Omar, Ravi Chugh | 15m |
Smyth implements live bidirectional evaluation to run and unevaluate partial programs, turning assertions into per-hole constraints that are fed to Myth (used… | ||
| Elaboration with First-Class Implicit Function Types | András Kovács | 15m |
Presents an elaboration algorithm that actually inserts implicit lambdas by extending core Martin-Löf type theory with strictly curried function types and… | ||
| Kinds are Calling Conventions | Paul Downen, Zena M. Ariola, Simon Peyton Jones, Richard A. Eisenberg | 15m |
An intermediate language encodes runtime representation, arity and evaluation strategy inside kinds so multi-argument calls compile statically even under… | ||
| nothing matches | ||