Automated temporal verification for algebraic effects

DOI10.1007/978-3-031-21037-2_5MaRDI QIDQ6176569zbMATH OpenOpenAlexFDO

Authors Yahui Song, Darius Foo, Wei-Ngan Chin

Publication date 25 July 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://zenodo.org/record/7009119

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Modular verification of programs with effects and effects handlers
• An effect system for algebraic effects and handlers
• A synchronous effects logic for temporal verification of pure Esterel
• A fixpoint logic and dependent effects for temporal property verification
• Programming with algebraic effects and handlers

Cites work

• A fixpoint logic and dependent effects for temporal property verification
• A generalization of jumps and labels
• A Hoare logic for the coinductive trace-based big-step semantics of While
• A synchronous effects logic for temporal verification of pure Esterel
• Abstract interpretation from Büchi automata
• ANTIMIROV AND MOSSES'S REWRITE SYSTEM REVISITED
• Automated Reasoning with Analytic Tableaux and Related Methods
• Contextual effects for version-consistent dynamic software updating and safe concurrent programming
• Do be do be do
• Doo bee doo bee doo
• Effect handlers via generalised continuations
• Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala
• Handlers in action
• Inferring algebraic effects
• Koka: programming with row polymorphic effect types
• Local temporal reasoning
• Partial derivatives of regular expressions and finite automata constructions
• Programming Languages and Systems
• Programming with algebraic effects and handlers
• Regular Linear Temporal Logic
• Resource usage verification.
• Rewriting extended regular expressions
• Rewriting regular inequalities
• Shallow effect handlers
• Symbolic solving of extended regular expression inequalities
• The inclusion problem for regular expressions
• The type and effect discipline
• Trace-based verification of imperative programs with I/O
• Type and behaviour reconstruction for higher-order concurrent programs
• Type directed compilation of row-typed algebraic effects
• Types and trace effects of higher order programs

This page was built for publication: Automated temporal verification for algebraic effects

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