Search events for 'all'
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 …
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 …
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 …
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 …
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
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 …
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 …
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 …
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 …
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 …