Explore projects
- 
Iris / stdppBSD 3-Clause "New" or "Revised" LicenseAn extended "Standard Library" for Coq. [coqdoc] Updated
- 
- 
Tesla Zhang / stdppBSD 3-Clause "New" or "Revised" LicenseAn extended "Standard Library" for Coq. coqdoc(https://plv.mpi-sws.org/coqdoc/stdpp/) Updated
- 
RT-PROOFS / PROSA - Formally Proven Schedulability AnalysisBSD 2-Clause "Simplified" LicenseThe main Coq development of the Prosa project: http://prosa.mpi-sws.org Updated
- 
Iris / IrisBSD 3-Clause "New" or "Revised" LicenseThe Coq development for Iris. [project website] [coqdoc] Updated
- 
operating-systems / buildos25 / cloudosMIT LicenseUpdated
- 
Updated
- 
Updated
- 
Jonas Kaufmann / cloudosMIT LicenseUpdated
- 
Antoine Kaufmann / cloudosMIT LicenseUpdated
- 
Athul Raj Kollareth / PROSA - Formally Proven Schedulability AnalysisBSD 2-Clause "Simplified" LicenseThe main Coq development of the Prosa project: http://prosa.mpi-sws.org Updated
- 
Simon Spies / IrisBSD 3-Clause "New" or "Revised" LicenseThe Coq development for Iris. [project website] [coqdoc] Updated
- 
Iris / lambda-rustBSD 3-Clause "New" or "Revised" LicenseThe Coq development of LambdaRust Updated
- 
Iris / simulirisBSD 3-Clause "New" or "Revised" LicenseLocal Simulation proofs, the Iris style Updated
- 
Iris / gpfslBSD 3-Clause "New" or "Revised" LicenseA combination of GPS and FSL in the ORC11 semantics (the promising semantics WITHOUT promises) Updated
- 
Iris / IronBSD 3-Clause "New" or "Revised" LicenseThe Iron logic for precise reasoning about resources [project website] Updated
- 
Iris / examplesBSD 3-Clause "New" or "Revised" LicenseSome example verification demonstrating the use of Iris. Updated
- 
Offering the seminar course at MPI-SWS & Universität des Saarlandes for Winter Semester 2025-2026 Updated
- 
Paolo G. Giarrusso / irisBSD 3-Clause "New" or "Revised" LicenseThe Coq development for Iris Updated
- 
Iris / DimSumBSD 3-Clause "New" or "Revised" LicenseUpdated
