7 citations · 9 across the 6 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…
On Algebraic Abstractions for Concurrent Separation Logics
František Farka, Aleksandar Nanevski, Anindya Banerjee +2
Concurrent separation logic is distinguished by transfer of state ownership upon parallel composition and framing. The algebraic structure that underpins ownership transfer is that…
Coinductive Soundness of Corecursive Type Class Resolution
František Farka, Ekaterina Komendantskaya, Kevin Hammond
Horn clauses and first-order resolution are commonly used to implement type classes in Haskell. Several corecursive extensions to type class resolution have recently been proposed,…