Functions with local state: regularity and undecidability

DOI10.1016/J.TCS.2004.12.036zbMATH Open1108.68076OpenAlexW2011823280MaRDI QIDQ557802FDOQ557802

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

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

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)

Cites Work

• Title not available (Why is that?)
• Formal Reductions of the General Combinatorial Decision Problem
• Visibly pushdown languages
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Operational reasoning for functions with local state
• Foundations of Software Science and Computation Structures
• Title not available (Why is that?)
• The regular-language semantics of second-order idealized ALGOL
• Game theoretic analysis of call-by-value computation
• Title not available (Why is that?)
• Regular-Language Semantics for a Call-by-Value Programming Language
• About the undecidability of program equivalence in finitary languages with state
• Tools and Algorithms for the Construction and Analysis of Systems
• Automata, Languages and Programming
• Foundations of Software Science and Computational Structures

Cited In (11)

• A Fragment of ML Decidable by Visibly Pushdown Automata
• ML and Extended Branching VASS
• The impact of higher-order state and control effects on local relational reasoning
• Algorithmic games for full ground references
• Algorithmic Nominal Game Semantics
• Block structure vs scope extrusion: between innocence and omniscience
• Full Abstraction for Reduced ML
• Algorithmic probabilistic game semantics. Playing games with automata
• Syntactic control of concurrency
• Full abstraction for Reduced ML
• Games for complexity of second-order call-by-name programs

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)