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