Ynot

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

zbMATH Keywords

monadstype theoryHoare logicseparation logic

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Logic in computer science (03B70)

Related Items (18)

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

• Spec#
• LEGO
• Unnamed Item
• Unnamed Item

This page was built for publication: Ynot