7,482 papers · page 3 of 375
Levy's call-by-push-value (CBPV) is a language that subsumes both call-by-name and call-by-value lambda calculi by syntactically distinguishing values from computations and explicitly specifying execution order. This low-level handling of computation suspension and resumption mak…
Optimistic replication of objects avoids coordination and brings higher responsiveness and availability. However, when clients issue concurrent operations, conflicts naturally arise which can lead the replicated states to diverge or lose integrity. When conflicts occur, existing …
Simulations are widely-used notions of program refinement. This paper discusses and compares several of them, in particular notions of simulation that are both weak and sensitive to divergence. Complex simulation proofs performed in proof assistants, for instance in a verified co…
As quantum computing becomes an emerging reality, designing efficient quantum programming capabilities is becoming more and more important. Particularly, the debugging and validation of quantum programs is of paramount importance, as these programs are by definition hard to test.…
A transient data structure is a combination of an ephemeral data structure, a persistent data structure, and fast conversions between them. We present a transient sequence data structure that supports efficient read and write access at an arbitrary index with worst-case time comp…
Differential privacy (DP) has established itself as one of the standards for ensuring privacy of individual data. However, reasoning about DP is a challenging and error-prone task, hence methods for formal verification and refutation of DP properties have received significant int…
Application profiling is an indispensable technique for many software development tasks, such as code and memory layout optimizations, where optimization decisions are tailored to specific program profiles. Unfortunately, modern application codebases exhibit highly variant behavi…
Boolean-algebraic subtyping (BAS) is a powerful subtyping approach introduced in 2022 as the "secret sauce" enabling backtracking-free principal type inference in the MLstruct research language, a structurally-typed functional programming language with tagged records, tag and rec…
Automatically translating system software from C to Rust is an appealing but challenging problem, as it requires whole-program reasoning to satisfy Rust’s ownership and borrowing discipline. A key enabling step in whole-program translation is interface translation , which produce…
GPU hardware implements a SIMT execution model, where small groups of threads, called subgroups (or warps in CUDA), execute synchronously. Languages expose this through high-performance subgroup-level APIs. However, providing precise subgroup semantics in languages is challenging…
Static analysis has profoundly improved software quality over the past decades, evolving from compiler-integrated optimizations and simple linting to sophisticated analyses for bug detection, security, and program understanding. In contrast, static analysis for hardware remains u…
We introduce semantic reification, a novel paradigm for random program generation that centers on program semantics rather than syntax. Our key insight is to reformulate random program generation to capture two types of program semantics: (1) compile-time semantics (what a progra…
There exist many techniques for automatically deriving parametric resource (or cost) bounds by analyzing the source code of a program. These techniques work effectively for a large class of programs and language features. However, non-local transfer of control as needed for excep…
Term rewriting systems are a common tool in automated reasoning and semantics of programming languages, and many practical applications require these systems to be convergent. While automated tools and theory exist to establish convergence, this paper is concerned with a practica…
We introduce a type system that provides strong types for exception tracking in ML-style languages. Our type system employs a rich notion of row polymorphism and subtyping to ensure backwards compatibility, making sure that code without exception tracking continues to work and ca…
In this work, we study the fundamental problems of counting and sampling traces that a regular language touches. Formally, one fixes the alphabet Σ and an independence relation I ⊆ Σ × Σ. The computational problems we address take as input a regular language L over Σ, presented a…
Hardware-software contracts are abstract specifications of a CPU’s leakage behavior. They enable verifying the security of high-level programs against side-channel attacks without having to explicitly reason about the microarchitectural details of the CPU. Using the abstraction p…
Convertibility checking — determining whether two lambda-terms are equal up to reductions — is a crucial component of proof assistants and dependently-typed languages. Practical implementations often use heuristics to quickly conclude that two terms are convertible, or are not co…
Hamiltonian Monte Carlo (HMC) is a successful generic inference method in probabilistic programming, but in its ordinary formulation it needs gradients and finite-dimensional parameter spaces. In Haskell, lazy evaluation lets probabilistic programs express stochastic processes an…
The growing demand for productivity in hardware development opens up new opportunities for applying programming language (PL) techniques to hardware description languages (HDLs). Chisel, a leading agile HDL, embraces this shift by leveraging modern PL features to enhance hardware…