编程语言

We propose a design for a functional programming language for autonomous agents, built off the ideas and motivations of Behavior Trees (BTs). BTs are a popular model for designing agents behavior in robotics and AI. However, as their growth…

Static single assignment form, or SSA, has been the dominant compiler intermediate representation for decades. In this paper, we give a type theory for a variant of SSA, including its equational theory, which are strong enough to validate a…

Process algebras have been widely used to verify security protocols in a formal manner. However they mostly focus on synchronous communication based on the exchange of messages. We present an alternative approach relying on asynchronous…

We propose an overview of the decentralized reconfiguration language Concerto-D through its Maude formalization. Concerto-D extends the already published Concerto language. Concerto-D improves on two different parameters compared with…

While formal models of concurrency tend to focus on synchronous communication, asynchronous communication is relevant in practice. In this paper, we will discuss asynchronous communication in the context of session-based concurrency, the…

Large language models (LLMs) show promise in code translation due to their ability to generate idiomatic code. However, a significant limitation when using LLMs for code translation is scalability: existing works have shown a drop in…

When proving the correctness of a method for slicing probabilistic programs, it was previously discovered by the authors that for a fixed point iteration to work one needs a non-standard starting point for the iteration. This paper presents…

Static analysis by abstract interpretation is generally designed to be "sound", that is, it should not claim to establish properties that do not hold-in other words, not provide "false negatives" about possible bugs. A rarer requirement is…

In this paper, we present the design of Owi, a symbolic interpreter for WebAssembly written in OCaml, and how we used it to create a state-of-the-art tool to find bugs in programs combining C and Rust code. WebAssembly (Wasm) is a binary…

Live programming features can be found in a range of programming environments, from individual prototypes to widely used environments. While liveness is generally considered a useful property, there is little empirical evidence on when and…

Many improvements to programming have come from shortening feedback loops, for example with Integrated Development Environments, Unit Testing, Live Programming, and Distributed Version Control. A barrier to feedback that deserves greater…

Various categories have been proposed as targets for the denotational semantics of higher-order probabilistic programming languages. One such proposal involves joint probability distributions (couplings) used in Bayesian statistical models…

Distributed systems adopt weak consistency to ensure high availability and low latency, but state convergence is hard to guarantee due to conflicts. Experts carefully design replicated data types (RDTs) that resemble sequential data types…

We study the problem of bounding the posterior distribution of discrete probabilistic programs with unbounded support, loops, and conditioning. Loops pose the main difficulty in this setting: even if exact Bayesian inference is possible,…

Over the last two decades practically all object-oriented programming languages have introduced features that are well-known from functional programming languages. But many features that were introduced were fragmentary. In Java-TX we…

The gradual guarantee is an important litmus test for gradually typed languages, that is, languages that enable a mixture of static and dynamic typing. The gradual guarantee states that changing the precision of a type annotation does not…

I present a novel formulation of substitution, where facts about substitution that previously required tens or hundreds of lines to justify in a proof assistant now follow immediately - they can be justified by writing the four letters…

A computational limit of combining partial evaluation and program inversion is investigated. Using a reversible Turing machine interpreter, we show that the first Futamura and inversion projections can produce not only functionally but also…

This Festschrift is dedicated to Peter Thiemann on the occasion of his sixtieth birthday, celebrating his significant contributions to the field of programming languages. Over the span of more than three decades, Peter has worked on a wide…

Computer science education has been at the heart of Scheme from the beginning. The language was designed in the 1970s concurrently with the MIT course 6.001 and the textbook "Structure and Interpretation of Computer Programs" (SICP). To…