Local variable scoping and Kleene algebra with tests

DOI10.1016/J.JLAP.2007.10.007zbMath1148.68033OpenAlexW2038553844WikidataQ114851555 ScholiaQ114851555MaRDI QIDQ929964

Dexter Kozen, Kamal Aboul-Hosn

Publication date: 19 June 2008

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2007.10.007

zbMATH Keywords

program verificationKleene algebraKleene algebra with testsprogramming with statevariable scoping

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

A model of context-dependent component connectors ⋮ Algebra-coalgebra duality in brzozowski's minimization algorithm ⋮ Synchronous Kleene algebra

Uses Software

• KAT-ML

Cites Work

• A simple calculus for program transformation (inclusive of induction)
• Propositional dynamic logic of regular programs
• A completeness theorem for Kleene algebras and the algebra of regular events
• Relational Semantics for Higher-Order Programs
• KAT-ML: an interactive theorem prover for Kleene algebra with tests
• Equivalence in functional languages with effects
• Substructural logic and partial correctness
• Foundations of Software Science and Computation Structures
• On Hoare logic and Kleene algebra with tests
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Local variable scoping and Kleene algebra with tests