Ynot: dependent types for imperative programs
From MaRDI portal
Recommendations
Cited in
(27)- Specification patterns for reasoning about recursion through the store
- Nested Hoare Triples and Frame Rules for Higher-Order Store
- Verification of non-functional programs using interpretations in type theory
- From proposition to program. Embedding the refinement calculus in Coq
- Refinement to imperative HOL
- scientific article; zbMATH DE number 1420787 (Why is no real title available?)
- Modular verification of programs with effects and effect handlers in Coq
- Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
- Dijkstra and Hoare monads in monadic computation
- Trace-based verification of imperative programs with I/O
- Ynot
- A shape graph logic and a shape system
- Protocol combinators for modeling, testing, and execution of distributed systems
- Partiality, state and dependent types
- Type-specialized staged programming with process separation
- Refinement to Imperative/HOL
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
- Mtac: a monad for typed tactic programming in Coq
- Correctly compiling proofs about programs without proving compilers correct
- Dependent types and multi-monadic effects in \(\mathrm{F}^*\)
- Quantum Hoare type theory: extended abstract
- Modular verification of programs with effects and effects handlers
- Foundations of dependent interoperability
- Effective interactive proofs for higher-order imperative programs
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
- SMLtoCoq: automated generation of Coq specifications and proof obligations from SML programs with contracts
- A Hoare Logic for the State Monad
This page was built for publication: Ynot: dependent types for imperative programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5178765)
