Logic and Semantics @ Aarhus University

All

34 repositories

aneris
Public
Program logic for developing and verifying distributed systems
distributed-systems coq iris separation-logic
Rocq Prover
•
MIT License
•8•35•4•0•Updated Jan 16, 2026Jan 16, 2026
clutch
Public
Probabilistic separation logics for verifying higher-order probabilistic programs.
asynchronous coq logic iris probabilistic relational higher-order separation-logic couplings
Rocq Prover
•
MIT License
•8•31•0•1•Updated Jan 15, 2026Jan 15, 2026
trillium
Public
The Trillium logic for proving trace refinement properties such as liveness via Iris
Coq
•
MIT License
•3•4•0•4•Updated Jan 15, 2026Jan 15, 2026
iris-project
Public
HTML
•24•2•1•2•Updated Jan 14, 2026Jan 14, 2026
griotte
Public
Rocq implementation of Griotte
Rocq Prover
•
Other
•0•2•0•3•Updated Jan 7, 2026Jan 7, 2026
iris-wasmfx
Public
Iris-WasmFX program logic and logical relation for WasmFX
Rocq Prover
•
MIT License
•0•4•0•0•Updated Dec 6, 2025Dec 6, 2025
cerisier
Public
Formalisation in Rocq of CHERI-TrEE
Rocq Prover
•
Other
•0•2•0•0•Updated Nov 11, 2025Nov 11, 2025
spirea
Public
Coq
•1•3•0•0•Updated Oct 20, 2025Oct 20, 2025
machine_utils
Public
Coq
•0•1•0•0•Updated Sep 21, 2025Sep 21, 2025
iris-tutorial
Public
Rocq Prover
•
MIT License
•33•67•1•1•Updated Sep 4, 2025Sep 4, 2025
cerise
Public
Formalisation of a capability machine and principles for reasoning about security properties
Coq
•
Other
•8•25•5•1•Updated Jul 4, 2025Jul 4, 2025
gitrees
Public
guarded interaction trees
Coq
•2•10•0•0•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
•1•1•0•1•Updated May 2, 2025May 2, 2025
melocoton
Public
Coq
•
Other
•1•13•5•0•Updated Apr 28, 2025Apr 28, 2025
iris-nextgen
Public
Next generation modality for Iris
Coq
•0•3•0•0•Updated Dec 6, 2024Dec 6, 2024
adiar
Public
External Memory (Binary) Decision Diagrams
bdd binary-decision-diagrams external-memory zdd zero-suppressed-decision-diagrams
C++
•
MIT License
•15•0•0•0•Updated Nov 6, 2024Nov 6, 2024
AxSL
Public
AxSL, a concurrent separation logic for Arm's relaxed concurrency
arm concurrency verification separation-logic
Coq
•
Other
•1•1•0•0•Updated Oct 10, 2024Oct 10, 2024
MSWasm
Public
Coq
•
MIT License
•0•4•0•0•Updated Aug 19, 2024Aug 19, 2024
iris-lecture-notes
Public
TeX
•
Other
•6•15•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•31•1•0•Updated Apr 17, 2023Apr 17, 2023
VMSL
Public
Verifying FF-A hypercalls using VMSL.
coq iris separation-logic logical-relation hypercall ff-a robust-safety
Coq
•
Other
•0•3•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
•
Other
•1•1•0•0•Updated Apr 11, 2022Apr 11, 2022
free-theorems-sl
Public
Coq
•0•10•0•0•Updated Sep 29, 2021Sep 29, 2021