Notions of Computation and Monads

Abstract The λ-calculus is considered a useful mathematical tool in the study of programming languages, since programs can be identified with λ-terms. However, if one goes further and uses βη-conversion to prove equivalence of programs, then a gross simplification is introduced (programs are identified with total functions from values to values ) that may jeopardise the applicability of theoretical results. In this paper we introduce calculi, based on a categorical semantics for computations , that provide a correct basis for proving equivalence of programs for a wide range of notions of computation .

• Publication year

  1991

• Venue

  Information and Computation

• Publication date

  1991-07-01

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1016/0890-5401(91)90052-4
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Semantic Domains

  1991cited by this paper
• New foundations for fixpoint computations

  1990cited by this paper
• Higher-order modules and the phase distinction

  1989cited by this paper
• A sound and complete axiomatization of operational equivalence of programs with memory

  1989cited by this paper
• Programming, Transforming, and Providing with Function Abstractions and Memories

  1989cited by this paper
• A category-theoretic account of program modules

  1989cited by this paper
• Linear Logic, -Autonomous Categories and Cofree Coalgebras

  1989cited by this paper
• Computational lambda-calculus and monads

  1989influential reference
• A Syntactic Theory of Sequential State

  1989cited by this paper
• The partial lambda calculus

  1988cited by this paper
• Computational foundations of basic recursive function theory

  1988cited by this paper
• The Linear Abstract Machine

  1988cited by this paper
• Verification of Programs That Destructively Manipulate Data

  1988cited by this paper
• The theory of constructions: Categorical semantics and topos-theoretic models

  1987cited by this paper
• Partial Objects In Constructive Type Theory

  1987cited by this paper
• Reasoning with Continuations

  1986cited by this paper
• Introduction to higher order categorical logic

  1986cited by this paper
• Denotational Semantics: A Methodology for Language Development

  1986cited by this paper
• Toposes, Triples and Theories

  1984cited by this paper
• Edinburgh LCF: A mechanised logic of computation

  1979cited by this paper
• Identity and existence in intuitionistic logic

  1979cited by this paper
• Edinburgh lcf: a mechanized logic of computation

  1978cited by this paper
• First order categorical logic

  1977influential reference
• Doctrines in Categorical Logic

  1977cited by this paper
• The Logic of Topoi

  1977cited by this paper
• The category-theoretic solution of recursive domain equations

  1977cited by this paper
• Call-by-Name, Call-by-Value and the lambda-Calculus

  1975influential reference
• Strong functors and monoidal monads

  1972cited by this paper
• Categories for the Working Mathematician

  1971influential reference

• Programming Backpropagation with Reverse Handlers for Arrows

  2026cites this paper
• Strongly finitary metric monads are too strong

  2026cites this paper
• Formalized Run-Time Analysis of Active Learning -- Coalgebraically in Agda

  2026cites this paper
• An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories

  2026cites this paper
• Domain-Theoretic Semantics for Functional Logic Programming

  2026cites this paper
• Profunctorial algebras

  2026cites this paper
• Strong Normalisation for Asynchronous Effects

  2026cites this paper
• Categories for collection monads

  2026cites this paper
• A taxonomy of categories for relations

  2025cites this paper
• Twin procedures, two kinds of variable binding, and two kinds of computation

  2025cites this paper
• Towards a Computational Quantum Logic: An Overview of an Ongoing Research Program

  2025cites this paper
• Calculating monad transformers with category theory

  2025cites this paper
• Distributive Laws of Monadic Containers

  2025cites this paper
• Notions of Stack-Manipulating Computation and Relative Monads

  2025cites this paper
• Classical Notions of Computation and the Hasegawa-Thielecke Theorem

  2025cites this paper
• Between Markov and restriction: Two more monads on categories for relations

  2025cites this paper
• Monad Translations for Higher-Order Logic

  2025cites this paper
• From Partial to Monadic: Combinatory Algebra with Effects

  2025influential citation
• Robust Topology and the Hausdorff-Smyth Monad on Metric Spaces over Continuous Quantales

  2025cites this paper
• Freer Arrows and Why You Need Them in Haskell

  2025cites this paper
• A simple formalization of alpha-equivalence

  2025cites this paper
• Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)

  2025cites this paper
• A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms

  2025cites this paper
• Big Steps in Higher-Order Mathematical Operational Semantics

  2025cites this paper
• Monadic type-and-effect soundness

  2025cites this paper
• Probabilistic Strategies: Definability and the Tensor Completeness Problem

  2025cites this paper
• Monadic Intersection Types, Relationally, and Ordered

  2025influential citation
• Type, Ability, and Effect Systems: Perspectives on Purity, Semantics, and Expressiveness

  2025cites this paper
• Some Consistent Power Constructions

  2025influential citation
• A Categorical Unification for Multi-Model Data: Part I Categorical Model and Normal Forms

  2025cites this paper
• The Relative Monadic Metalanguage

  2025cites this paper
• Monadic Context Engineering

  2025cites this paper
• How much is in a square? Calculating functional programs with squares

  2025cites this paper
• Correct and Abstract Semantics Lifting for Domain-Specific Language Implementation

  2025cites this paper
• Scoped Effects, Scoped Operations, and Parameterized Algebraic Theories

  2025influential citation
• Fail Faster: Staging and Fast Randomness for High-Performance PBT

  2025cites this paper
• Adequacy for Algebraic Effects Revisited

  2025cites this paper
• An effectful object calculus

  2025cites this paper
• On Circuit Description Languages, Indexed Monads, and Resource Analysis

  2025cites this paper
• Syntactic Effectful Realizability in Higher-Order Logic

  2025cites this paper
• Division algebras in monoidal categories

  2025cites this paper
• ALEA IACTA EST: A Declarative Domain-Specific Language for Manually Performable Random Experiments

  2025cites this paper
• Compositional Taylor expansion in cartesian differential categories

  2025cites this paper
• LLM-Powered, Expert-Refined Causal Loop Diagramming via Pipeline Algebra

  2025cites this paper
• Parametric Distributive Laws: uniform monad composition

  2025cites this paper
• An adequate while-language for stochastic hybrid computation

  2025cites this paper
• Quantitative Types for the Functional Machine Calculus

  2025cites this paper
• A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants

  2025cites this paper
• Lax Modal Lambda Calculi

  2025cites this paper
• Logical relations for call-by-push-value models, via internal fibrations in a 2-category

  2025influential citation
• The Hidden Strength of Costrong Functors

  2025influential citation
• Realizability Models and Complexity Classes

  2025cites this paper
• Hyperintensions as Computations

  2025cites this paper
• Metric Equational Theories

  2025cites this paper
• Demystifying Codensity Monads via Duality

  2025cites this paper
• Interpretando Efeitos Algébricos por Meio de Mônadas

  2025influential citation
• Strong Dinatural Transformations and Generalised Codensity Monads

  2025influential citation
• The Functional Machine Calculus III: Control

  2025cites this paper
• CoreDPPL: Towards a Sound Composition of Differentiation, ODE Solving, and Probabilistic Programming

  2025cites this paper
• Zippy - Generic White-Box Proof Search with Zippers

  2025influential citation
• A quantitative approach to global state composition

  2025cites this paper
• Linear effects, exceptions, and resource safety: a Curry-Howard correspondence for destructors

  2025cites this paper
• Time Aware Compilation Verified: A Category-Theoretic Approach in Rocq

  2025cites this paper
• Functional Reactive Programming with Effects, A More Permissive Approach

  2025cites this paper
• Two-sorted algebraic decompositions of Brookes's shared-state denotational semantics

  2025cites this paper
• A Brookes-Style Denotational Semantics for Release/Acquire Concurrency

  2025cites this paper
• Algebraic Effect Handlers with Bidirectional Type-Checking

  2024cites this paper
• Algebraic Language Theory with Effects

  2024cites this paper
• If cheating is optimisation then assessment must not be pure

  2024cites this paper
• Abstract Operational Methods for Call-by-Push-Value

  2024cites this paper
• Arity Hierarchies for Quantifiers Closed Under Partial Polymorphisms

  2024cites this paper
• The Functional Machine Calculus III: Choice (Early Announcement)

  2024cites this paper
• A Simple Formal Language for Probabilistic Decision Problems

  2024cites this paper
• Semantics Lifting for Syntactic Sugar

  2024cites this paper
• A Low-Level Look at A-Normal Form

  2024cites this paper
• On the Soundness of Auto-completion Services for Dynamically Typed Languages

  2024cites this paper
• Di- is for Directed: First-Order Directed Type Theory via Dinaturality

  2024cites this paper
• The Maquette Monad

  2024cites this paper
• Comodule Representations of Second-Order Functionals

  2024cites this paper
• Beyond Monads and Biproducts: A Uniform Interpretation of Parallelism in Intuitionistic Logic

  2024cites this paper
• Algebraic effects and handlers for arrows

  2024cites this paper
• Fibrations of algebras

  2024influential citation
• Effectful Mealy Machines: Bisimulation and Trace

  2024cites this paper
• A computational method for left-adjointness

  2024cites this paper
• The Relational Machine Calculus

  2024cites this paper
• Meaningfulness and Genericity in a Subsuming Framework

  2024cites this paper
• Numerical Fuzz: A Type System for Rounding Error Analysis

  2024cites this paper
• A Denotational Approach to Release/Acquire Concurrency

  2024cites this paper
• Correspondence between Composite Theories and Distributive Laws

  2024cites this paper
• A Cartesian Closed Category for Random Variables

  2024cites this paper
• A Generalized Theory of Interactions -- I. The General Problem

  2024cites this paper
• Abstracting Effect Systems for Algebraic Effect Handlers

  2024cites this paper
• Compositional Semantics for Shared-Variable Concurrency

  2024cites this paper
• Compositional Imprecise Probability: A Solution from Graded Monads and Markov Categories

  2024influential citation
• Asymptotic speedup via effect handlers

  2024cites this paper
• Monadic Intersection Types, Relationally (Extended Version)

  2024cites this paper
• A Unifying Categorical View of Nondeterministic Iteration and Tests

  2024cites this paper
• Extending the Quantitative Pattern-Matching Paradigm

  2024cites this paper
• A Categorical Approach to DIBI Models

  2024cites this paper
• Algebraic Effects Meet Hoare Logic in Cubical Agda

  2024cites this paper