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
• A coinductive calculus for asynchronous side-effecting processes
• Monad transformers as monoid transformers
• Dijkstra Monads in Monadic Computation
• Propositional lax logic
• Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
• Title not available (Why is that?)
• Normalization by evaluation and algebraic effects
• Monads for behaviour
• Algebraic properties of stochastic effectivity functions
• Title not available (Why is that?)
• On the relations between monadic semantics
• Logical relations for monadic types
• Resource modalities in tensor logic
• Lifting theorems for Kleisli categories
• A first order logic of effects
• Comprehending monads
• Observationally-induced lower and upper powerspace constructions
• Specifying properties of concurrent computations in CLF
• Freyd categories are enriched Lawvere theories
• Towards a notion of lambda monoid
• The coinductive resumption monad
• Program equivalence in linear contexts
• A fully abstract model for the \(\pi\)-calculus.
• A coinductive calculus for asynchronous side-effecting processes
• A monadic framework for delimited continuations
• Combining algebraic effects with continuations
• Game-theoretic analysis of call-by-value computation
• Kleene monads: handling iteration in a framework of generic effects
• Complete iterativity for algebras with effects
• Modelling environments in call-by-value programming languages.
• Coalgebras and monads in the semantics of Java
• On the ubiquity of certain total type structures
• Generic models for computational effects
• On the algebraic structure of declarative programming languages
• A relational realizability model for higher-order stateful ADTs
• Duoidally enriched Freyd categories
• Continuity spaces: Reconciling domains and metric spaces
• Extending separation logic with fixpoints and postponed substitution
• A categorical model of the fusion calculus
• Constructive Boolean circuits and the exactness of timed ternary simulation

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)