Functions with local state: regularity and undecidability

DOI10.1016/J.TCS.2004.12.036MaRDI QIDQ557802zbMATH OpenOpenAlexFDO

Authors Andrzej S. Murawski

Publication date 30 June 2005

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://ora.ox.ac.uk/objects/uuid:537af42f-01ca-427e-a341-8e114caa5117

zbMATH Keywords

Model checkingAutomataGame semanticsSoftware verification

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25)

Recommendations

• Operational reasoning for functions with local state
• About the undecidability of program equivalence in finitary languages with state
• Fragments of ML decidable by nested data class memory automata
• Algorithmic games for full ground references
• Algorithmic games for full ground references

Cites work

• scientific article; zbMATH DE number 1670817 (Why is no real title available?)
• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 1223609 (Why is no real title available?)
• scientific article; zbMATH DE number 1342245 (Why is no real title available?)
• scientific article; zbMATH DE number 2110612 (Why is no real title available?)
• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• scientific article; zbMATH DE number 3311755 (Why is no real title available?)
• About the undecidability of program equivalence in finitary languages with state
• Automata, Languages and Programming
• Formal Reductions of the General Combinatorial Decision Problem
• Foundations of Software Science and Computation Structures
• Foundations of Software Science and Computational Structures
• Game theoretic analysis of call-by-value computation
• Operational reasoning for functions with local state
• Regular-language semantics for a call-by-value programming language
• The regular-language semantics of second-order idealized ALGOL
• Tools and Algorithms for the Construction and Analysis of Systems
• Visibly pushdown languages

Cited in

(14)

• Games for complexity of second-order call-by-name programs
• Contextual equivalence for state and control via nested data
• ML and extended branching VASS
• Algorithmic games for full ground references
• Algorithmic nominal game semantics
• The impact of higher-order state and control effects on local relational reasoning
• Algorithmic games for full ground references
• Fragments of ML decidable by nested data class memory automata
• Block structure vs scope extrusion: between innocence and omniscience
• Full Abstraction for Reduced ML
• Algorithmic probabilistic game semantics. Playing games with automata
• A fragment of ML decidable by visibly pushdown automata
• Syntactic control of concurrency
• Full abstraction for Reduced ML

This page was built for publication: Functions with local state: regularity and undecidability

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