swMATH12334MaRDI QIDQ24263FDOQ24263
Author name not available (Why is that?)
Official website: http://lambda-the-ultimate.org/node/2638
Cited In (58)
- Specification patterns for reasoning about recursion through the store
- Dijkstra Monads in Monadic Computation
- From proposition to program. Embedding the refinement calculus in Coq
- Refinement to imperative HOL
- Title not available (Why is that?)
- Sound, modular and compositional verification of the input/output behavior of programs
- Two for the price of one: lifting separation logic assertions
- Just do it
- Proceedings of the 13th ACM SIGPLAN international conference on Functional programming
- Toward a verified relational database management system
- MoSeL
- Program extraction for mutable arrays
- Dijkstra and Hoare monads in monadic computation
- Trace-based verification of imperative programs with I/O
- A shape graph logic and a shape system
- Partiality, state and dependent types
- Type-specialized staged programming with process separation
- AURA
- Crowfoot
- ARA
- KAT-ML
- Autolocker
- Flask
- EasyCrypt
- jStar
- Aglet
- CFML
- Rtac
- VeriML
- Security-typed programming within dependently typed programming
- Mtac: a monad for typed tactic programming in Coq
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
- Cogent
- Nested Hoare triples and frame rules for higher-order store
- Grail
- A3PAT
- TAG
- CSimpl
- Camelot
- AVL trees
- Equations
- Separation Logic
- VST-Floyd
- MiniML
- Secure distributed programming with value-dependent types
- FreeSpec
- Program analysis and verification based on Kleene algebra in Isabelle/HOL
- Probabilistic relational verification for cryptographic implementations
- Free theorems involving type constructor classes, functional pearl
- Effective interactive proofs for higher-order imperative programs
- A Deadlock-Free Semantics for Shared Memory Concurrency
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
- Combining proofs and programs in a dependently typed language
- Programming and reasoning with algebraic effects and dependent types
- Structuring the verification of heap-manipulating programs
- Correct-by-construction concurrency: using dependent types to verify implementations of effectful resource usage protocols
- A Hoare Logic for the State Monad
- Nested Hoare Triples and Frame Rules for Higher-Order Store
This page was built for software: Ynot
