Skip to content

@isabelle-utp Isabelle/UTP

Change the repository type filter

All

    Repositories list

    36 repositories

    • Optics

      Public
      Lenses, Prisms, Scenes, and other Optics in Isabelle/HOL
      Isabelle
      •2•5•0•1•Updated Oct 3, 2025Oct 3, 2025

    • UTP

      Public
      A refreshed and minimalist implementation of Isabelle/UTP
      Isabelle
      •2•4•0•1•Updated Sep 26, 2025Sep 26, 2025

    • UTP-IMP

      Public
      A simple UTP relational imperative programming language with code generation support
      Isabelle
      •0•0•0•0•Updated Sep 26, 2025Sep 26, 2025

    • IsaCircus

      Public
      An implementation of the UTP semantics of Circus in Isabelle/UTP
      Isabelle
      •0•0•0•0•Updated Sep 24, 2025Sep 24, 2025

    • interaction-trees

      Public
      Interactions Trees in Isabelle/HOL and a CSP model
      Isabelle
      •1•7•1•1•Updated Sep 18, 2025Sep 18, 2025

    • Abstract_Prog_Syntax

      Public
      A simple Isabelle session introducing syntax for abstract programs
      Isabelle
      •1•1•0•0•Updated Sep 18, 2025Sep 18, 2025

    • Verified_Numerical_Methods

      Public
      Verifying numerical methods in Isabelle/HOL
      Isabelle
      •0•0•0•0•Updated Sep 12, 2025Sep 12, 2025

    • CyPhyAssure

      Public
      Distribution of the CyPhyAssure tools
      Shell
      •1•1•1•0•Updated Aug 28, 2025Aug 28, 2025

    • Shallow-Expressions

      Public
      Isabelle
      •
      BSD 3-Clause "New" or "Revised" License
      •2•3•1•0•Updated Aug 26, 2025Aug 26, 2025

    • Z_Toolkit

      Public
      This is an implementation of the Z mathematical toolkit in Isabelle/HOL, as described in ISO 13568:2002.
      Isabelle
      •1•5•2•0•Updated Aug 26, 2025Aug 26, 2025

    • Hybrid-Verification

      Public
      Components for Verifying Hybrid Systems in Isabelle/HOL
      Isabelle
      •1•6•0•0•Updated Jul 20, 2025Jul 20, 2025

    • UTP-Reactive-Designs

      Public
      The UTP theory of reactive designs
      Isabelle
      •0•0•0•0•Updated Jul 11, 2025Jul 11, 2025

    • UTP-Reactive

      Public
      UTP theory of reactive processes
      Isabelle
      •
      BSD 3-Clause "New" or "Revised" License
      •1•1•0•0•Updated Jul 8, 2025Jul 8, 2025

    • IsaVODEs_meta

      Public
      Meta repository for IsaVODEs
      Isabelle
      •0•0•0•0•Updated Jun 12, 2025Jun 12, 2025

    • Z_Machines

      Public
      Z-style Machines based on Interaction Trees
      Isabelle
      •
      BSD 3-Clause "New" or "Revised" License
      •1•1•0•0•Updated Apr 29, 2025Apr 29, 2025

    • UTP-Designs

      Public
      The UTP theory of designs
      Isabelle
      •
      BSD 3-Clause "New" or "Revised" License
      •2•1•0•0•Updated Apr 29, 2025Apr 29, 2025

    • explore-subgoal

      Public
      Adds an "explore_subgoal" command to Mathias Fleury's Explorer.thy
      Isabelle
      •2•1•0•0•Updated Apr 29, 2025Apr 29, 2025

    • CAS-Integration

      Public
      A project to integrate the functionality of Computer Algebra Systems into Isabelle
      Isabelle
      •2•3•0•0•Updated Apr 23, 2025Apr 23, 2025

    • mirror-afp-2025

      Public
      Git mirror of https://foss.heptapod.net/isa-afp/afp-2025
      Isabelle
      •1•0•0•0•Updated Apr 3, 2025Apr 3, 2025

    • Circus_Toolkit

      Public
      An extension of the Z Toolkit to support the Circus process language family.
      Isabelle
      •0•0•0•0•Updated Apr 3, 2025Apr 3, 2025

    • mirror-afp-2024

      Public
      Git mirror of https://foss.heptapod.net/isa-afp/afp-2024
      Isabelle
      •2•0•0•0•Updated Jan 3, 2025Jan 3, 2025

    • Hybrid-Library

      Public
      Additional theorems and tools to supporting reasoning about hybrid systems in Isabelle/HOL
      TeX
      •1•2•0•0•Updated Nov 27, 2024Nov 27, 2024

    • Total_Recall

      Public
      A utility to enable better support for overriding of syntax notation in Isabelle/HOL, developed by Dr Frank Zeyda.
      Standard ML
      •1•2•0•0•Updated Mar 30, 2024Mar 30, 2024

    • utp-main

      Public
      An implementation of Hoare and He's Unifying Theories of Programming in Isabelle
      theoryisabelleholutpunifying-theories
      Isabelle
      •
      Other
      •10•37•2•1•Updated Jan 29, 2024Jan 29, 2024

    • mirror-afp-2023

      Public
      Git mirror of https://foss.heptapod.net/isa-afp/afp-2023
      Isabelle
      •2•0•0•0•Updated Jan 15, 2024Jan 15, 2024

    • Z_Machines_Examples

      Public
      A library of examples based on Z-Machines
      Isabelle
      •0•1•0•0•Updated Mar 12, 2023Mar 12, 2023

    • mirror-afp-2022

      Public
      Git mirror of https://foss.heptapod.net/isa-afp/afp-2022
      Isabelle
      •2•0•0•0•Updated Mar 2, 2023Mar 2, 2023

    • isabelle-quantity

      Public
      Quantities in Isabelle/HOL
      TeX
      •0•2•0•0•Updated Jan 9, 2023Jan 9, 2023

    • RoboChart-Isabelle

      Public
      Isabelle
      •0•2•0•0•Updated Jan 4, 2023Jan 4, 2023

    • FSA_Proof

      Public
      A simple example tool for verifying finite state automata with a little DSL
      Isabelle
      •0•1•0•0•Updated Dec 12, 2022Dec 12, 2022