ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States
Events (31 results)

HasChor: Functional Choreographic Programming for All (Artifact)

Artifact Evaluation People: Gan Shen, Shun Kashiwa, Lindsey Kuper

… …

HasChor: Functional Choreographic Programming for All (Functional Pearl)

ICFP Papers and Events When: Tue 5 Sep 2023 15:30 - 16:00 People: Gan Shen, Shun Kashiwa, Lindsey Kuper

… …

Modal FRP for all: Functional reactive programming without space leaks in Haskell

ICFP Papers and Events When: Wed 6 Sep 2023 15:00 - 15:30 People: Patrick Bahr

… …

A R4RS Compliant REPL in 8Kb

Scheme When: Sat 9 Sep 2023 14:00 - 14:30 People: Léonard Oest O'Leary

… conformant Scheme implementation of all time.

Authors :
- Léonard Oest …

Aggregating combinatorial biomedical graph ranking results for drug repurposing

DeclMed 2023 When: Sat 9 Sep 2023 16:05 - 16:30 People: Daniel Korn

… identifier with every possible drug, we refer to this data as All-Against-All, for all drugs against all diseases. Our resulting dataset includes 22506 diseases …

Rank-Polymorphism for Shape-Guided Blocking

FHPNC 2023 When: Mon 4 Sep 2023 09:45 - 10:30 People: Artjoms Šinkarovs, Thomas Koopman, Sven-Bodo Scholz

… it to demonstrate that all blocked algorithms can be
naturally derived … indexing, and we also prove that all the
blocked versions compute the same …

A type-theoretic account of quantum computation (Extended Abstract)

TyDe 2023 When: Mon 4 Sep 2023 14:45 - 15:07 People: Takafumi Saikawa, Jacques Garrigue

… We use type-theoretic concepts to describe and prove properties of quantum computations, in particular those denoted by so-called quantum circuits. Our proposal combines several components, which are all represented using dependent …

Invited Talk: Set-theoretic Types for Erlang

Erlang 2023 When: Mon 4 Sep 2023 14:00 - 14:45 People: Albert Schimpf, Stefan Wehr, Annette Bieniusa

… expressing nearly all constructs of its type language and provide means …

Exploring Self-Embedded Knitting Programs with Twine

FARM 2023 When: Fri 8 Sep 2023 11:00 - 11:30 People: Amy Zhu, Adriana Schulz, Zachary Tatlock

… of the reality that all objects must be manufactured, incurring labour and environmental …

Layout Polymorphism: Using static computation to allow efficient polymorphism over variable representations

ML When: Fri 8 Sep 2023 15:00 - 15:30 People: Richard A. Eisenberg

… of garbage.

However, all is not well. Heap-allocated types (along with `int …

Keynote: Perfectly Imperfect: Music, Math and the Keyboard

FARM 2023 When: Fri 8 Sep 2023 19:50 - 20:50 People: Gloria Cheng

… explore some basic mathematic principles that underlie all musical discourse …

The Essence of Reactivity

Haskell 2023 When: Fri 8 Sep 2023 11:30 - 12:00 People: Ivan Perez, Frank Dedden

… Reactive programming, functional reactive programming, event-based programming, stream programming, and temporal logic all share an underlying commonality: values can vary over time. These languages differ in multiple ways, including …

Semantic Encapsulation using Linking Types

TyDe 2023 When: Mon 4 Sep 2023 16:00 - 16:22 People: Daniel Patterson, Andrew Wagner, Amal Ahmed

… Interoperability pervades nearly all mainstream language implementations, as
most systems leverage subcomponents written in different languages. And yet,
such linking can expose a language to foreign behaviors that are internally …

Special Delivery: Programming with Mailbox Types

Artifact Evaluation People: Simon Fowler, Duncan Paul Attard, Franciszek Sowul, Phil Trinder, Simon J. Gay

… includes all of the examples in the paper. …

Explicit Refinement Types

ICFP Papers and Events When: Thu 7 Sep 2023 10:30 - 11:00 People: Jad Elkhaleq Ghalayini, Neel Krishnaswami

… that every erased program has all of the properties demanded by its refined type. All of our proofs are formalised in Lean 4. …

Artifact: Intrinsically Typed Sessions With Callbacks

Artifact Evaluation People: Peter Thiemann

All formalizations of session types rely on linear types for soundness … principle. With our approach, all application programs are intrinsically session typed … obligation for a tiny encapsulated library that can be discharged once and for all

Intrinsically Typed Sessions with Callbacks (Functional Pearl)

ICFP Papers and Events When: Thu 7 Sep 2023 13:30 - 14:00 People: Peter Thiemann

All formalizations of session types rely on linear types for soundness …-of-control design principle. With
our approach, all application programs …
obligation that can be discharged once and for all when the library is built …

Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl)

ICFP Papers and Events When: Thu 7 Sep 2023 14:00 - 14:30 People: Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers

… is so simple,
we are able to give all definitions as part of this paper,
and mechanize all our results using the Iris framework in less than 1000 lines …

Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols

Artifact Evaluation People: Léon Gondelman, Jonas Kastberg Hinrichsen, Mário Pereira, Amin Timany, Lars Birkedal

… (not the implementation). All our results are formalized in the Coq proof … with all the needed dependencies of the project. Both share the same README.md file …

With or Without You: Programming with Effect Exclusion

Artifact Evaluation People: Matthew Lutze, Magnus Madsen, Philipp Schuster, Jonathan Immanuel Brachthäuser

… library with a accompanying program.

These elements are all packaged in a virtual …

As low-level as possible, but no lower

ICFP Keynotes When: Tue 5 Sep 2023 13:30 - 14:30 People: Andreas Rossberg

… document, verified interpreters, and mechanised definitions can all be generated. Key to all this have been collaborations with patient researchers from …

Typing Records, Maps, and Structs

ICFP Papers and Events When: Wed 6 Sep 2023 15:30 - 16:00 People: Giuseppe Castagna

… associate all keys to
values of the same type, they are accessed by providing …

Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification

ICFP Papers and Events When: Wed 6 Sep 2023 10:30 - 11:00 People: Son Ho, Aymeric Fromherz, Jonathan Protzenko

… For all the successes in verifying low-level, efficient, security-critical code,
little has been said or studied about the structure, architecture
and engineering of such large-scale proof developments.

We present the design …

Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification

Artifact Evaluation People: Son Ho, Aymeric Fromherz, Jonathan Protzenko

… For all the successes in verifying low-level, efficient, security-critical code, little has been said or studied about the structure, architecture and engineering of such large-scale proof developments. We present the design …

FP^2: Fully in-Place Functional Programming

Artifact Evaluation People: Anton Lorenzen, Daan Leijen, Wouter Swierstra

… of) the Koka compiler and all examples in the paper can be checked and executed …

Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols

ICFP Papers and Events When: Wed 6 Sep 2023 11:30 - 12:00 People: Léon Gondelman, Jonas Kastberg Hinrichsen, Mário Pereira, Amin Timany, Lars Birkedal

… (not the implementation). All our results are formalized in the Coq proof …

Formal Specification and Testing for Reinforcement Learning

ICFP Papers and Events When: Wed 6 Sep 2023 11:30 - 12:00 People: Mahsa Varshosaz, Mohsen Ghaffari, Einar Broch Johnsen, Andrzej Wąsowski

… agents). More importantly, almost half of all mutants are killed by generic write …

Asynchronous Modal FRP

ICFP Papers and Events When: Wed 6 Sep 2023 15:30 - 16:00 People: Patrick Bahr, Rasmus Ejlers Møgelberg

… Over the past decade, a number of languages for functional reactive
programming (FRP) have been suggested, which use modal types to
ensure properties like causality, productivity and lack of space
leaks. So far, almost all

A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized

ICFP Papers and Events When: Tue 5 Sep 2023 11:30 - 12:00 People: Andreas Abel, Nils Anders Danielsson, Oskar Eriksson

… >open</em> programs, as
long as all variables in the context …

An Agda Formalization of a Graded Dependent Type Theory with a Universe and Erasure

Artifact Evaluation People: Andreas Abel, Nils Anders Danielsson, Oskar Eriksson

… , as long as all variables in the context are erasable, the context is consistent …

Vehicle - A Specification Language for Neural Network Properties

Tutorials When: Fri 8 Sep 2023 09:00 - 10:30Fri 8 Sep 2023 11:00 - 12:30 People: Ekaterina Komendantskaya, Matthew L. Daggitt, Wen Kokke

… Vehicle, a functional (Haskell-based) DSL that allows users to do all of this. We …