### Abstract

Isabelle/UTP is a mechanised theory engineering toolkit based on Hoare and He’s Unifying Theories of Programming (UTP). UTP enables the creation of denotational, algebraic, and operational semantics for different programming languages using an alphabetised relational calculus. We provide a semantic embedding of the alphabetised relational calculus in Isabelle/HOL, including new type definitions, relational constructors, automated proof tactics, and accompanying algebraic laws. Isabelle/UTP can be used to both capture laws of programming for different languages, and put these fundamental theorems to work in the creation of associated verification tools, using calculi like Hoare logics. This document describes the relational core of the UTP in Isabelle/HOL.

### License

BSD License

### Topics

- Computer science/Programming languages/Logics

### Session UTP-Toolkit

- List_Extra
- Sequence
- FSet_Extra
- Countable_Set_Extra
- Map_Extra
- List_Lexord_Alt
- Partial_Fun
- Finite_Fun
- Infinity
- Positive
- Total_Recall
- utp_toolkit

### Session UTP

- utp_parser_utils
- utp_var
- utp_expr
- utp_expr_insts
- utp_expr_funcs
- utp_unrest
- utp_usedby
- utp_subst
- utp_tactics
- utp_meta_subst
- utp_pred
- utp_alphabet
- utp_lift
- utp_pred_laws
- utp_healthy
- utp_rel
- utp_recursion
- utp_sequent
- utp_rel_laws
- utp_theory
- utp_hoare
- utp_wp
- utp_dynlog
- utp_state_parser
- utp_rel_opsem
- utp_sym_eval
- utp_sp
- utp_concurrency
- utp
- utp_expr_ovld
- utp_full
- utp_easy_parser
- sum_list
- utp_simple_time

### Depends on

- Optics

## Cite

×

UTP-AFP

    @article{UTP-AFP,
      author  = {Simon Foster and Frank Zeyda and Yakoub Nemouchi and Pedro Ribeiro and Burkhart Wolff},
      title   = {Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/UTP.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Feb 6, 2019 : Isabelle2018