编程语言
Ownership and borrowing systems, designed to enforce safe memory management without the need for garbage collection, have been brought to the fore by the Rust programming language. Rust also aims to bring some guarantees offered by…
Graded type systems, such as the one underlying the Granule programming language, allow various different properties of a program's behaviour to be tracked via annotating types with additional information, which we call grades. One example…
Session types provide guarantees about concurrent behaviour and can be understood through their correspondence with linear logic, with propositions as sessions and proofs as processes. However, a strictly linear setting is somewhat…
Failure transparency enables users to reason about distributed systems at a higher level of abstraction, where complex failure-handling logic is hidden. This is especially true for stateful dataflow systems, which are the backbone of many…
We develop a declarative DSL - \cf - that can be used to specify Abstract Interpretation-based DNN certifiers. In \cf, programmers can easily define various existing and new abstract domains and transformers, all within just a few 10s of…
Concurrent objects form the foundation of many applications that exploit multicore architectures and their importance has lead to informal correctness arguments, as well as formal proof systems. Correctness arguments (as found in the…
Verification-aware programming languages such as Dafny and F* provide means to formally specify and prove properties of a program. Although the problem of checking an implementation against a specification can be defined mechanically, there…
Algebraic Data Types (ADTs) are an increasingly common feature in modern programming languages. In many implementations, values of non-nullary, multi-case ADTs are allocated on the heap, which may reduce performance and increase memory…
Charts, figures, and text derived from data play an important role in decision making, from data-driven policy development to day-to-day choices informed by online articles. Making sense of, or fact-checking, outputs means understanding how…
TScore is both an abstract formalism and its computer implementation to construct models of arbitrary kinds of time-related data. It is a research project about the semantics of musical notation, applying the method of computer-aided…
Verifying programs that manipulate tree data structures often requires complex, ad-hoc proofs that are hard to generalize and automate. This paper introduces an automatic technique for analyzing such programs. Our approach combines automata…
Real Time performance testing can be divided into two distinct parts: system test and algorithm test. System test checks that the right functions operate on the right data within power, latency, and other constraints under all conditions.…
Monadic programming presents a significant challenge for many programmers. In light of category theory, we offer a new perspective on the use of monads in functional programming. This perspective is clarified through numerous examples coded…
Large language models (LLMs) have reshaped the landscape of program synthesis. However, contemporary LLM-based code completion systems often hallucinate broken code because they lack appropriate context, particularly when working with…
With the large diversity of platforms and devices used by students, web applications increasingly suggest themselves as the solution of choice. Developing adequate educational programming environments in the browser, however, remains a…
Library learning is the process of building a library of common functionalities from a given set of programs. Typically, this process is applied in the context of aiding program synthesis: concise functions can help the synthesizer produce…
In C++, objects can be allocated in static memory, on the stack, or on the heap -- the latter being significantly more performance-costly than the former options. We hypothesized that programmers, particularly those involved in widely-used…
Session types are widely used as abstractions of asynchronous message passing systems. Refinement for such abstractions is crucial as it allows improvements of a given component without compromising its compatibility with the rest of the…
Rust aims to be a safe programming language applicable to systems programming applications. In particular, its type system has strong guardrails to prevent a variety of issues, such as memory safety bugs and data races. However, these…
After large models (LMs) have gained widespread acceptance in code-related tasks, their superior generative capacity has greatly promoted the application of the code LM. Nevertheless, the security of the generated code has raised attention…