3 citations · 6 across the 10 of their papers we have counts for
3 papers · 1 filter
Corten - Foundational Verification of Rust Programs
František Farka, Carmine Abate, Sven Linker +1
We present Corten, a foundational verification framework for Rust programs in the Rocq theorem prover, built on the Iris separation logic framework. Corten provides the first seman…
Interaction Tree Semantics for RISC-V: Bridging Compiler and Hardware Verification
Shuanglong Kan, Sebastian Ertel
The Instruction Set Architecture (ISA) is the contract between compilers and processors; proving this contract formally demands cross-level connection to existing mechanized compil…
Category-Theoretic Foundations of "STCLang: State Thread Composition as a Foundation for Monadic Dataflow Parallelism"
Sebastian Ertel, Justus Adam, Norman A. Rink +2
This manuscript gives a category-theoretic foundation to the composition of State Threads as a Foundation for Monadic Dataflow Parallelism. It serves as a supplementary formalizati…