The following pages link to Ynot (Q5178765):
Displaying 15 items.
- Ynot (Q24263) (← links)
- Specification patterns for reasoning about recursion through the store (Q393092) (← links)
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control (Q444460) (← links)
- Trace-based verification of imperative programs with I/O (Q617977) (← links)
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (Q670699) (← links)
- A shape graph logic and a shape system (Q744329) (← links)
- Dijkstra and Hoare monads in monadic computation (Q890377) (← links)
- Refinement to imperative HOL (Q1739909) (← links)
- Type-specialized staged programming with process separation (Q1929349) (← links)
- Modular verification of programs with effects and effects handlers (Q1996433) (← links)
- Modular verification of programs with effects and effect handlers in Coq (Q2024352) (← links)
- From Proposition to Program (Q2798255) (← links)
- Refinement to Imperative/HOL (Q2945637) (← links)
- Partiality, State and Dependent Types (Q3007667) (← links)
- A Hoare Logic for the State Monad (Q3183544) (← links)
