Mostly Sound Type System Improves a Foundational Program Verifier
No abstract available.
DOI 10.1007/978-3-319-03545-1_2
Related papers
- Sound gradual typing: only mostly dead OOPSLA 2017
- System FR: formalized foundations for the stainless verifier OOPSLA 2019
- Semantic foundations for typed assembly languages TOPLAS 2010
- A Formal Framework for the Java Bytecode Language and Verifier OOPSLA 1999
- Bidirectional Higher-Rank Polymorphism with Intersection and Union Types POPL 2025
- ιDOT: a DOT calculus with object initialization OOPSLA 2020
- VerusBelt: A Semantic Foundation for Verus's Proof-Oriented Extensions to the Rust Type System PLDI 2026
- RefinedC: automating the foundational verification of C code with refined ownership types PLDI 2021