Ynot

swMATH12334MaRDI QIDQ24263FDOQ24263

Author name not available (Why is that?)

Described by source

• Ynot

Cited In (33)

• Specification patterns for reasoning about recursion through the store
• Dijkstra Monads in Monadic Computation
• Free theorems involving type constructor classes
• Refinement to imperative HOL
• Title not available (Why is that?)
• Two for the price of one: lifting separation logic assertions
• Correct-by-Construction Concurrency: Using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols
• Mtac: A monad for typed tactic programming in Coq
• Just do it
• Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL
• Proceedings of the 13th ACM SIGPLAN international conference on Functional programming
• From Proposition to Program
• Toward a verified relational database management system
• Program extraction for mutable arrays
• Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs
• Dijkstra and Hoare monads in monadic computation
• Trace-based verification of imperative programs with I/O
• A shape graph logic and a shape system
• Type-specialized staged programming with process separation
• Security-typed programming within dependently typed programming
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
• Secure distributed programming with value-dependent types
• Probabilistic relational verification for cryptographic implementations
• Partiality, State and Dependent Types
• Effective interactive proofs for higher-order imperative programs
• A Deadlock-Free Semantics for Shared Memory Concurrency
• Nested Hoare Triples and Frame Rules for Higher-order Store
• 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
• A Hoare Logic for the State Monad
• Nested Hoare Triples and Frame Rules for Higher-Order Store

This page was built for software: Ynot