Search events for 'all'
Requirements are All You Need
ICFP Papers and Events When: Tue 3 Sep 2024 09:00 - 10:00 People: Andrew D. Gordon
… …
A Teaching Language for Specification
Scheme 2024 When: Sat 7 Sep 2024 11:00 - 11:30 People: Cameron Moy
… to provide a smooth path from informal specifications all the way to statically …
Typed, Concise, Nanopass (pick 3) (Extended Abstract)
TyDe 2024 When: Fri 6 Sep 2024 16:00 - 16:22 People: Lawrence Chonavel
… Writing maintainable compilers is hard. You might want a typed compiler. You want a nanopass compiler. Your might want a concise compiler. But you can’t have all 3 at once – until you read this paper! …
Bidirectional Data Transformations
FUNARCH 2024 When: Fri 6 Sep 2024 16:00 - 16:45 People: Marcus Crestani, Markus Schlegel, Marco Schneider
… several data structures and formats all the time. Authoring these translations …
Tail Modulo Async/Await
FProPer 2024 When: Fri 6 Sep 2024 11:00 - 11:45 People: Vivien GACHET, Gabriel Radanne, Ludovic Henrio
… programming languages and are available in virtually all modern production compilers …
Beyond SICP - Design and Implementation of a Notional Machine for Scheme
Scheme 2024 When: Sat 7 Sep 2024 11:30 - 12:00 People: Kyriel Abad, Martin Henz
… of Scheme sufficient for all programs in SICP that we call SICP Scheme. We extend …
Architecting Functional Programs
FUNARCH 2024 When: Fri 6 Sep 2024 09:30 - 10:30 People: Marco Sampellegrini
… is definitely non-technical. Conversations among all parties involved (yes, business …
ChorCaml: Functional Choreographic Programming in OCaml
OCaml Users and Developers Workshop 2024 When: Sat 7 Sep 2024 16:45 - 17:07 People: Rokas Urbonas
… Choreographic programming offers a way of implementing distributed systems with better safety and clarity than traditional approaches. This is achieved by unifying the code of all participants into a single program, and entrusting …
An introduction to synthetic guarded domain theory with applications to probabilistic programming languages
HOPE 2024 When: Mon 2 Sep 2024 09:00 - 10:00 People: Rasmus Ejlers Møgelberg
… is used in all steps of the process: Defining the semantics, reasoning about …
Is this really a refactoring? Automated equivalence checking for Erlang projects
Erlang When: Mon 2 Sep 2024 15:00 - 15:30 People: Bendegúz Seres, Dániel Horpácsi, Simon Thompson
… We present an automated approach to checking whether a change to a repository is a refactoring, implemented in the EquivcheckEr tool. The tool detects the places in which the code has changed, and compares the old and new versions of all …
Amplifying Contextual Distance in Higher-Order Languages, using the Law of Large Numbers
HOPE 2024 When: Mon 2 Sep 2024 11:00 - 11:30 People: Raphaëlle Crubillé, Houssein Mansour
… that in a probabilistic language where all programs terminate with probability …
Light-speed type unification modulo isomorphisms
ML When: Fri 6 Sep 2024 15:00 - 15:30 People: Emmanuel Arrighi, Gabriel Radanne
… are guaranteed to be sound (the type does match) and complete (all …
Fabricating Functional Formalisms for Fun
Haskell 2024 When: Fri 6 Sep 2024 09:05 - 10:15 People: Brent Yorgey
… For almost as long as I can remember, all my best projects—the ones that I’m proudest of, the ones that have been the most fruitful and brought me the most joy—have all centered around building some kind of language. Perhaps I am just …
Project-wide occurrences for OCaml, a progress report
OCaml Users and Developers Workshop 2024 When: Sat 7 Sep 2024 11:22 - 11:45 People: Ulysse Gérard
… This progress report describes the design of the first implementation of project-wide occurrences for OCaml, a feature of editor tooling that allows users to query all the occurrences of a selected value (or type or module), anywhere …
Modeling Erlang Compiler IR as SMT Formulas
Erlang When: Mon 2 Sep 2024 12:00 - 12:30 People: John Högberg
… , and requires sophisticated analysis to safely apply all but the simplest …
Unsafe Impedance: safe languages and safe by design software
Erlang When: Mon 2 Sep 2024 10:00 - 10:30 People: Lee Barney, Adolfo Neto
… In December 2023, security agencies from five countries in North America, Europe, and the south Pacific produced a document encouraging senior executives in all software producing organizations to take responsibility for and oversight …
(Keynote) Environmentally sustainable software and data architectures
Erlang When: Mon 2 Sep 2024 09:05 - 10:00 People: Madeleine Malmsten
… -functional requirement for all software development. - Companies can incorporate …
Same same but different: A Comparative Analysis of Static Type Checkers in Erlang
Erlang When: Mon 2 Sep 2024 11:00 - 11:30 People: Florian Berger, Albert Schimpf, Annette Bieniusa, Stefan Wehr
… cases across all test suites, Dialyzer’s success-typing approach sets it apart …
Towards Type-Directed API Search for Mainstream Languages
TyDe 2024 When: Fri 6 Sep 2024 16:45 - 17:07 People: Marc Etter, Farhad Mehta
… Software developers spend a lot of their time finding and composing pre-existing functions from various libraries. Almost all developers today use general-purpose search engines for this search. Specialized search engines such as *Hoogle …
A Non-allocating Option
OCaml Users and Developers Workshop 2024 When: Sat 7 Sep 2024 09:45 - 10:07 People: Richard A. Eisenberg
… advantage of an all-0, or null, value to denote error conditions, all …
Mica: Automated Differential Testing for OCaml Modules
OCaml Users and Developers Workshop 2024 When: Sat 7 Sep 2024 11:45 - 12:07 People: Ernest Ng, Harrison Goldstein, Benjamin C. Pierce
… Suppose we are given two OCaml modules implementing the same signature. How do we check that they are observationally equivalent—that is, that they behave the same on all inputs? One established technique is to use a property-based …
Mixed Blocks: Storing More Fields Flat
OCaml Users and Developers Workshop 2024 When: Sat 7 Sep 2024 10:07 - 10:30 People: Nicholas Roberts
… from the current OCaml, which supports only uniform blocks: either all …
The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data Structures (Artifact)
Artifact Evaluation People: Yijia Chen, Lionel Parreaux
… a test suite containing all the examples in the paper and all the `nofib …
Abstract Interpreters: A Monadic Approach to Modular Verification
ICFP Papers and Events When: Tue 3 Sep 2024 11:06 - 11:24 People: Sébastien Michelland, Yannick Zakowski, Laure Gonnord
… proven correct once and for all against their concrete counterpart. We … effects.
We formalize all the aforementioned combinators …
CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs
Artifact Evaluation People: Cole Kurashige, Ruyi Ji, Aditya Giridharan, Mark Barbone, Daniel Noor, Shachar Itzhaky, Ranjit Jhala, Nadia Polikarpova
… Haskell*.
We include with our tool all of the datasets necessary to run … in the optimization dataset, will run to timeout. We estimate running all …
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
Artifact Evaluation People: Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
… of our program. By representing error bounds as a resource, we recover all … algorithms. All of our results have been mechanized using Coq, Iris …
Beyond Trees: Calculating Graph-Based Compilers
Artifact Evaluation People: Patrick Bahr, Graham Hutton
… . This artifact consists of an Agda formalisation of all calculations in the paper. …
Normalization by evaluation for modal dependent type theory
JFP First Papers When: Tue 3 Sep 2024 13:30 - 13:48 People: Jason Z.S. Hu, Junyoung Jang, Brigitte Pientka
… to all four aforementioned modal systems without modification. This NbE proof …
Refinement Composition Logic
ICFP Papers and Events When: Wed 4 Sep 2024 14:24 - 14:42 People: Youngju Song, Dongjae Lee
… refinements. All our results are formalized in Coq. …
Call-by-Unboxed-Value
ICFP Papers and Events When: Tue 3 Sep 2024 15:48 - 16:06 People: Paul Downen
… , while nonetheless preserving types all the way to the machine. …
Contextual Typing
Artifact Evaluation People: Xu Xue, Bruno C. d. S. Oliveira
… an all (checking mode) or nothing (inference mode) approach. QTASs enable …, records and overloading. All the metatheory is formalized in the Agda theorem …
Snapshottable Stores
ICFP Papers and Events When: Wed 4 Sep 2024 13:48 - 14:06 People: Clément Allain, Basile Clément, Alexandre Moine, Gabriel Scherer
… an arbitrary set of references (of any type) and restore all of them at once … for arbitrary data structures, by simply replacing all mutable references …
Contextual Typing
ICFP Papers and Events When: Thu 5 Sep 2024 10:48 - 11:06 People: Xu Xue, Bruno C. d. S. Oliveira
… generalizes modes in traditional bidirectional typing, which can only model an all … and overloading. All the metatheory is formalized in the Agda theorem prover. …
Closure-Free Functional Programming in a Two-Level Type Theory
Artifact Evaluation People: András Kovács
… by staging and we can reuse almost all definitions from the existing Haskell ecosystem …
Dependent Ghosts Have a Reflection for Free
Artifact Evaluation People: Théo Winterhalter
… gets rid of all ghost data and proofs, a step which may be used as a first step …
Level-p-complexity of Boolean functions using thinning, memoization, and polynomials
JFP First Papers When: Wed 4 Sep 2024 15:48 - 16:06 People: Julia Jansson, Patrik Jansson
… expected cost of all possible decision trees — which directly translates …
Parallel Algebraic Effect Handlers
ICFP Papers and Events When: Tue 3 Sep 2024 10:48 - 11:06 People: Ningning Xie, Daniel D. Johnson, Dougal Maclaurin, Adam Paszke
… . All examples presented can be encoded in the Haskell implementation. We believe …
Dependent Ghosts Have a Reflection for Free
ICFP Papers and Events When: Tue 3 Sep 2024 14:24 - 14:42 People: Théo Winterhalter
… erasure procedure which gets rid of all ghost data and proofs, a step which may …
Closure-Free Functional Programming in a Two-Level Type Theory
ICFP Papers and Events When: Tue 3 Sep 2024 13:48 - 14:06 People: András Kovács
… by staging and we can reuse almost all definitions from the existing Haskell ecosystem …
Almost-Sure Termination by Guarded Refinement
Artifact Evaluation People: Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
… -Watson trees that uses higher-order store. All the results in this paper have been …
Abstracting Effect Systems for Algebraic Effect Handlers
ICFP Papers and Events When: Tue 3 Sep 2024 10:30 - 10:48 People: Takuma Yoshioka, Taro Sekiyama, Atsushi Igarashi
… Many effect systems for algebraic effect handlers are designed to guarantee that all invoked effects are handled adequately. However, respective researchers have developed their own effect systems that differ in how to represent …
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
ICFP Papers and Events When: Wed 4 Sep 2024 13:30 - 13:48 People: Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
… and almost-sure termination of
rejection sampling algorithms. All of our …
Almost-Sure Termination by Guarded Refinement
ICFP Papers and Events When: Wed 4 Sep 2024 14:06 - 14:24 People: Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
… higher-order store. All the results have been mechanized in the Coq proof …
CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs
ICFP Papers and Events When: Wed 4 Sep 2024 16:06 - 16:24 People: Cole Kurashige, Ruyi Ji, Aditya Giridharan, Mark Barbone, Daniel Noor, Shachar Itzhaky, Ranjit Jhala, Nadia Polikarpova
… and compactly represent
the space of <em>all</em> goal …
Double-Ended Bit-Stealing for Algebraic Data Types
ICFP Papers and Events When: Thu 5 Sep 2024 14:06 - 14:24 People: Martin Elsman
… the representation supports that all values can be held uniformly in one machine word, possibly …