Inductive and coinductive predicate liftings for effectful programs

DOI10.4204/eptcs.351.16MaRDI QIDQ6653761

Niccolò Veltri, Niels Voorneveld

Publication date: 17 December 2024

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Notions of computation and monads
• Generic weakest precondition semantics from monads enriched with order
• Coinductive big-step operational semantics
• LCF considered as a programming language
• Modelling environments in call-by-value programming languages.
• Proving congruence of bisimulation in functional programming languages
• A sound and complete logic for algebraic effects
• Containers: Constructing strictly positive types
• Handling Algebraic Effects
• Copatterns
• Partiality, Revisited
• Similarity Quotients as Final Coalgebras
• Some Domain Theory and Denotational Semantics in Coq
• Quotienting the delay monad by weak bisimilarity
• General Recursion via Coinductive Types
• A model of PCF in guarded type theory

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