ABSTRACT. We extend the Dafny system with an interactive proof mode. We present how the interactive proof mode can be used on a motivating example, we discuss the underlying architecture of the system, and provide a prototype implementation.

ABSTRACT. This work investigates resource improvements for probabilistic lazy PCF, a simply typed, higher-order call-by-need functional language with natural numbers, branching, fixpoints, and probabilistic choice. Building on deterministic improvement theory, a contextual cost improvement preorder is defined, requiring semantic equivalence and non-increasing expected reduction steps in all contexts. To avoid context quantification, distribution-cost improvement is introduced as an intrinsic preorder that compares per-value conditional expected steps. The main result establishes that both preorders coincide for closed programs of number type. This extends the distribution-equivalence characterisation to the resource-sensitive setting and enables local, context-free improvement proofs. As applications, garbage collection and a surface unique-copying transformation are verified as cost improvements, while deterministic common subexpression elimination is conjectured to exhibit the same property.

ABSTRACT. Trace logic is an expressive formalism for specifying the step-wise behaviors of recursive programs using state predicates, binary relations, sequential composition, and fixed points. By characterizing a program via its strongest trace formula, verification is reduced to checking the validity of trace formula implications. However, existing proof systems for trace logic are limited to finite traces and rely on explicit fixed-point induction rules, which pose challenges for automated proof search since invariants must be explicitly provided. In this work, we extend trace logic with greatest fixed points to express infinite, reactive behaviors. Furthermore, we propose a cyclic proof system for checking trace formula implications in this extended logic. By representing inductive and co-inductive reasoning as cyclic structures within the proof derivation, our system reduces the need for explicit invariants. Finally, we formally establish the soundness of our proposed system.

ABSTRACT. We study rewriting for measurement-bearing expressions whose measured leaves carry both bounded uncertainty and observation-token identity. A token-sensitive enclosure semantics assigns each expression its warranted enclosure—the set of values realizable by token-consistent hidden-value environments. Over that denotational core we define two rewrite judgments mechanized in Lean 4: RewritesTo for sound one-way claim tightening via enclosure containment, and Interchangeable for genuine equivalence via enclosure equality. The checked development establishes three compact classification results: same-token cancellation, shared-background subtraction, and same-token self-division over positive intervals are interchangeable with their simplified forms, while the corresponding distinct-token variants support only one-way tightening. Its main negative result is that provenance-blind summaries—even ones that preserve intervals, dimensions, and syntax modulo token erasure—cannot in general recover the correct rewrite class. We also show that on the exact fragment both rewrite judgments collapse to ordinary equality of exact denotations. All stated results are sorry-free in Lean 4.

ABSTRACT. In an introductory programming class using, e.g., Python, students are often asked to modify sample programs under specific coding constraints so that the modified programs prompt the printing of expected results by means of print statements in the sample programs. In grading the submitted programs, checking only the correctness of the required printing is insufficient, as it cannot detect unacceptable computational behaviors, deceptive printing, and/or violations of coding constraints. In this paper, we propose a method to support the grading of introductory programming assignments based on the comparison of rewrite sequences of rewrite systems obtained from a pre-prepared answer program and students' submitted programs. In our method, both the answer program and submitted programs are transformed into logically constrained rewrite systems, respectively, and their rewrite sequences from the same initial state for the required execution of the assignment are compared. This enables us to detect differences in execution, such as the use of different constructs or incorrect loop conditions.

ABSTRACT. Code fusion, also called deforestation, is a compiler-optimization technique that removes intermediate data structures. Though it has been studied in the literature for over 30 years, it is rarely used in production compilers due to the many challenges that automatic deforestation faces. We believe that many of these issues can be solved if we think about deforestation as an interactive process instead. In this work-in-progress report, we describe the user-controlled system we envision and give preliminary results from working on it. More specifically, we present a small, domain-specific language for deforestation and give intuition for the way many of previous deforestation techniques can be expressed in it.