Local variable scoping and Kleene algebra with tests

DOI10.1016/J.JLAP.2007.10.007MaRDI QIDQ929964zbMATH OpenOpenAlexWikidataFDO

Authors Kamal Aboul-Hosn, Dexter Kozen

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

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

Recommendations

• Local Variable Scoping and Kleene Algebra with Tests
• Local completeness logic on Kleene algebra with tests
• Kleene algebra with tests and Coq tools for while programs
• Some variations on the notion of locally testable language
• scientific article; zbMATH DE number 431769
• From regular to strictly locally testable languages
• From regular to strictly locally testable languages
• Concurrent Kleene algebra with tests
• scientific article; zbMATH DE number 1500648
• scientific article; zbMATH DE number 3940702

Cites work

• scientific article; zbMATH DE number 431769 (Why is no real title available?)
• scientific article; zbMATH DE number 3793435 (Why is no real title available?)
• scientific article; zbMATH DE number 46740 (Why is no real title available?)
• scientific article; zbMATH DE number 1223609 (Why is no real title available?)
• scientific article; zbMATH DE number 1231510 (Why is no real title available?)
• scientific article; zbMATH DE number 1241702 (Why is no real title available?)
• scientific article; zbMATH DE number 1303727 (Why is no real title available?)
• scientific article; zbMATH DE number 1086671 (Why is no real title available?)
• scientific article; zbMATH DE number 3366846 (Why is no real title available?)
• scientific article; zbMATH DE number 4189708 (Why is no real title available?)
• A completeness theorem for Kleene algebras and the algebra of regular events
• A simple calculus for program transformation (inclusive of induction)
• Equivalence in functional languages with effects
• Foundations of Software Science and Computation Structures
• KAT-ML: an interactive theorem prover for Kleene algebra with tests
• On Hoare logic and Kleene algebra with tests
• Operational reasoning for functions with local state
• Propositional dynamic logic of regular programs
• Relational Semantics for Higher-Order Programs
• Substructural logic and partial correctness
• Unifying theories for logic programming

Cited in

(5)

• Relating two semantics of locally scoped names
• A model of context-dependent component connectors
• Algebra-coalgebra duality in Brzozowski's minimization algorithm
• Local Variable Scoping and Kleene Algebra with Tests
• Synchronous Kleene algebra

Describes a project that uses

Uses Software

• KAT-ML

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

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