Bidirectional Type Checking for Existential Types with Higher-Rank Polymorphism
Abstract elided by the publisher.
14,842 papers · page 13 of 743
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
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…
Abstract elided by the publisher.
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…
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…
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…
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…
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…
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…
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 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…
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…
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 …
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.
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…
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…
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…