• Eff

  • Referenced in 15 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 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...
  • F*

  • Referenced in 19 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 nondeterminism-monad 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 second-order logic. Mosel is a new tool ... analysis and verification in Monadic Second-order Logic. In this paper we concentrate...
  • Irdis

  • Referenced in 6 articles [sw09690]
  • records with projection and update; Type classes; Monad comprehensions; Syntactic conveniences for lists, tuples, dependent...
  • 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...
  • Monomorphic Monad

  • Referenced in 2 articles [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 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, monad-plus, 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 post-conditions drawn...
  • 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...
  • TateOnProducts

  • Referenced in 2 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...
  • TravMC2

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