### Abstract

This is a simple framework for expressing linear-time properties. It supports the usual programming constructs (including interleaving parallel composition), equational and inequational reasoning about these, compositional assume/guarantee specifications and refinement, and the mixing of specifications and programs, all shallowly embedded in Isabelle/HOL.

### License

BSD License

### Topics

- Computer science/Concurrency

### Session ConcurrentHOL

- Strengthen
- HOL_Basis
- Aczel_Sequences
- Lifted_Predicates
- More_Lattices
- Closures
- Galois
- Heyting
- Safety_Logic
- Constructions
- Next_Imp
- Stability
- Refinement
- Programs
- Combinators
- Local_State
- TLS
- ConcurrentHOL
- Atomic
- Exceptions
- Assume_Guarantee
- WickersonDoddsParkinson
- Inhabitation
- FindP
- BFS
- Safety_Closure
- Ix
- Heap
- CImperativeHOL
- TSO
- TSO_Code_Gen
- TSO_litmus
- Floyd_Warshall

### Depends on

- Coinductive
- Optics

## Cite

×

ConcurrentHOL-AFP

    @article{ConcurrentHOL-AFP,
      author  = {Peter Gammie},
      title   = {ConcurrentHOL},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2024},
      note    = {\url{https://isa-afp.org/entries/ConcurrentHOL.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest