Nadia Polikarpova, Deian Stefan, Jean Yang and

Shachar Itzhaky, Travis Hance, Armando Solar-Lezama

Keywords Abstract Paper

program synthesis, information flow control, liquid types

Arthur Charguéraud

Keywords Abstract Paper

Program verification, Separation Logic, Coq

Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi

Keywords Abstract Paper

polymorphic effects, polymorphic type assignment, algebraic effects and handlers

Wouter Swierstra

Keywords Abstract Paper

Justin Lubin, Nick Collins, Cyrus Omar, Ravi Chugh

Keywords Abstract Paper

Program Synthesis, Examples, Sketches, Bidirectional Evaluation

Ningning Xie, Jonathan Immanuel Brachthäuser, Daniel Hillerström and

Philipp Schuster, Daan Leijen

Keywords Abstract Paper

Handlers, Evidence Passing Translation, Algebraic Effects

Daniel Hillerström, Sam Lindley, John Longley

Keywords Abstract Paper

effect handlers, generic search, asymptotic complexity analysis

Kazutaka Matsuda, Meng Wang

Keywords Abstract Paper

linear types, reversible computation

Matthew Weidner, Christopher Meiklejohn, Heather Miller

Keywords Abstract Paper

Operational Transformation, CRDTs, Eventual Consistency

Pierce Darragh, Michael D. Adams

Keywords Abstract Paper

Zippers, Parsing with Derivatives, Parsing, Derivatives

Jeremiah Griffin, Mohsen Lesani, Narges Shadab, Xizhe Yin

Keywords Abstract Paper

Program Logic, Composition, Operational Semantics, Temporal Logic, Distributed Protocols

Daniel Selsam, Simon Hudon, Leonardo De Moura

Keywords Abstract Paper

functional programming, interactive theorem proving, Lean

Tristan Knoth, Di Wang, Adam Reynolds and

Nadia Polikarpova, Jan Hoffmann

Keywords Abstract Paper

Automated amortized resource analysis, Refinement types

Zachary Palmer, Theodore Park, Scott F. Smith, Shiwei Weng

Keywords Abstract Paper

Symbolic Execution, Demand-Driven Execution, Test Generation

Nick Rioux, Steve Zdancewic

Keywords Abstract Paper

full abstraction, type systems, compiler verification, program equivalence, focusing

Di Wang, David M. Kahn, Jan Hoffmann

Keywords Abstract Paper

resource-aware type system, expected execution cost, analysis of probabilistic programs

Jamie Willis, Nicolas Wu, Matthew Pickering

Keywords Abstract Paper

parsers, meta-programming, combinators

Kwanghoon Choi, Byeong-Mo Chang

Keywords Abstract Paper

Sebastian Graf, Simon Peyton Jones, Ryan Scott

Keywords Abstract Paper

guards, Haskell, pattern matching, strictness

Paolo G. Giarrusso, Leo Stefanesco, Amin Timany and

Lars Birkedal, Robbert Krebbers

Keywords Abstract Paper

type soundness, data abstraction, DOT, step-indexing, Coq, Scala, logical relations, Iris

Aaron Stump, Chris Jenkins, Stephan Spahn, Colin McDonald

Keywords Abstract Paper

recursion schemes, strong functional programming, programming with continuations, regular-expression matcher

Nandor Licker, Timothy M. Jones

Keywords Abstract Paper

OCaml, LLVM, C, post-link, optimisation, inlining

Xiaohong Chen, Grigore Roşu

Keywords Abstract Paper

completeness, matching logic, binders, conservative extension

Andreas Abel, Jean-Philippe Bernardy

Keywords Abstract Paper

subtyping, linear types, modal logic

Paul Downen, Zena M. Ariola, Simon Peyton Jones, Richard A. Eisenberg

Keywords Abstract Paper

representation, type systems, arity, levity, polymorphism

Glen Mével, Jacques-Henri Jourdan, François Pottier

Keywords Abstract Paper

program verification, weak memory, concurrency, separation logic

Joseph W. Cutler, Dan Licata, Norman Danner

Keywords Abstract Paper

amortized analysis, recurrence extraction, denotational semantics, resource analysis, higher order recurrences, cost semantics

Matt McCutchen, Judith Borghouts, Andrew D. Gordon and

Simon Peyton Jones, Advait Sarkar

Keywords Abstract Paper

Benoît Montagu, Thomas P. Jensen

Keywords Abstract Paper

correlations, static analysis, abstract interpretation, lambda-calculus

Philipp Schuster, Jonathan Immanuel Brachthäuser, Klaus Ostermann

Keywords Abstract Paper

lexically-scoped effect handlers, continuation-passing style, algebraic effects, capability-passing style, continuations, control effects, compilation

Timothée Haudebourg, Thomas Genet, Thomas P. Jensen

Keywords Abstract Paper

Higher-Order, Program Verification, Type Inference, Functional Languages, Regular Languages, Term Rewriting

Vikraman Choudhury, Neel Krishnaswami

Keywords Abstract Paper

capabilities, modal type theory, effects, categorical semantics, comonads

Gabriel Radanne, Hannes Saffrich, Peter Thiemann

Keywords Abstract Paper

Ownership, Functional programming, Type inference, Linear types

Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz and

Denis Merigoux, Danel Ahman, Guido Martínez

Keywords Abstract Paper

Separation Logic, Program Proofs, Concurrency

Andreas Abel, Guillaume Allais, Aliya Hameer and

Brigitte Pientka, Alberto Momigliano, Steven Schäfer, Kathrin Stark

Keywords Abstract Paper

KC Sivaramakrishnan, Stephen Dolan, Leo White and

Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, Anil Madhavapeddy

Keywords Abstract Paper

backwards compatibility, concurrent garbage collection

Oleksandr Manzyuk, Barak A. Pearlmutter, Alexey Radul and

David Rush, Jeffrey Mark Siskind

Keywords Abstract Paper

András Kovács

Keywords Abstract Paper

type theory, type inference, impredicative polymorphism, elaboration

Lionel Parreaux

Keywords Abstract Paper

subtyping, principal types, type inference

Álvaro García Perez, Pablo Nogueira

Keywords Abstract Paper