
Eff
 Referenced in 20 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...

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

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

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...

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

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

Monomorphic Monad
 Referenced in 3 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...

TateOnProducts
 Referenced in 4 articles
[sw12475]
 twisted global sections, and also the Beilinson monads of all twists. Although the Tate resolution ... computed efficiently, starting either from a Beilinson monad or from a multigraded module...

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...

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

Certification_Monads
 Referenced in 2 articles
[sw32235]
 Certification Monads. This entry provides several monads intended for the development of standalone certifiers ... specifically, there are three flavors of error monads (the sum type, for the case where ... monadic functions are total; an instance of the former, the so called check monad, yielding ... explicit bottom element) and a parser monad built on top. All of this monads...

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...

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