Explore GitLab
Discover projects, groups and snippets. Share your projects with others

FP / LambdaRustcoq
The Coq development of LambdaRust

FP / gpfsl
A combination of GPS and FSL in the ORC11 semantics (the promising semantics WITHOUT promises)

FP / orc11
Operational Repaired C11

Jonas Kastberg / iriscoq
The Coq development for Iris

FP / iriscoq
The Coq development for Iris

Felix Stutz / rtproofs
The main Coq development.
0updated 
FP / opamdev
opam repository for development versions of things we develop.
1updated 
Iris / stdpp
An extended "Standard Library" for Coq

Iris / examples
Some example verification demonstrating the use of Iris.

Iris / Iron
The Iron logic for precise reasoning about resources.

Joseph Tassarotti / fricoq
An extension of the Iris program logic to support linearity and fair refinement reasoning.
0updated 
Iris / oRA
Formalizes the ordered RA model of Iris

Dan Frumin / ReLoC
A calculus of logical relations for concurrency, formalized in Iris.

FP / promising
An extraction of the promising semantics

FP / ragps
A soundness proof for GPS and RSL with ReleaseAcquire semantics in Iris.

Iris / atomic
Logically Atomic Triples in Iris

Marcus Pirron / CableRobot
Code for the CableRobot

Dan Frumin / iriscoq
The Coq development for Iris
0updated 
FP / irisci
This project contains some scripts and other files that are used by many Iris project for their CI
0updated 
Maxime Lesourd / rtproofs
The main Coq development.
0updated