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 …

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 …

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 …

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

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 …

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 …

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 …