Automated temporal verification for algebraic effects

DOI10.1007/978-3-031-21037-2_5zbMATH Open1524.68103OpenAlexW4312688668MaRDI QIDQ6176569FDOQ6176569

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

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

Mathematics Subject Classification ID

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

Cites Work

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

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)