Skip to content

@logsem Logic and Semantics @ Aarhus University

Change the repository type filter

All

    Repositories list

    34 repositories

    • clutch

      Public
      Probabilistic separation logics for verifying higher-order probabilistic programs.
      asynchronouscoqlogic
      asynchronouscoqlogicirisprobabilisticrelationalhigher-orderseparation-logiccouplings
      Rocq Prover
      •
      MIT License
      •9•38•0•2•Updated Apr 18, 2026Apr 18, 2026

    • aneris

      Public
      Program logic for developing and verifying distributed systems
      distributed-systemscoqiris
      distributed-systemscoqirisseparation-logic
      Rocq Prover
      •
      MIT License
      •8•36•4•0•Updated Apr 16, 2026Apr 16, 2026

    • cerisier

      Public
      Formalisation in Rocq of CHERI-TrEE
      Rocq Prover
      •
      Other
      •0•2•0•0•Updated Apr 8, 2026Apr 8, 2026

    • iris-nextgen

      Public
      Next generation modality for Iris
      Coq
      •0•3•0•0•Updated Apr 7, 2026Apr 7, 2026

    • iris-project

      Public
      HTML
      •27•3•1•2•Updated Mar 31, 2026Mar 31, 2026

    • spirea

      Public
      Coq
      •1•3•0•0•Updated Mar 30, 2026Mar 30, 2026

    • adiar

      Public
      External Memory (Binary) Decision Diagrams
      bddbinary-decision-diagramsexternal-memory
      bddbinary-decision-diagramsexternal-memoryzddzero-suppressed-decision-diagrams
      C++
      •
      MIT License
      •17•0•0•0•Updated Mar 24, 2026Mar 24, 2026

    • griotte

      Public
      Rocq implementation of Griotte
      Rocq Prover
      •
      Other
      •0•2•0•3•Updated Mar 20, 2026Mar 20, 2026

    • machine_utils

      Public
      Coq
      •0•1•0•0•Updated Mar 20, 2026Mar 20, 2026

    • iris-wasmfx

      Public
      Iris-WasmFX program logic and logical relation for WasmFX
      Rocq Prover
      •
      MIT License
      •0•4•0•0•Updated Mar 15, 2026Mar 15, 2026

    • cerise

      Public
      Formalisation of a capability machine and principles for reasoning about security properties
      Rocq Prover
      •
      Other
      •8•26•5•1•Updated Mar 12, 2026Mar 12, 2026

    • trillium

      Public
      The Trillium logic for proving trace refinement properties such as liveness via Iris
      Coq
      •
      MIT License
      •3•4•0•4•Updated Feb 13, 2026Feb 13, 2026

    • AxSL

      Public
      AxSL, a concurrent separation logic for Arm's relaxed concurrency
      armconcurrencyverification
      armconcurrencyverificationseparation-logic
      Rocq Prover
      •
      Other
      •1•1•0•0•Updated Jan 21, 2026Jan 21, 2026

    • iris-tutorial

      Public
      Rocq Prover
      •
      MIT License
      •34•75•0•1•Updated Sep 4, 2025Sep 4, 2025

    • gitrees

      Public
      guarded interaction trees
      Coq
      •3•13•0•1•Updated Jul 4, 2025Jul 4, 2025

    • cerise-interpreter

      Public
      OCaml
      •
      Other
      •0•2•0•0•Updated May 27, 2025May 27, 2025

    • synthetic_domains

      Public
      Coq
      •
      MIT License
      •0•1•0•0•Updated May 14, 2025May 14, 2025

    • iriswasm

      Public
      IrisWasm program logic and logical relation for WebAssembly
      Coq
      •
      MIT License
      •0•1•0•0•Updated May 2, 2025May 2, 2025

    • melocoton

      Public
      Coq
      •
      Other
      •1•13•5•0•Updated Apr 28, 2025Apr 28, 2025

    • MSWasm

      Public
      Coq
      •
      MIT License
      •0•4•0•0•Updated Aug 19, 2024Aug 19, 2024

    • iris-lecture-notes

      Public
      TeX
      •
      Other
      •6•16•8•1•Updated Jul 24, 2024Jul 24, 2024

    • fw-rec-inj

      Public
      Coq
      •
      MIT License
      •0•2•0•1•Updated Mar 11, 2024Mar 11, 2024

    • well-bracketed-logic

      Public
      Coq
      •
      MIT License
      •0•3•0•0•Updated Jan 2, 2024Jan 2, 2024

    • machine_program_logic

      Public
      Coq
      •0•0•0•0•Updated Dec 14, 2023Dec 14, 2023

    • terpsichore

      Public
      Studying and Formalising Choreographies in Iris
      0•0•0•0•Updated Oct 31, 2023Oct 31, 2023

    • two_pcf_models

      Public
      Two models of PCF in siProp
      Coq
      •0•0•0•0•Updated Jul 14, 2023Jul 14, 2023

    • mitten_preorder

      Public
      OCaml
      •
      MIT License
      •2•32•1•0•Updated Apr 17, 2023Apr 17, 2023

    • VMSL

      Public
      Verifying FF-A hypercalls using VMSL.
      coqirisseparation-logic
      coqirisseparation-logiclogical-relationhypercallff-arobust-safety
      Coq
      •
      Other
      •0•4•1•0•Updated Apr 14, 2023Apr 14, 2023

    • cerise-stack-monotone

      Public
      Formalisation of temporal stack safety properties on a capability machine with local, uninitialized and directed capabilities.
      coq
      coq
      Coq
      •
      Other
      •1•2•0•0•Updated Apr 11, 2022Apr 11, 2022

    • free-theorems-sl

      Public
      Coq
      •0•11•0•0•Updated Sep 29, 2021Sep 29, 2021
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.