3 citations · 3 across the 3 of their papers we have counts for
Showing cs.PLShow all
2 papers · 1 filter
cs.PL2025
A Coq implementation of a Theory of Tagged Objects
Matthew Gates, Alex Potanin
We present a first step towards the Coq implementation of the Theory of Tagged Objects formalism. The concept of tagged types is encoded, and the soundness proofs are discussed wit…
cs.PL2024
Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Extended Version)
David Young, Ziyi Yang, Ilya Sergey +1
Synthetic Separation Logic (SSL) is a formalism that powers SuSLik, the state-of-the-art approach for the deductive synthesis of provably-correct programs in C-like languages that…