Inductive and coinductive predicate liftings for effectful programs

DOI10.4204/EPTCS.351.16MaRDI QIDQ6653761zbMATH OpenFDO

Authors Niccolò Veltri, Niels Voorneveld

Publication date 17 December 2024

Full work available at URL https://doi.org/10.4204/EPTCS.351.16

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Cites work

• A model of PCF in guarded type theory
• A sound and complete logic for algebraic effects
• Coinductive big-step operational semantics
• Containers: Constructing strictly positive types
• Copatterns, programming infinite structures by observations
• Effectful applicative bisimilarity: monads, relators, and Howe's method
• General Recursion via Coinductive Types
• Generic weakest precondition semantics from monads enriched with order
• Handling algebraic effects
• scientific article; zbMATH DE number 1705158 (Why is no real title available?)
• scientific article; zbMATH DE number 2090728 (Why is no real title available?)
• LCF considered as a programming language
• Modelling environments in call-by-value programming languages.
• Notions of computation and monads
• Partiality, Revisited
• Proving congruence of bisimulation in functional programming languages
• Quotienting the delay monad by weak bisimilarity
• Similarity quotients as final coalgebras
• Some Domain Theory and Denotational Semantics in Coq

Cited in

(2)

• What monads can and cannot do with a bit of extra time
• What monads can and cannot do with a few extra pages

This page was built for publication: Inductive and coinductive predicate liftings for effectful programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6653761)