ICFP 2021
Sun 22 - Sat 28 August 2021
Events (36 results)

Improvements to GHC's parallel garbage collector

HIW 2021 When: Sun 22 Aug 2021 20:44 - 21:06 People: Douglas Wilson

… collections. This requires synchronisation between all threads in the program, which must which must all be stopped before a collection can begin. This synchronisation imposes a significant cost on the runtime on both GHC and all parallel …

Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques

ML 2021 When: Thu 26 Aug 2021 19:00 - 19:30 People: Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos

… automatically detect all inequivalences, and is able to automatically or semi-automatically prove many equivalences, including all classical Meyer and Sieber …

A metalanguage for multi-phase modularity

ML 2021 When: Thu 26 - Fri 27 Aug 2021 People: Jonathan Sterling, Robert Harper

… Type abstraction, the phase distinction, and computational effects all play an important role in the design and implementation of ML-style module systems. We … as all extant forms of structure sharing. …

Is Functional HPC the Key to Low Carbon Computing? by Sven-Bodo Scholz

FHPNC 2021 When: Sun 22 Aug 2021 22:00 - 23:00

… , the contribution of computing will rise to 14% of all emissions in 2040 already …

Performance: Homotopy

FARM 2021 When: Fri 27 Aug 2021 22:40 - 23:00 People: José Miguél Fernandez

… attack an API which hide all the technical details of the asynchronous …

Computational calculus: bridging reduction and evaluation

HOPE 2021 When: Sun 22 Aug 2021 19:00 - 19:30 People: Claudia Faggian, Giulio Guerrieri, Riccardo Treglia

… ): E = [] | let x:=E in M. We show that, when considering all the monadic rules …

Handler calculus

HOPE 2021 When: Sun 22 Aug 2021 20:30 - 21:00 People: Sam Lindley

… We present handler calculus, a core calculus of effect handlers. Inspired by the Frank programming language, handler calculus does not have primitive functions, just handlers. Functions, products, sums, and inductive types, are all

Adding AD to Scheme by Differentiating the Interpreter

Scheme 2021 When: Fri 27 - Sat 28 Aug 2021 People: Mehrdad Maleki, Barak A. Pearlmutter, Jeffrey Mark Siskind

… ). This machinery needs to be generalized to all objects, including closures …

Computational and Contextual Program Differences: Reasoning About Non-equivalent Effectful Programs in an Higher-Order Scenario

HOPE 2021 When: Sun 22 Aug 2021 17:00 - 17:30 People: Ugo Dal Lago, Francesco Gavazzo

… Semantics is traditionally concerned with program equivalence, in which all pairs of programs which are not equivalent are treated the same, and simply dubbed as incomparable. In recent years, various forms of program metrics have been …

Higher-order Programming with Effects and Handlers — with First-Class Functions

HOPE 2021 When: Sun 22 Aug 2021 16:30 - 17:00 People: Jonathan Immanuel Brachthäuser, Philipp Schuster, Edward Lee, Aleksander Boruch-Gruszecki

… . By assuming that all functions are second class, we can admit natural …

Haskell⁻¹: Automatic Function Inversion in Haskell

Haskell 2021 When: Thu 26 Aug 2021 21:00 - 21:30 People: Finn Teegen, Kai-Oliver Prott, Niels Bunkenburg

… into the language, covering almost all of the Haskell2010 language standard. …

Design with Blocks, Code in Text (Lightning Talk)

Scheme 2021 When: Fri 27 Aug 2021 20:30 - 21:00 People: Junya Nose, Youyou Cong, Hidehiko Masuhara

… through all necessary steps, and would serve as a guide for each intermediate …

Avoiding quadratic GHC core code size

HIW 2021 When: Sun 22 Aug 2021 20:22 - 20:44 People: Edsko de Vries, Andres Löh

… quite in a bit in the details to avoid all O(n^2) pitfalls. For a module …

Keynote: Narratives and Lessons from The Early History of F#

ML 2021 When: Thu 26 Aug 2021 22:00 - 23:00 People: Don Syme

… Functional programming is now a mainstream technique in nearly all programming languages, and F# has been part of this story. I’ll talk a walk through the early history of F#, starting with the origins of strongly-typed functional …

A Multiverse of Glorious Documentation

OCaml 2021 When: Fri 27 Aug 2021 20:50 - 21:10 People: Lucas Pluvinage, Jonathan Ludlam

… , of handling different compiler versions and incompatible libraries are all addressed …

Lightning Talk: QuadBlockQuiz – Supply Chain Edition

Erlang 2021 When: Thu 26 Aug 2021 21:20 - 21:30 People: Duncan Sparrell

… of BEAM/OTP to supply chain security. All the software is opensource …

The Hera Framework for Fault-Tolerant Sensor Fusion with Erlang and GRiSP on an IoT Network

Erlang 2021 When: Fri 27 Aug 2021 02:00 - 02:30 People: Sébastien Kalbusch, Vincent Verpoten, Peter Van Roy

all the computations directly at the sensor-equipped devices themselves …

The Dynamic Haskell Plugin for GHC

HIW 2021 When: Mon 23 Aug 2021 00:14 - 00:36 People: Matthías Páll Gissurarson, Agustín Mista

… to other dynamically typed languages.

All these features combine to make the use …

Generalization is hard, but somebody's got to do it

HIW 2021 When: Sun 22 Aug 2021 23:30 - 23:52 People: Richard A. Eisenberg

… in the case where there is no type signature at all, and also for partial type …

Securing Web-Applications with A Refinement Typed ORM

HIW 2021 When: Mon 23 Aug 2021 03:30 - 03:52 People: Nico Lehmann, Rose Kunkel, Niki Vazou, Nadia Polikarpova, Deian Stefan, Ranjit Jhala

… We present STORM, a new web framework that lets developers build model-view-controller (MVC) applications, with compile-time enforcement of security policies.

With STORM, users specify all security policies in a declarative language …

PLTea

PLTea When: Mon 23 Aug 2021 21:00 - 21:30Tue 24 Aug 2021 09:00 - 09:30

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Sat 28 Aug 2021 03:00 - 03:30

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Fri 27 Aug 2021 03:00 - 03:30

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Mon 23 Aug 2021 03:00 - 03:30

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Tue 24 Aug 2021 18:00 - 18:30Wed 25 Aug 2021 06:00 - 06:30

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Tue 24 Aug 2021 21:00 - 21:30Wed 25 Aug 2021 09:00 - 09:30

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Wed 25 Aug 2021 18:00 - 18:30Thu 26 Aug 2021 06:00 - 06:30

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Wed 25 Aug 2021 21:00 - 21:30Thu 26 Aug 2021 09:00 - 09:30

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Mon 23 Aug 2021 18:00 - 18:30Tue 24 Aug 2021 06:00 - 06:30

… of minutes, or as long as you like. All welcome! …

Calculating Dependently-Typed Compilers (Functional Pearl)

Research Papers When: Tue 24 Aug 2021 07:15 - 07:30Mon 23 Aug 2021 19:15 - 19:30 People: Mitchell Pickard, Graham Hutton

… languages, ensure that all compilation components are type-safe, and make the resulting …

Proof-directed program transformation: A functional account of efficient regular expression matching (JFP Presentation)

Research Papers When: Wed 25 Aug 2021 08:00 - 08:15Tue 24 Aug 2021 20:00 - 20:15 People: Andrzej Filinski

… machine. All steps of the development are supported by self-contained (and machine …

Higher-Order Probabilistic Adversarial Computations: Categorical Semantics and Program Logics

Research Papers When: Wed 25 Aug 2021 04:15 - 04:30Tue 24 Aug 2021 16:15 - 16:30 People: Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato

… coupling-based properties. All logics feature rules
for adversarial computations, and yield guarantees that are valid
for all adversaries that satisfy …

A Theory of Higher-Order Subtyping with Type Intervals

Research Papers When: Wed 25 Aug 2021 07:15 - 07:30Tue 24 Aug 2021 19:15 - 19:30 People: Sandro Stucki, Paolo G. Giarrusso

… and undecidability of subtyping. All our proofs are mechanized in Agda using …

Theorems for Free from Separation Logic Specifications

Research Papers When: Thu 26 Aug 2021 04:45 - 05:00Wed 25 Aug 2021 16:45 - 17:00 People: Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, Nikos Tzevelekos

… module operation implies that the operation is linearizable. All the results …

Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Course (Functional Pearl)

Research Papers When: Thu 26 Aug 2021 07:45 - 08:00Wed 25 Aug 2021 19:45 - 20:00 People: Adam Chlipala

… separation logic), and type checking (session types) – all presented without …

ProbNV: Probabilistic Verification of Network Control Planes

Research Papers When: Wed 25 Aug 2021 04:45 - 05:00Tue 24 Aug 2021 16:45 - 17:00 People: Nick Giannarakis, Alexandra Silva, David Walker

… , such as probabilistic all-failures analysis of medium-sized networks with 100-200 devices. When …