Proving Syntactic Properties of Exceptions in an Ordered Logical Framework
No abstract available.
Related papers
- An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic POPL 2024
- An Axiomatic Basis for Computer Programming on Relaxed Hardware Architectures: The AxSL Logics TOPLAS 2026
- Di- is for Directed: First-Order Directed Type Theory via Dinaturality POPL 2026
- All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs POPL 2026
- Modeling Reachability Types with Logical Relations: Semantic Type Soundness, Termination, Effect Safety, and Equational Theory OOPSLA 2025
- Failure is Not an Option - An Exceptional Type Theory ESOP 2018
- Full functional verification of linked data structures PLDI 2008
- An Isabelle/HOL Framework for Synthetic Completeness Proofs CPP 2025