Notions of computation and monads

DOI10.1016/0890-5401(91)90052-4zbMath0723.68073OpenAlexW1997143185WikidataQ55895577 ScholiaQ55895577MaRDI QIDQ757075

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

zbMATH Keywords

monads proving equivalence of programs categorical semantics for computations

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Normalization by evaluation and algebraic effects, Monads for behaviour, Extending separation logic with fixpoints and postponed substitution, Evolution of rule-based programs, Freyd categories are enriched Lawvere theories, The coinductive resumption monad, Introducing \(\llparenthesis\lambda\rrparenthesis\), a \(\lambda \)-calculus for effectful computation, A theory of bisimulation for a fragment of concurrent ML with local names, Semantics of weakening and contraction, A first-order one-pass CPS transformation, On the call-by-value CPS transform and its semantics, Stable power domains, Strong normalization from weak normalization in typed \(\lambda\)-calculi, About permutation algebras, (pre)sheaves and named sets, Constructing a quasi-uniform function space, Call-by-push-value: Decomposing call-by-value and call-by-name, Eilenberg--Moore algebras for stochastic relations, Generic models for computational effects, Discrete Lawvere theories and computational effects, Semantics of higher-order quantum computation via geometry of interaction, Combining control effects and their models: game semantics for a hierarchy of static, dynamic and delimited control effects, Propositional lax logic, Query languages for bags and aggregate functions, Combining algebraic effects with continuations, On the relations between monadic semantics, Constructing language processors with algebra combinators, Bundle functors and fibrations, Full abstraction for Reduced ML, A coinductive calculus for asynchronous side-effecting processes, A first order logic of effects, Programming from metaphorisms, Monad transformers as monoid transformers, Continuity spaces: Reconciling domains and metric spaces, Monad as modality, Generic weakest precondition semantics from monads enriched with order, Dijkstra and Hoare monads in monadic computation, Lewis meets Brouwer: constructive strict implication, Algebraic properties of stochastic effectivity functions, An equational notion of lifting monad, A new framework for declarative programming, A fully abstract model for the \(\pi\)-calculus., Commutativity, Cartesian effect categories are Freyd-categories, Resource modalities in tensor logic, Coalgebras in functional programming and type theory, Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control, A relational realizability model for higher-order stateful ADTs, The Cooper storage idiom, Constructive Boolean circuits and the exactness of timed ternary simulation, Mathematical modal logic: A view of its evolution, Game-theoretic analysis of call-by-value computation, Program equivalence in a simple language with state, Proofs of randomized algorithms in Coq, Modelling environments in call-by-value programming languages., On theorem prover-based testing, Full abstraction for non-deterministic and probabilistic extensions of PCF. I: The angelic cases, Gabriel-Morita theory for excisive model categories, Modes of adjointness, Observationally-induced lower and upper powerspace constructions, Principles of programming with complex objects and collection types, A monad for randomized algorithms, Complete Elgot monads and coalgebraic resumptions, Fibrational modal type theory, New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic, The Giry monad is not strong for the canonical symmetric monoidal closed structure on \textbf {Meas}, Flag-based big-step semantics, A theory of binding structures and applications to rewriting, A domain model characterising strong normalisation, Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code, Comparing free algebras in topological and classical domain theory, Modules over monads and initial semantics, VDM semantics of programming languages: Combinators and monads, A generic complete dynamic logic for reasoning about purity and effects, The proof monad, Game semantics and linear CPS interpretation, Eager and delayed contract monitoring for call-by-value and call-by-name evaluation, A formal abstract framework for modelling and testing complex software systems, The order-sobrification monad, Kleisli morphisms and randomized congruences for the Giry monad, Predicate liftings and functor presentations in coalgebraic expression languages, Monoidal computer III: a coalgebraic view of computability and complexity (extended abstract), HasCasl: integrated higher-order specification and program development, Datatype-generic termination proofs, A provably correct translation of the \(\lambda \)-calculus into a mathematical model of C++, Full abstractness for a functional/concurrent language with higher-order value-passing, Simply-typed underdeterminism, Cut-free Gentzen calculus for multimodal CK, Domain semantics of possibility computations, On the algebraic structure of declarative programming languages, A behavioural theory of first-order CML, Swinging types=functions+relations+transition systems, CPS transformation of beta-redexes, The lambda-context calculus (extended version), Coalgebras and monads in the semantics of Java, Combining a monad and a comonad, A fully abstract denotational semantics for the \(\pi\)-calculus, Lifting results for categories of algebras, Premonoidal categories as categories with algebraic structure, Comparing logics for rewriting: Rewriting logic, action calculi and tile logic, Taut monads and \(T0\)-spaces., LF+ in Coq for "fast and loose" reasoning, Modalities in homotopy type theory, Semantics of value recursion for Monadic Input/Output, Adjoint Logic with a 2-Category of Modes, Runners in Action, Monads, indexes and transformations, Unnamed Item, Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages, Synthetic topology in Homotopy Type Theory for probabilistic programming, Partiality and Container Monads, The costructure–cosemantics adjunction for comodels for computational effects, String diagram rewrite theory II: Rewriting with symmetric monoidal structure, Convexity via Weak Distributive Laws, Unnamed Item, Finitary monads on the category of posets, Quotienting the delay monad by weak bisimilarity, Finitely Presentable Algebras For Finitary Monads, Metric monads, The geometry of Bayesian programming, Unnamed Item, Game theoretic analysis of call-by-value computation, Partial hyperdoctrines: categorical models for partial function logic and Hoare logic, Computation semantics of the functional scientific workflow language Cuneiform, Contributions to a computational theory of policy advice and avoidability, Ambiguity and Incomplete Information in Categorical Models of Language, Total and Partial Computation in Categorical Quantum Foundations, Formal categorical reasoning, The linear-non-linear substitution 2-monad, How to prove decidability of equational theories with second-order computation analyser SOL, Constructive forcing, CPS translations and witness extraction in Interactive realizability, Local algebraic effect theories, Interleaving data and effects, Correctness of compiling polymorphism to dynamic typing, Sequential real number computation and recursive relations, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Sound and complete axiomatisations of call-by-value control operators, Notions of computation as monoids, Unnamed Item, Logical relations for monadic types, Transactional events, Hoare type theory, polymorphism and separation, Selection functions, bar recursion and backward induction, Codensity Lifting of Monads and its Dual, Regular-Language Semantics for a Call-by-Value Programming Language, Pseudo-commutative Monads, Semantics for Algebraic Operations, A typed, algebraic, computational lambda-calculus, What is a Categorical Model of Arrows?, Idioms are Oblivious, Arrows are Meticulous, Monads are Promiscuous, Sequential Real Number Computation and Recursive Relations, Causal commutative arrows, Operational Properties of Lily, a Polymorphic Linear Lambda Calculus with Recursion, Presheaf Models of Quantum Computation: An Outline, A graphical approach to monad compositions, A Superposition Operator for the Refinement of Algebraic Models, Models for the computational λ-calculus, Coherence for monoidal endofunctors, Coherence for monoidal monads and comonads, Realisability semantics of parametric polymorphism, general references and recursive types, A Calculus for Game-Based Security Proofs, The arrow calculus, Unnamed Item, Coherence of subsumption for monadic types, Full Abstraction for Reduced ML, Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types, Unnamed Item, Relating Structure and Power: Comonadic Semantics for Computational Resources, Strong functors on many-sorted sets, Unnamed Item, Weakest preconditions in fibrations, The Computational SLR: A Logic for Reasoning about Computational Indistinguishability, Monads and Quantitative Equational Theories for Nondeterminism and Probability, Monadic Translation of Intuitionistic Sequent Calculus, The Arrow Calculus as a Quantum Programming Language, THE HERBRAND FUNCTIONAL INTERPRETATION OF THE DOUBLE NEGATION SHIFT, Gabriel–Ulmer duality and Lawvere theories enriched over a general base, Parameterised notions of computation, The essence of the <scp>Iterator</scp> pattern, Traced Premonoidal Categories, Unnamed Item, Enriching an Effect Calculus with Linear Types, Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages, Dynamic game semantics, Unnamed Item, Continuation passing style for effect handlers, PROLOG'S CONTROL CONSTRUCTS IN A FUNCTIONAL SETTING — AXIOMS AND IMPLEMENTATION, Unnamed Item, Encoding FIX in Object Calculi, Unnamed Item, Amb Breaks Well-Pointedness, Ground Amb Doesn't, Taut Monads, Dynamic Logic and Determinism, Relational Parametricity for Control Considered as a Computational Effect, From curves to currents, Gradual type theory, A type- and scope-safe universe of syntaxes with binding: their semantics and proofs, The parametric continuation monad, Algebras for Parameterised Monads, Kleene Monads: Handling Iteration in a Framework of Generic Effects, Complete Iterativity for Algebras with Effects, Coalgebraic Components in a Many-Sorted Microcosm, A Semantical Approach to Equilibria and Rationality, Uniqueness logic, The effects of effects on constructivism, Quantitative logics for equivalence of effectful programs, Weakest preconditions in fibrations, Equational logic and categorical semantics for multi-languages, Parametrized fixed points and their applications to session types, Initial algebras and final coalgebras consisting of nondeterministic finite trace strategies, Iterated covariant powerset is not a monad, Continuity as a computational effect, Probabilistic operational semantics for the lambda calculus, Lawvere theories enriched over a general base, A Nominal Relational Model for Local Store, Observationally-induced Effects in Cartesian Closed Categories, A Simply Typed λ-Calculus of Forward Automatic Differentiation, A duality between exceptions and states, Some Domain Theory and Denotational Semantics in Coq, Logic in Access Control (Tutorial Notes), Embedding Constructive K into Intuitionistic K, Generalized arrays for Stainless frames, Comprehending Ringads, Categorifying Computations into Components via Arrows as Profunctors, Families of Symmetries as Efficient Models of Resource Binding, Accessibility and presentability in 2-categories, Program logic for higher-order probabilistic programs in Isabelle/HOL, Implication via spacetime, Notions of Bidirectional Computation and Entangled State Monads, Turing-Completeness Totally Free, A (co)algebraic theory of succinct automata, Interpreting Localized Computational Effects Using Operators of Higher Type, C-system of a module over a \(Jf\)-relative monad, A System F with Call-by-Name Exceptions, Monad compositions II: Kleisli strength, Asymptotic Improvement of Computations over Free Monads, No-iteration mixed distributive laws, Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism, Mac Lane's comparison theorem for the Kleisli construction formalized in Coq, The untyped computational \(\lambda \)-calculus and its intersection type discipline, Unnamed Item, Equational Theories of Abnormal Termination Based on Kleene Algebra, Safe functional systems through integrity types and verified assembly, Unifying Guarded and Unguarded Iteration, Commutative Semantics for Probabilistic Programming, Powersets of terms and composite monads, Classical misuse attacks on NIST round 2 PQC. The power of rank-based schemes, Domain-Freeλµ-Calculus, Combining semilattices and semimodules, A general semantic construction of dependent refinement type systems, categorically, Graded Hoare logic and its categorical semantics, Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs, A novel formal approach to program slicing, Traces for coalgebraic components, A static simulation of dynamic delimited control, Structural recursion with locally scoped names, Free-algebra models for the \(\pi \)-calculus, Infinite trace equivalence, Roles, stacks, histories: A triple for Hoare, Elements of a theory of algebraic theories, Cryptographic logical relations, On the unity of duality, Combining effects: sum and tensor, Boolean restriction categories and taut monads, Weak bisimulations for the Giry monad, The computational SLR: a logic for reasoning about computational indistinguishability, A relational account of call-by-value sequentiality, A general method for proving decidability of intuitionistic modal logics, A computational treatment of anaphora and its algorithmic implementation, Whither semantics?, Game Semantics for Access Control, Categories of Timed Stochastic Relations, Two Cotensors in One: Presentations of Algebraic Theories for Local State and Fresh Names, Stateful runners of effectful computations, Dependent Types and Fibred Computational Effects, A Coinductive Calculus for Asynchronous Side-Effecting Processes, Connected monads weakly preserve products, Formal ball monads, Introducing a Calculus of Effects and Handlers for Natural Language Semantics, GS·Λ Theories, Adjunction Models For Call-By-Push-Value With Stacks, On a monadic semantics for freshness, A functional correspondence between monadic evaluators and abstract machines for languages with computational effects, Noninterference in a predicative polymorphic calculus for access control, Trace semantics via determinization, Formal security proofs with minimal fuss: implicit computational complexity at work, Access Control in a Core Calculus of Dependency, A Convenient Category of Domains, The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads, Structuring Operational Semantics: Simplification and Computation, Coalgebraic semantics for nominal automata, Algebraic presentation of semifree monads, Program equivalence in linear contexts, Quantum Arrows in Haskell, A Rewriting Logic Approach to Operational Semantics (Extended Abstract), Specifying Properties of Concurrent Computations in CLF, Comonadic Notions of Computation, Delimited control and computational effects, Stream processors and comodels, Lifting theorems for Kleisli categories, Probabilistic power domains, information systems, and locales, On the transformation between direct and continuation semantics, From gs-monoidal to oplax cartesian categories: constructions and functorial completeness, The expressive power of Structural Operational Semantics with explicit assumptions, A formal logic for formal category theory, From semantics to types: the case of the imperative \(\lambda\)-calculus, Flexibly graded monads and graded algebras, Hypernormalisation in an abstract setting, Monadic augment and generalised short cut fusion, Plethysms and operads, Divergences on monads for relational program logics, Promonads and String Diagrams for Effectful Categories, Galois connecting call-by-value and call-by-name, Protocol choice and iteration for the free cornering, Distributive laws for relative monads, Runners for interleaving algebraic effects, A dependent dependency calculus, Structured handling of scoped effects, Duoidally enriched Freyd categories, \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic, An algebraic theory for shared-state concurrency, Interactive programming in Agda – Objects and graphical user interfaces, No value restriction is needed for algebraic effects and handlers, Unnamed Item, Unguarded recursion on coinductive resumptions, Reversible monadic computing, Healthiness conditions for predicate transformers, Unnamed Item, Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot, Monadic translation of classical sequent calculus, A Categorical Model of the Fusion Calculus, Tensors of Comodels and Models for Operational Semantics, Towards Effects in Mathematical Operational Semantics, Observationally-induced Effect Monads: Upper and Lower Powerspace Constructions, Capsules and Closures, Partiality and recursion in interactive theorem provers – an overview, A monadic framework for delimited continuations, On one-pass CPS transformations, Fusion of recursive programs with computational effects, On the ubiquity of certain total type structures, Unnamed Item, On reduction and normalization in the computational core

Uses Software

LCF

Cites Work