Skip to content
@logsem

Logic and Semantics @ Aarhus University

Popular repositories Loading

  1. iris-tutorial iris-tutorial Public

    Rocq Prover 70 34

  2. aneris aneris Public

    Program logic for developing and verifying distributed systems

    Rocq Prover 35 8

  3. clutch clutch Public

    Probabilistic separation logics for verifying higher-order probabilistic programs.

    Rocq Prover 33 9

  4. mitten_preorder mitten_preorder Public

    OCaml 31 2

  5. cerise cerise Public

    Formalisation of a capability machine and principles for reasoning about security properties

    Coq 25 8

  6. iris-lecture-notes iris-lecture-notes Public

    TeX 15 6

Repositories

Showing 10 of 34 repositories
  • clutch Public

    Probabilistic separation logics for verifying higher-order probabilistic programs.

    logsem/clutch’s past year of commit activity
    Rocq Prover 33 MIT 9 0 1 Updated Feb 3, 2026
  • iris-project Public
    logsem/iris-project’s past year of commit activity
    HTML 2 24 1 2 Updated Feb 3, 2026
  • aneris Public

    Program logic for developing and verifying distributed systems

    logsem/aneris’s past year of commit activity
    Rocq Prover 35 MIT 8 4 0 Updated Feb 3, 2026
  • griotte Public

    Rocq implementation of Griotte

    logsem/griotte’s past year of commit activity
    Rocq Prover 2 0 0 3 Updated Feb 1, 2026
  • AxSL Public

    AxSL, a concurrent separation logic for Arm's relaxed concurrency

    logsem/AxSL’s past year of commit activity
    Rocq Prover 1 1 0 0 Updated Jan 21, 2026
  • trillium Public

    The Trillium logic for proving trace refinement properties such as liveness via Iris

    logsem/trillium’s past year of commit activity
    Coq 4 MIT 3 0 4 Updated Jan 15, 2026
  • iris-wasmfx Public

    Iris-WasmFX program logic and logical relation for WasmFX

    logsem/iris-wasmfx’s past year of commit activity
    Rocq Prover 4 MIT 0 0 0 Updated Dec 6, 2025
  • cerisier Public

    Formalisation in Rocq of CHERI-TrEE

    logsem/cerisier’s past year of commit activity
    Rocq Prover 2 0 0 0 Updated Nov 11, 2025
  • spirea Public
    logsem/spirea’s past year of commit activity
    Coq 3 1 0 0 Updated Oct 20, 2025
  • machine_utils Public
    logsem/machine_utils’s past year of commit activity
    Coq 1 0 0 0 Updated Sep 21, 2025
View all repositories