Towards a practical library for monadic equational reasoning in Coq

DOI10.1007/978-3-031-16912-0_6OpenAlexW4296963110MaRDI QIDQ6109209

Ayumu Saito, Reynald Affeldt

Publication date: 30 June 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-031-16912-0_6

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Program extraction for mutable arrays
• Declarative pearl: deriving monadic quicksort
• Handling local state with global state
• A hierarchy of monadic effects for program verification using equational reasoning
• Packaging Mathematical Structures
• Type-Based Termination with Sized Products
• Modular Monad Transformers
• Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
• A trustful monad for axiomatic reasoning with probability and nondeterminism
• Just do it
• MRI: Modular reasoning about interference in incremental programming

This page was built for publication: Towards a practical library for monadic equational reasoning in Coq