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 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

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)