Showing cs.PLShow all
2 papers · 1 filter
cs.PL2026
Type Safety via Hoare Logic with Separation and Pure Types
Wenhua Li, Darius Foo, Quang Trung Ta +1
Type safety has traditionally rested on carefully crafted type systems, under the motto "well-typed programs cannot go wrong". Modern demands push type systems past this basic guar…
cs.PL2024
Staged Specification Logic for Verifying Higher-Order Imperative Programs (Technical Report)
Darius Foo, Yahui Song, Wei-Ngan Chin
Higher-order functions and imperative states are language features supported by many mainstream languages. Their combination is expressive and useful, but complicates specification…