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)

• 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
• \(\gamma\) \(\omega\)-calculus semantics of functional programming language FFP
• Regular-language semantics for a call-by-value programming language
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• On theorem prover-based testing
• Domain semantics of possibility computations
• Game semantics for access control
• Title not available (Why is that?)
• Families of symmetries as efficient models of resource binding
• Full abstraction for non-deterministic and probabilistic extensions of PCF. I: The angelic cases
• Cut-free Gentzen calculus for multimodal CK
• A first-order one-pass CPS transformation
• The Arrow Calculus as a Quantum Programming Language
• New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic
• Modes of adjointness
• Coalgebras in functional programming and type theory
• Adjunction models for call-by-push-value with stacks
• The untyped computational \(\lambda \)-calculus and its intersection type discipline
• An equational notion of lifting monad
• Stable power domains
• Semantics for algebraic operations
• Substitution: A formal methods case study using monads and transformations
• Principles of programming with complex objects and collection types
• Embedding constructive K into intuitionistic K
• A graphical approach to monad compositions
• A typed, algebraic, computational lambda-calculus
• Tensors of comodels and models for operational semantics
• Monads and Quantitative Equational Theories for Nondeterminism and Probability
• Continuation passing style for effect handlers
• Local algebraic effect theories
• Flag-based big-step semantics
• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
• Title not available (Why is that?)
• 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

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)