• HasCasl

  • Referenced in 16 articles [sw00399]
  • Moreover, HasCasl provides dedicated specification support for monad-based functional-imperative programming with generic side ... effects, including a monad-based 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 nondeterminism-monad 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 post-conditions 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]
  • higher-order logic. The notion of a monad cannot be expressed within higher-order 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, monad-plus, 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]
  • first-class 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...