Unifying Theories of Programming in Isabelle

DOI10.1007/978-3-642-39721-9_3zbMath1444.68049OpenAlexW63036761MaRDI QIDQ2948230

Simon Foster, J. C. P. Woodcock

Publication date: 30 September 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://eprints.whiterose.ac.uk/94531/1/utp_in_isabelle.pdf

zbMATH Keywords

denotational semanticsinteractive theorem provingIsabellelaws of programmingunifying theories of programming (UTP)

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

A UTP semantics for communicating processes with shared variables and its formal encoding in PVS ⋮ Isabelle/UTP: A Mechanised Theory Engineering Framework

Uses Software

• Isabelle
• Nitpick
• Isabelle/HOL
• VAMPIRE
• SPASS
• z3
• ProofPower
• Sledgehammer
• Z
• Handel-C
• Isabelle/Circus
• Waldmeister
• Circus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A theoretical basis for stepwise refinement and the programming calculus
• A UTP semantics for \textsf{Circus}
• Unifying theories in ProofPower-Z
• Generating Denotational Semantics from Algebraic Semantics for Event-Driven System-Level Language
• Automatic Proof and Disproof in Isabelle/HOL
• Circus Time with Reactive Designs
• UTP Semantics for Handel-C
• Component Publications and Compositions
• The B-Book
• Refinement Calculus
• Retrospective and Prospective for Unifying Theories of Programming
• Mathematics of Program Construction
• A Theory of Pointers for the UTP
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
• Integrated Formal Methods

This page was built for publication: Unifying Theories of Programming in Isabelle