Showing cs.LOShow all
3 papers · 1 filter
cs.LO2026
Domain Theory Meets Interaction Trees in Rocq
David Nowak, Vlad Rusu
We present a domain-theoretical formalization of interaction trees in the Rocq prover. Unlike existing formalizations, ours does not rely on Rocq's built-in coinduction. Hence, we…
cs.LO2022
Proceedings of the Sixth Working Formal Methods Symposium
Vlad Rusu
It is our pleasure to present the papers of the sixth Working Formal Methods Symposium (FROM 2022) held at the "Al. I. Cuza" university of Iasi, Romania on September 19-20, 2022. F…
cs.LO2019
(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic
Vlad Rusu, David Nowak
Reachability Logic is a formalism that can be used, among others, for expressing partial-correctness properties of transition systems. In this paper we present three proof systems…