Pages that link to "Item:Q3546051"
From MaRDI portal
The following pages link to Hoare type theory, polymorphism and separation (Q3546051):
Displaying 18 items.
- Symbolic execution proofs for higher order store programs (Q287265) (← links)
- Specification patterns for reasoning about recursion through the store (Q393092) (← links)
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (Q670699) (← links)
- Building program construction and verification tools from algebraic principles (Q736461) (← links)
- Towards patterns for heaps and imperative lambdas (Q2374314) (← links)
- Dependent Types and Fibred Computational Effects (Q2811331) (← links)
- Crowfoot: A Verifier for Higher-Order Store Programs (Q2891407) (← links)
- Partiality, State and Dependent Types (Q3007667) (← links)
- Compositional System Security with Interface-Confined Adversaries (Q3178245) (← links)
- An Isbell duality theorem for type refinement systems (Q4640309) (← links)
- Syntactic soundness proof of a type-and-capability system with hidden state (Q4912884) (← links)
- (Q5020617) (← links)
- Relational cost analysis in a functional-imperative setting (Q5020903) (← links)
- Mtac: A monad for typed tactic programming in Coq (Q5371944) (← links)
- Foundations of mathematics in polymorphic type theory (Q5950500) (← links)
- Safe session-based concurrency with shared linear state (Q6535247) (← links)
- Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding (Q6611968) (← links)
- Quantum Hoare type theory: extended abstract (Q6645590) (← links)