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)

• A domain model characterising strong normalisation
• Title not available (Why is that?)
• Correctness of compiling polymorphism to dynamic typing
• On one-pass CPS transformations
• Comparing free algebras in topological and classical domain theory
• On equation systems in monotonic models of typed \(\lambda\)-calculus
• Gabriel-Morita theory for excisive model categories
• A generic complete dynamic logic for reasoning about purity and effects
• Title not available (Why is that?)
• The transformation calculus
• Operational properties of \texttt{Lily}, a polymorphic linear lambda calculus with recursion
• Full abstractness for a functional/concurrent language with higher-order value-passing
• Sound and complete axiomatisations of call-by-value control operators
• A monad for randomized algorithms
• Contributions to a computational theory of policy advice and avoidability
• Algebras for parameterised monads
• Simply-typed underdeterminism
• Query languages for bags and aggregate functions
• A behavioural theory of first-order CML
• Parameterised notions of computation
• Title not available (Why is that?)
• Kan extensions for program optimisation Or: Art and Dan explain an old trick
• Continuity as a computational effect
• Datatype-generic termination proofs
• Dijkstra and Hoare monads in monadic computation
• Generic weakest precondition semantics from monads enriched with order
• Formal categorical reasoning
• A Calculus for Game-Based Security Proofs
• Formal security proofs with minimal fuss: implicit computational complexity at work
• Modules over monads and initial semantics
• Distributive laws for relative monads
• Presheaf models of quantum computation: an outline
• Pseudo-commutative monads
• Bundle functors and fibrations
• On the call-by-value CPS transform and its semantics
• Lifting results for categories of algebras
• CPS transformation of beta-redexes
• Whither semantics?
• Programming from metaphorisms
• An algebraic theory for shared-state concurrency
• Lewis meets Brouwer: constructive strict implication
• Total and partial computation in categorical quantum foundations
• Modalities in homotopy type theory
• Idioms are oblivious, arrows are meticulous, monads are promiscuous
• Asymptotic Improvement of Computations over Free Monads
• The Herbrand functional interpretation of the double negation shift
• The Computational SLR: A Logic for Reasoning about Computational Indistinguishability
• A computational treatment of anaphora and its algorithmic implementation
• Monads, indexes and transformations
• Monadic augment and generalised short cut fusion
• Game semantics and linear CPS interpretation
• The Cooper storage idiom
• 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

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)