Streams of approximations, equivalence of recursive effectful programs

DOI10.1007/978-3-031-16912-0_8MaRDI QIDQ6109211zbMATH OpenFDO

Authors Niccolò Veltri, Niels Voorneveld

Publication date 30 June 2023

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

Full work available at URL https://doi.org/10.1007/978-3-031-16912-0_8

zbMATH Keywords

Agdaalgebraic effectscall-by-push-valueprogram equivalence

Mathematics Subject Classification ID

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

Cites work

• A Powerdomain Construction
• A syntactic approach to type soundness
• Behavioural equivalence via modalities for algebraic effects
• Call-by-push-value: Decomposing call-by-value and call-by-name
• Continuous Lattices and Domains
• Domain theory in logical form
• Effectful applicative bisimilarity: monads, relators, and Howe's method
• Fixpoint semantics and simulation
• Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda
• Fully abstract models of typed \(\lambda\)-calculi
• General Recursion via Coinductive Types
• Guarded dependent type theory with coinductive types
• Guarded recursion in Agda via sized types
• Handling algebraic effects
• scientific article; zbMATH DE number 1705158 (Why is no real title available?)
• LCF considered as a programming language
• Modelling environments in call-by-value programming languages.
• On full abstraction for PCF: I, II and III
• Partiality, Revisited
• Quotienting the delay monad by weak bisimilarity
• Similarity quotients as final coalgebras
• Stateful runners of effectful computations
• The clocks are ticking: no more delays!: Reduction semantics for type theory with guarded recursion
• The delay monad and restriction categories
• The revised report on the syntactic theories of sequential control and state

Cited in

(3)

• Characterizing polynomial time complexity of stream programs using interpretations
• On the complexity of stream equality
• PSEUDO: applications of streams and lazy evaluation to integrable models

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

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