Streams of approximations, equivalence of recursive effectful programs

DOI10.1007/978-3-031-16912-0_8MaRDI QIDQ6109211

Niccolò Veltri, Niels Voorneveld

Publication date: 30 June 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

zbMATH Keywords

algebraic effectsAgdaprogram equivalencecall-by-push-value

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Call-by-push-value: Decomposing call-by-value and call-by-name
• Domain theory in logical form
• The revised report on the syntactic theories of sequential control and state
• LCF considered as a programming language
• Fully abstract models of typed \(\lambda\)-calculi
• A syntactic approach to type soundness
• Modelling environments in call-by-value programming languages.
• Fixpoint semantics and simulation
• The delay monad and restriction categories
• On full abstraction for PCF: I, II and III
• Behavioural equivalence via modalities for algebraic effects
• Stateful runners of effectful computations
• Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda
• Guarded Dependent Type Theory with Coinductive Types
• Handling Algebraic Effects
• Partiality, Revisited
• Similarity Quotients as Final Coalgebras
• A Powerdomain Construction
• Quotienting the delay monad by weak bisimilarity
• Continuous Lattices and Domains
• General Recursion via Coinductive Types

This page was built for publication: Streams of approximations, equivalence of recursive effectful programs