一句话：提出 Agda 嵌入式 DSL Citrus，支持超导电子电路的门等价与代数推理，并证明 PyLSE 无法处理的任务。
超导电子学（SCE）电路设计依赖高层抽象与验证，但现有 PyLSE 通过将基本结构编译为时间自动机进行模型检测，受状态空间爆炸限制，且缺少对门等价的代数推理支持。本文提出 Citrus：一个用依赖类型语言 Agda 实现的嵌入式 DSL，形式化 SCE 电路的高层抽象，定义 SCE 门的等价关系与等式推理引理，并提供函数组合子以设计和分析更大电路。Citrus 与 PyLSE 等价，但增强了表达力与验证能力。作者用两组案例研究评估：一是形式化证明 SCE 设计者常用但此前未证的多条等式定律；二是证明一个 PyLSE 因模型检测状态爆炸而无法证明的验证任务。结果表明 Citrus 能进行代数推理并扩展可验证范围。
We present Citrus, an embedded DSL in the dependently-typed language Agda that formalizes high-level abstractions for specifying and reasoning about superconducting electronics (SCE) circuits. We build on the existing PyLSE language, a Python DSL for writing SCE programs that provides facilities for simulating designs and for verification via model-checking (by compiling its basic structures into Timed Automata). Citrus expands on the verification capabilities of PyLSE by defining equivalence over SCE gates, as well as corresponding equational reasoning lemmas, and providing a toolbox of functional combinators for designing and analyzing larger circuits. The formalization enables a large increase in expressivity, specifically in the form of algebraic reasoning about SCE designs. We evaluate Citrus using two sets of case studies. In the first, we establish several equational laws which are often used by SCE designers but have yet to be formally proven. In the second, we prove a verification task which the PyLSE language was unable to prove due to the state space explosion inherent in its model checking approach. In this way, Citrus provides a simple functional programming language, equivalent to PyLSE, with increased verification capabilities.
@article{KringenSH26,
title = {Citrus: Algebraic Reasoning about Superconductor Electronics},
author = {Harlan Kringen and Timothy Sherwood and Ben Hardekopf},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828690}
}