Mechanizing a Proof-Relevant Logical Relation for Timed Message-Passing Protocols
Tesla Zhang, Asher Kornfeld, Rui Li, Sonya Simkin, Yue Yao, Stephanie Balzer
TL;DR
This work presents the first mechanization in the Rocq proof assistant of YaoPOPL2025's proof-relevant logical relation for timed message-passing protocols, enabling machine-checked verification of protocol compliance across heterogeneous components. It formalizes a timed intuitionistic linear logic session-type system (ILLST) with temporal predicates, develops an algebra of computable trajectories, and proves the Fundamental Theorem of the Logical Relation (FTLR) to connect types with observable runtime behavior. The mechanization includes a detailed treatment of trajectories, transports, and a realizability relation, along with design and implementation decisions tailored to Rocq, and an artifact that reproduces the results. The approach supports modularity across languages and provides a scalable path towards automated verification of timed protocols in IoT and real-time systems, with rigorous correctness guarantees grounded in a machine-checked framework.
Abstract
Semantic typing has become a powerful tool for program verification, applying the technique of logical relations as not only a proof method, but also a device for prescribing program behavior. In recent work, Yao et al. scaled semantic typing to the verification of timed message-passing protocols, which are prevalent in, e.g., IoT and real-time systems applications. The appeal of semantic typing in this context is precisely because of its ability to support typed and untyped program components alike -- including physical objects -- which caters to the heterogeneity of these applications. Another demand inherent to these applications is timing: constraining the time or time window within which a message exchange must happen. Yao et al. equipped their logical relation not only with temporal predicates, but also with computable trajectories, to supply the evidence that an inhabitant can step from one time point to another one. While Yao et al. provide the formalization for such a verification tool, it lacks a mechanization. Mechanizing the system would not only provide a machine proof for it, but also facilitate scalability for future extensions and applications. This paper tackles the challenge of mechanizing the resulting proof-relevant logical relation in a proof assistant. allowing trajectories to be interleaved, partitioned, and concatenated, while the intended equality on trajectories is the equality of their graphs when seen as processes indexed by time. Unfortunately, proof assistants based on intensional type theory only have modest support for such equations, forcing a prolific use of transports. This paper reports on the process of mechanizing Yao et al.'s results, comprising the logical relation, the algebra of computable trajectories with supporting lemmas, and the fundamental theorem of the logical relation, in the Rocq theorem prover.