Program equivalence in a simple language with state
From MaRDI portal
game semanticslogical relationsenvironmental bisimulationshigher-order computation and local statenominal computationprogram equivalence
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Recommendations
- The impact of higher-order state and control effects on local relational reasoning
- The impact of higher-order state and control effects on local relational reasoning
- Operational reasoning for functions with local state
- Relational Semantics for Higher-Order Programs
- Program equivalence in linear contexts
Cites work
- scientific article; zbMATH DE number 1670817 (Why is no real title available?)
- scientific article; zbMATH DE number 431771 (Why is no real title available?)
- scientific article; zbMATH DE number 3688686 (Why is no real title available?)
- A bisimulation for dynamic sealing
- A bisimulation for type abstraction and recursion
- A fragment of ML decidable by visibly pushdown automata
- A game semantics of names and pointers
- A new approach to abstract syntax with variable binding
- A theory of bisimulation for a fragment of concurrent ML with local names
- Algorithmic nominal game semantics
- Computer Science Logic
- Finitary PCF is not decidable
- Finite state machines for strings over infinite alphabets
- Foundations of Software Science and Computation Structures
- Fresh-register automata
- From applicative to environmental bisimulation
- Full Abstraction for Reduced ML
- Full abstraction for PCF
- Full abstraction for nominal general references
- Game Semantics for Higher-Order Concurrency
- Game-theoretic analysis of call-by-value computation
- Intensional interpretations of functionals of finite type I
- Introduction to categories and categorical logic
- Kripke logical relations and PCF
- Logical relations for monadic types
- Notions of computation and monads
- On full abstraction for PCF: I, II and III
- Operational reasoning for functions with local state
- Programming Languages and Systems
- Realisability semantics of parametric polymorphism, general references and recursive types
- Small bisimulations for reasoning about higher-order imperative programs
- State-dependent representation independence
- The \(\pi\)-calculus: A theory of mobile processes
- The impact of higher-order state and control effects on local relational reasoning
- Untyped lambda-calculus with input-output
Cited in
(6)- A language-independent proof system for full program equivalence
- Modular verification of procedure equivalence in the presence of memory allocation
- Denotational semantics with nominal Scott domains
- Program equivalence in linear contexts
- From bounded checking to verification of equivalence via symbolic up-to techniques
- Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts
This page was built for publication: Program equivalence in a simple language with state
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q456473)
