
HasCasl
 Referenced in 16 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 13 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...

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

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

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

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

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

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

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

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

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

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

Imperative Refinement
 Referenced in 3 articles
[sw29235]
 uses the Monadic Refinement Framework as a frontend for the specification of the abstract programs...

Monomorphic Monad
 Referenced in 1 article
[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 1 article
[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...

rmonad
 Referenced in 1 article
[sw22071]
 Haskell rmonad package. A library for restricted monads based on associated datatypes. This allows datatypes ... such as Set to be made into monads. Users can either use the NoImplicitPrelude extension ... unEmbed combinators to use the normal Prelude monad operations...

Memoization
 Referenced in 1 article
[sw28640]
 into a monadified version in a state monad or the Imperative HOL heap monad ... memory implementations for the two types of monads. A number of simple techniques allow...

CLF
 Referenced in 2 articles
[sw21372]
 firstclass representation of concurrent executions as monadic expressions. We illustrate the representation techniques available...

HNT
 Referenced in 2 articles
[sw22614]
 rewriting algorithms with freshness contexts; a monadic framework handling environments, freshness contexts, substitutions easily...

Celf
 Referenced in 2 articles
[sw22718]
 support representation of state and a monad to support representation of concurrency. It relies...