Programming Languages
Despite numerous previous formalisation projects targeting Verilog, the semantics of Verilog defined by the Verilog standard -- Verilog's simulation semantics -- has thus far eluded definitive mathematical formalisation. Previous projects…
Semantics-Guided Synthesis (SemGuS) provides a framework to specify synthesis problems in a solver-agnostic and domain-agnostic way, by allowing a user to provide both the syntax and semantics of the language in which the desired program…
This paper presents an automated reasoning technique for checking equivalence between graph database queries written in Cypher and relational queries in SQL. To formalize a suitable notion of equivalence in this setting, we introduce the…
We introduce extensions to Data Spatial Programming (DSP) that enable scale-agnostic programming for application development. Building on DSP's paradigm shift from data-to-compute to compute-to-data, we formalize additional intrinsic…
Nondeterminism introduced by race conditions and message reorderings makes parallel and distributed programming hard. Nevertheless, promising approaches such as LVars and CRDTs address this problem by introducing a partial order structure…
Ensuring the correct functionality of systems software, given its safety-critical and low-level nature, is a primary focus in formal verification research and applications. Despite advances in verification tooling, conventional programmers…
Rust is gaining popularity for its well-known memory safety guarantees and high performance, distinguishing it from C/C++ and JVM-based languages. Its compiler, rustc, enforces these guarantees through specialized mechanisms such as trait…
We propose a calculus for modeling implicit programming that supports first-class, overlapping, locally scoped, and higher-order instances with higher-kinded types. We propose a straightforward generalization of the well-established System…
Rewriting C code in Rust provides stronger memory safety, yet migrating large codebases such as the 32-million-line Linux kernel remains challenging. While rule-based translators (e.g., C2Rust) provide accurate yet largely unsafe Rust…
Visual learners think in pictures rather than words and learn best when they utilize representations based on graphs, tables, charts, maps, colors and diagrams. We propose a new pedagogy for teaching pointers in the C programming language…
We report on a recent breakthrough in rule-based graph programming, which allows us to reach the time complexity of imperative linear-time algorithms. In general, achieving the complexity of graph algorithms in conventional languages using…
Interaction nets constitute a visual programming language grounded in graph transformation. Owing to their distinctive properties, they inherently facilitate parallelism in the rewriting step. This paper showcases a simple and concise…
As large language models have shown remarkable capabilities in conversing via natural language, the question arises as to how LLMs could potentially assist chemical engineers in research and industry with domain-specific tasks. We generate…
Can a memory manager be built with fast bump-pointer allocation, single-pass heap tracing, and a low upper bound on memory overhead? The Immix collector answered in the affirmative for the first two, but the granularity at which it reclaims…
Program synthesis from input-output examples, also called programming by example (PBE), has had tremendous impact on automating end-user tasks. Large language models (LLMs) have the ability to solve PBE tasks by generating code in different…
Probabilistic programming is becoming increasingly popular thanks to its ability to specify problems with a certain degree of uncertainty. In this work, we focus on term rewriting, a well-known computational formalism. In particular, we…
Effect handlers are a powerful abstraction for defining, customising, and composing computational effects. Statically ensuring that all effect operations are handled requires some form of effect system, but using a traditional effect system…
In recent years, there has been extensive research on how to extend general-purpose programming language semantics with domain-specific modeling constructs. Two areas of particular interest are (i) universal probabilistic programming where…
Multiple types can represent the same concept. For example, lists and trees can both represent sets. Unfortunately, this easily leads to incomplete libraries: some set-operations may only be available on lists, others only on trees.…
Quantum computing leverages the principles of quantum mechanics to perform computations far beyond the capabilities of classical systems, particularly in fields such as cryptography and optimization. However, current quantum programming…