FUNARCH 2024
who it's for
functional programmers, programming language researchers, formal methods engineers, verification engineers, compiler engineers, data engineers, blockchain developers
topics
bidirectional lenses for serializers; delimited continuations for resumable workflows; Agda-to-Haskell CI integration; Plutus and Plutus Core modeling; QuickCheck state-machine testing; verified interpreter extraction to OCaml; modal state logic with Y3; normalization by evaluation for feature pipelines; moving filters across SQL left joins; intersection types for semantic labels
| title | author | length |
|---|---|---|
| Future of FUNARCH | Michael Sperber | 29m |
FUNARCH debates whether to continue after seeing fewer submissions than last year and a smaller room; current format ties papers to an ACM publication with… | ||
| Bidirectional Data Transformations | Marcus Crestani, Markus Schlegel, Marco Schneider | 45m |
Claim: using lenses as bidirectional transformations eliminates paired DTO functions and yields inverses automatically. Implementation: an industrial Clojure… | ||
| Continuations: what have they ever done for us? | Marc Kaufman, Bogdan Popa | 38m |
Congame is a Racket platform that uses delimited continuations to represent studies as composable tree objects, letting handlers pause, serialize a… | ||
| Applying Continuous Formal Methods to Cardano | James Chapman, Arnaud Bailly, Polina Vinogradova | 46m |
A concrete report of formal-methods engineering applied to a live Cardano node: a team of 11 formal-methods specialists embeds Agda specs and Haskell… | ||
| Design and implementation of a verified interpreter for additive manufacturing programs | Matthew Sottile, Mohit Tekriwal | 45m |
A verified interpreter for RS-274 G‑code is implemented by extracting verified components into OCaml and composing them with handwritten driver code; about 54%… | ||
| F3: A Compiler For Feature Engineering | Weixi Ma, Siyu Wang, Arnaud Venet, Junhua Gu, Subbu Subramanian, Rocky Liu, Yafei Yang, Daniel P. Friedman | 31m |
F3 is a Python DSL and compiler that converts feature pipelines into a canonical semantic form so the system can prove equivalence, move filters safely across… | ||
| nothing matches | ||