Dijkstra monads for free

DOI10.1145/3009837.3009878zbMath1380.68266arXiv1608.06499OpenAlexW2507710874MaRDI QIDQ5370885

Kenji Maillard, Cătălin Hriţcu, Aseem Rastogi, Danel Ahman, Jonathan Protzenko, Guido Martínez, Nikhil Swamy, Gordon D. Plotkin

Publication date: 20 October 2017

Published in: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1608.06499

zbMATH Keywords

verificationdependent typesproof assistantseffectful programming

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (5)

Weakest preconditions in fibrations ⋮ Combining algebraic effect descriptions using the tensor of complete lattices ⋮ Generalized arrays for Stainless frames ⋮ Unnamed Item ⋮ Weakest preconditions in fibrations

Uses Software

• Dafny
• Haskell
• Why3
• z3
• F*

This page was built for publication: Dijkstra monads for free