Ynot
From MaRDI portal
Publication:5178765
DOI10.1145/1411204.1411237zbMath1323.68142OpenAlexW4245524452MaRDI QIDQ5178765
Aleksandar Nanevski, Paul Govereau, Greg Morrisett, Avraham Shinnar, Lars Birkedal
Publication date: 16 March 2015
Published in: Proceedings of the 13th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1411204.1411237
Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Logic in computer science (03B70)
Related Items
A Hoare Logic for the State Monad, Refinement to Imperative/HOL, Type-specialized staged programming with process separation, Specification patterns for reasoning about recursion through the store, Dijkstra and Hoare monads in monadic computation, Trace-based verification of imperative programs with I/O, 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, Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits, Refinement to imperative HOL, Partiality, State and Dependent Types, Modular verification of programs with effects and effects handlers, Modular verification of programs with effects and effect handlers in Coq, From Proposition to Program, A shape graph logic and a shape system, Ynot, Nested Hoare Triples and Frame Rules for Higher-Order Store, Protocol combinators for modeling, testing, and execution of distributed systems
Uses Software