Notions of computation and monads

DOI10.1016/0890-5401(91)90052-4zbMATH Open0723.68073OpenAlexW1997143185WikidataQ55895577 ScholiaQ55895577MaRDI QIDQ757075FDOQ757075

Authors: Eugenio Moggi 

Publication date: 1991

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(91)90052-4

Recommendations

• Publication:3202991
• Categorical combinators
• scientific article; zbMATH DE number 2087441
• Computational types from a logical perspective
• The Impact of the Lambda Calculus in Logic and Computer Science

zbMATH Keywords

monadscategorical semantics for computationsproving equivalence of programs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Cites Work

• Edinburgh LCF. A mechanized logic of computation
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The Category-Theoretic Solution of Recursive Domain Equations
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• First order categorical logic. Model-theoretical methods in the theory of topoi and related categories
• The formal theory of monads
• Strong functors and monoidal monads
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The linear abstract machine
• The hereditary partial effective functionals and recursion theory in higher types
• A category-theoretic account of program modules
• A syntactic theory of sequential state
• Verification of programs that destructively manipulated data
• New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic
• Indexed categories and their applications
• Computational foundations of basic recursive function theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (only showing first 100 items - show all)

• Mac Lane's comparison theorem for the Kleisli construction formalized in Coq
• Finitely presentable algebras for finitary monads
• Unguarded recursion on coinductive resumptions
• Reversible monadic computing
• Algebraic presentation of semifree monads
• Coalgebraic semantics for nominal automata
• Iterated covariant powerset is not a monad
• Combining semilattices and semimodules
• Semantics of value recursion for Monadic Input/Output
• Safe functional systems through integrity types and verified assembly
• Dependent types and fibred computational effects
• Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
• Evolution of rule-based programs
• Title not available (Why is that?)
• Complete Elgot monads and coalgebraic resumptions
• Fibrational modal type theory
• A general semantic construction of dependent refinement type systems, categorically
• Graded Hoare logic and its categorical semantics
• Commutative semantics for probabilistic programming
• The Giry monad is not strong for the canonical symmetric monoidal closed structure on \textbf {Meas}
• Codensity lifting of monads and its dual
• A (co)algebraic theory of succinct automata
• Amb Breaks Well-Pointedness, Ground Amb Doesn't
• Equational logic and categorical semantics for multi-languages
• Quantitative logics for equivalence of effectful programs
• Parametrized fixed points and their applications to session types
• The effects of effects on constructivism
• Weakest preconditions in fibrations
• Initial algebras and final coalgebras consisting of nondeterministic finite trace strategies
• Connected monads weakly preserve products
• Introducing a calculus of effects and handlers for natural language semantics
• Adjoint logic with a 2-category of modes
• Ambiguity and incomplete information in categorical models of language
• The arrow calculus
• Partial hyperdoctrines: categorical models for partial function logic and Hoare logic
• Categories of timed stochastic relations
• Dynamic game semantics
• The bang calculus and the two Girard's translations
• Generalized arrays for Stainless frames
• No-iteration mixed distributive laws
• Accessibility and presentability in 2-categories
• Program logic for higher-order probabilistic programs in Isabelle/HOL
• An Essay in λ‐Calculus
• C-system of a module over a \(Jf\)-relative monad
• The linear-non-linear substitution 2-monad
• Title not available (Why is that?)
• Predicate liftings and functor presentations in coalgebraic expression languages
• Interactive programming in Agda -- objects and graphical user interfaces
• Monoidal computer. III: A coalgebraic view of computability and complexity (extended abstract)
• Relating structure and power: comonadic semantics for computational resources
• Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
• Formal ball monads
• Boolean restriction categories and taut monads
• Noninterference in a predicative polymorphic calculus for access control
• Quotienting the delay monad by weak bisimilarity
• A simply typed \(\lambda\)-calculus of forward automatic differentiation
• A Semantical Approach to Equilibria and Rationality
• Synthesis of strategies using the Hoare logic of angelic and demonic nondeterminism
• No value restriction is needed for algebraic effects and handlers
• Unifying graded and parameterised monads
• Access control in a core calculus of dependency
• Monad compositions II: Kleisli strength
• Transactional events
• Eager and delayed contract monitoring for call-by-value and call-by-name evaluation
• A functional correspondence between monadic evaluators and abstract machines for languages with computational effects
• A theory of binding structures and applications to rewriting
• Game theoretic analysis of call-by-value computation
• A new framework for declarative programming
• Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code
• Title not available (Why is that?)
• Introducing \(\llparenthesis\lambda\rrparenthesis\), a \(\lambda \)-calculus for effectful computation
• A relational account of call-by-value sequentiality
• A provably correct translation of the \(\lambda \)-calculus into a mathematical model of C++
• VDM semantics of programming languages: Combinators and monads
• Programs as data structures in \(\lambda\)SF-calculus
• Comonadic notions of computation
• The proof monad
• Models for the computational \(\lambda\)-calculus
• Constructing a quasi-uniform function space
• Call-by-push-value: Decomposing call-by-value and call-by-name
• A formal abstract framework for modelling and testing complex software systems
• Kleisli morphisms and randomized congruences for the Giry monad
• Discrete Lawvere theories and computational effects
• Gabriel–Ulmer duality and Lawvere theories enriched over a general base
• The lambda-context calculus (extended version)
• Commutativity
• Some Domain Theory and Denotational Semantics in Coq
• Semantics of weakening and contraction
• On structuring functional programs with monoidal profunctors
• Classical misuse attacks on NIST round 2 PQC. The power of rank-based schemes
• A general method for proving decidability of intuitionistic modal logics
• Constructing language processors with algebra combinators
• Automata, Languages and Programming
• Lazy lambda calculus: theories, models and local structure characterization (extended abstract)
• Premonoidal categories as categories with algebraic structure
• Comparing logics for rewriting: Rewriting logic, action calculi and tile logic
• Infinite trace equivalence
• A fully abstract denotational semantics for the \(\pi\)-calculus
• Structuring operational semantics: simplification and computation
• Capsules and closures

Uses Software

• LCF

This page was built for publication: Notions of computation and monads

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q757075)