
Eff
 Referenced in 19 articles
[sw22721]
 technical sense they are subsumed by the monadic approach to computational effects, but they offer ... programming that are not easily achieved with monads. In particular, algebraic effects are combined seamlessly ... whereas monad transformers are needed in the monadic style. The main idea...

HasCasl
 Referenced in 17 articles
[sw00399]
 Moreover, HasCasl provides dedicated specification support for monadbased functionalimperative programming with generic side ... effects, including a monadbased generic Hoare logic...

Mtac
 Referenced in 14 articles
[sw13075]
 Mtac: a monad for typed tactic programming in Coq. Effective support for custom proof automation ... these new tactical primitives in a monad, and instrumenting Coq so that it executes monadic...

F*
 Referenced in 20 articles
[sw27563]
 type system includes dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together...

Irdis
 Referenced in 19 articles
[sw09690]
 records with projection and update; Type classes; Monad comprehensions; Syntactic conveniences for lists, tuples, dependent...

Lava
 Referenced in 13 articles
[sw28643]
 exploits functional programming language features, such as monads and type classes, to provide multiple interpretations...

Refinement Monadic
 Referenced in 6 articles
[sw28551]
 Refinement for Monadic Programs. We provide a framework for program and data refinement in Isabelle/HOL ... framework is based on a nondeterminismmonad with assertions, i.e., the monad carries...

Dijkstra Shortest Path
 Referenced in 9 articles
[sw28550]
 implemented using the data refinement framework for monadic, nondeterministic programs. An efficient implementation is derived...

Mosel
 Referenced in 5 articles
[sw30493]
 Mosel: A flexible toolset for monadic secondorder logic. Mosel is a new tool ... analysis and verification in Monadic Secondorder Logic. In this paper we concentrate...

MSO_Regex_Equivalence
 Referenced in 7 articles
[sw32230]
 Words Based on Derivatives of Regular Expressions. Monadic secondorder logic on finite words...

LLFp
 Referenced in 4 articles
[sw20866]
 evidence, side conditions, and proof irrelevance using monads. We extend the constructive dependent type theory ... Logical Framework 𝖫𝖥 with monadic, dependent type constructors indexed with predicates over judgements, called Locks...

Monatron
 Referenced in 3 articles
[sw28602]
 Monatron: An Extensible Monad Transformer Library. Monads are pervasive in functional programming. In order ... their abstraction power, combinator libraries for monads are necessary. Monad transformers provide the basis...

CryptHOL
 Referenced in 5 articles
[sw28582]
 higher order logic. The language features monadic sequencing, recursion, random sampling, failures and failure handling...

Monomorphic Monad
 Referenced in 2 articles
[sw28583]
 higherorder logic. The notion of a monad cannot be expressed within higherorder logic ... system restrictions. We show that if a monad is used with values of only ... library of effect specifications and implementations of monads and monad transformers. Hence, we can abstract ... over the concrete monad in HOL definitions and thus use the same definition for different...

Tycon
 Referenced in 2 articles
[sw25267]
 Tycon: Type Constructor Classes and Monad Transformers. These theories contain a formalization of first class ... ICFP 2012 paper Formal Verification of Monad Transformers by the author. The formalization ... Haskell, we define classes for functors, monads, monadplus, etc. Each one includes ... instantiate the type class hierarchy with various monads and monad transformers...

Aglet
 Referenced in 4 articles
[sw13305]
 proofs. Third, we represent computations using a monad indexed by pre and postconditions drawn...

TravMC2
 Referenced in 4 articles
[sw20008]
 using alternating parity tree automata (or equivalently monadic second order logic). Our experimental results offer...

qPCF
 Referenced in 4 articles
[sw20267]
 manage circuits and an implicit form of monad to manage quantum states via a destructive...

Unbound
 Referenced in 4 articles
[sw22613]
 error messages), and integration with Haskell’s monad transformer library...

Lwt
 Referenced in 4 articles
[sw32970]
 Programs involving threads are written in a monadic style. This makes it possible to write...