1,066 papers · page 2 of 54
Jack Liell-Cock, Sam Staton
Imprecise probability generalizes standard probability theory by replacing a single distribution with a convex set of possible distributions. We show that this generalization requires no change to the standard BDD compilation and weighted model counting pipeline used by discrete …
Vilem-Benjamin Liepelt, Danielle Marshall, Dominic Orchard
Graded types provide a way to augment a type system with fine-grained information, e.g., to track side effects or context dependence and resource use (called coeffects ). Graded types for coeffects have found their way into languages such as Haskell, Idris, and Granule, enabling …
Alexandre Moine, Sam Westrick, Joseph Tassarotti
We present Parcas, a concurrent separation logic for verifying the parallel time complexity of fork-join programs. In order to abstract from the specifics of the machine, time complexity for parallel programs is given in terms of two metrics: the work, measuring the total number …
J. Garrett Morris
We propose yet another approach to type inference with first-class implicit polymorphism, based on the interleaving of an Algorithm ℳ-style constraint-generating elaboration of terms and a solver for the generated constraints. The novelty of our approach is that types include exp…
Keisuke Nakano
This pearl presents the classical Möbius inversion theorem for posets as a calculation method for inverting scan-like cumulative computations. We model a scan function as summation over principal down-sets of a lower-finite poset: local values are accumulated according to the ord…
Emma Nardino, Ludovic Henrio, Gabriel Radanne, Yannick Zakowski
This article extends tail-call optimisation by applying it to asynchronous calls. We first introduce Tail-Modulo-Await , a novel code transformation for asynchronous tail recursive functions that prevents the creation of unnecessary tasks. We then show how to combine Tail-Modulo-…
Zoe Paraskevopoulou
We report on using an agentic coding assistant (Claude Code, powered by Claude Opus 4.6) to mechanize a substantial Rocq correctness proof from scratch, with human guidance but without any human-authored proof code. The proof establishes semantic preservation for the administrati…
Benjamin Peters, Jules Jacobs, Diana Kalinichenko, Liam Stevenson, Aspen Smith, Derek Dreyer, Richard A. Eisenberg
OxCaml extends the OCaml type system with support for safe low-level systems programming via modes . For example, OxCaml's modal portability and contention axes ensure that concurrent OxCaml programs have no data races. In practice, however, mode tracking can reject programs that…
Michael Rainey, Michael H. Borkowski, Michael Vollmer, Chaitanya S. Koparkar, Mikah Kainen, Vidush Singhal
Functional programming languages support non-destructive updates via structural sharing, creating a funda-mental tradeoff in memory representation: pointer-based heaps preserve sharing but degrade layout locality, while serialized heaps prioritize locality at the cost of duplicat…
Takahiro Sanada, Keisuke Hoshino, Kenshin Hirai, Shin-ya Katsumata
We introduce a new programming language and its categorical semantics in order to design and implement neural networks within the framework of algebraic effects and handlers for arrows. Our language enables us to construct neural networks symbolically, in the same manner as algeb…
Albert Schimpf, Annette Bieniusa
Set-theoretic type connectives with their native support for union, intersection, and negation have the potential to capture the idioms of dynamically typed languages like Erlang. We investigate whether this theoretical expressiveness translates into practice: does the resulting …
Manuel Serrano
The Proceedings of the ACM series presents the highest-quality research conducted in diverse areas of computer science, as represented by the ACM Special Interest Groups (SIGs). The Proceedings of the ACM on Programming Languages (PACMPL) focuses on research on all aspects of pro…
April Tune, G. A. Kavvos
We develop a compositional semantics for abstract machines, focusing on CK/CEK machines for call-by-push-value. Taking abstract machines as the primary operational semantics, we introduce bimodels, which give denotations to both programs and stacks, and environment bimodels, whic…
Anthony Vandikas, Kiarash Sotoudeh, Marsha Chechik
Property-based testing (PBT) is a powerful technique for software verification that relies on random input generators and “shrinking” processes to find and minimize counterexamples to executable specifications called properties. While optimizing these generators is crucial for te…
Kazuki Watanabe, Mirai Ikebuchi, Mayuko Kori
Verifying effectful higher-order programs, such as probabilistic programs with unbounded recursion, is a central problem in program verification. Predicate transformer semantics, closely related to continuation-passing style and weakest precondition semantics, has been proposed a…
Guannan Wei, Jun Tan, Dinghong Zhong
Multi-stage programming lets programmers write meta-programs that generate efficient code. Staging is typically realized either as a language primitive with quotations and splices ( e.g. , MetaML and its descendants), or as a library embedded in a host language ( e.g. , Lightweig…
Tim Whiting, Kimball Germane
Effect handlers enable powerful control flow patterns by capturing and resuming continuations, but no control flow analysis exists for programs using them. Applying existing approaches for other delimited control operators would either lose precision through CPS translation or be…
Shushu Wu, Chengxi Yang, Xiwei Wu, Qinxiang Cao
Verifying the functional correctness of real-world code with complex algorithms can be decomposed into two layers: verifying that the concrete code refines an abstract algorithmic description, and proving the correctness of the formal description. However, in practice the two lay…
Yifan Xiao, Shijie Li, Yuhao Ge
Large language models are increasingly deployed as autonomous agents for cloud incident response, yet their direct use admits hallucinated diagnoses, unauthorized actions, irreversible changes, and unauditable decision trails. We present RunbookFX , a typed functional domain-spec…
Junyoung Jang, Antoine Gaulin, Jason Z. S. Hu, Brigitte Pientka
Proof assistants based on type theories have been widely successful from verifying safety-critical software to establishing a new standard of rigour by formalizing mathematics. But these proof assistants and even their type-checking kernels are also complex pieces of software, an…