Bidirectional Type Checking for Existential Types with Higher-Rank Polymorphism
Abstract elided by the publisher.
14,842 papers · page 13 of 743
Practical Refinement Session Type Inference
Abstract elided by the publisher.
A Formally Verified Procedure for Width Inference in FIRRTL
Abstract elided by the publisher.
Dependently-Typed AARA: A Non-Affine Approach for Resource Analysis of Higher-Order Programs
Abstract elided by the publisher.
Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
This paper presents several efficient decision procedures for trace equivalence of GKAT automata, which make use of on-the-fly symbolic techniques via SAT solvers. To demonstrate applicability of our algorithms, we designed symbolic derivatives for CF-GKAT, a practical system bas…
Auditing Rust Crates Effectively
Abstract elided by the publisher.
Executable Counterfactuals: A Causal Calculus for Concurrent Systems (Keynote)
Modern software systems are increasingly concurrent, adaptive, and generative, yet our formal methods still focus primarily on describing what systems do rather than why particular behaviours arise. In this talk, I will present ongoing work on a causal calculus for concurrent sys…
Comparing Solver Representations for Analyzing Cardinality-Based Feature Models
The variability of product lines can exceed purely Boolean configuration spaces. Cardinality-based Feature Models (CFMs) are employed to model multi-instantiation of features along with individually configurable subtrees. Due to the added complexity, the analysis of CFMs cannot b…
Modular Substructural Constraints for Embedded DSLs
Substructural type systems provide static guarantees about resource usage in programs. In most practical systems, however, the available usage constraints and their composition are predetermined by the language design, with only limited support for application programmers to cust…
TurtleTalk: A DSL for Constraint-Based Turtle Graphics in Programmatic CAD
In programmatic CAD (PCAD), 3D shapes are generally modelled either by position-based composition of simpler shapes, or by direct generation via path-based techniques (e.g., extrusions, sweeps, revolves). While state-of-the-art PCAD tools effectively support position-based modell…
Programmable Record Types in Haskell
In Haskell, accessing an object's fields requires deconstructing it. Thankfully, it is possible to name the fields of a data type using the record syntax, allowing programmers to access objects' fields using their name. This can help improve the readability of Haskell code. Howev…
Metis: A Compositional DSL for Board Games and Game Tree Search
We present Metis, a domain-specific language embedded in Haskell for two-player board games on rectangular boards that exploits their shared structure (setup, rules, win condition) through three composable mini-DSLs. Atomic operations for placing, moving, and capturing pieces com…
Stageleft: Multi-stage Programming in Standard Rust
Rust has emerged as a popular systems language with growing interest in metaprogramming, yet it lacks staging support—developers must write unsafe, untyped macros instead. We present Stageleft, a library that brings type-safe staged programming to standard Rust without compiler m…
Synthesizing Recursive Functional Programs via Structure-Element Separation
Synthesizing recursive functional programs over algebraic data types from input-output examples remains challenging, largely due to the explosion of structurally distinct candidates during search. We present a synthesis approach for structurally recursive list/tree transformation…
Less Is More: Measuring How LLM Involvement Affects Chatbot Accuracy in Static Analysis
Large language models are increasingly used to make static analysis tools accessible through natural language, yet existing systems differ in how much they delegate to the LLM without treating the degree of delegation as an independent variable. We compare three architectures alo…
ATLAS: From Access conTrol Language to ACSL Specifications
Access control is a classical way to express which users are allowed to do which actions on which objects. Many formalisms study how to model access control policies. However, fewer works target formal verification of an actual implementation with respect to a given policy. This …
Bringing Mixed-Stage Programming to OCaml (Keynote)
Over the last three decades, multi-stage programming has been used to write high-level, type-safe, optimising code generators for a wide variety of domains, from database queries and stream processing to geometry, parsing, and differentiable programming.
The Next 700 Block-Based Editors (Keynote)
Block-based code editors have been adopted widely in classrooms with young learners, yet they are often perceived as inferior compared to the ultimate flexibility of text editors. Beyond blocks, alternatives to manipulating programs as text have been pursued through various struc…
Coercive Subtyping for Implicit Functorial Programming
Programming with typeclass-defined combinators like fmap allows programs a great deal of generality and concision, but programmers have to explicitly invoke combinators in the right places in order to get their programs to type check. In this paper, we propose inferring these ope…
Turning Parser Errors into Suggestions for REPL-Driven DSLs (Functional Pearl)
Many of the domain-specific languages we use every day are not written to files but typed at an interactive prompt, e.g., database shells, cloud CLIs, and in-house analytics consoles. For these REPL-driven command languages, autocomplete is, we argue, not a polish feature but a c…