Explore projects

The Coq development of LambdaRust

The Coq development for Iris. project website(https://iris-project.org/) coqdoc(https://plv.mpi-sws.org/coqdoc/iris/)

mperl: A language for custom robotic manipulators

3D visualization of asynchronous program executions.

Some example verification demonstrating the use of Iris.

The Coq development for Iris. project website(https://iris-project.org/) coqdoc(https://plv.mpi-sws.org/coqdoc/iris/)

An extended "Standard Library" for Coq. [coqdoc]

This is a static analyser developed for the Program Analysis course at TU Kaiserslautern. for more information see the course page: https://moodle.mpi-sws.org/course/view.php?id=24

An extended "Standard Library" for Coq. coqdoc(https://plv.mpi-sws.org/coqdoc/stdpp/)

The Coq development for Iris. project website(https://iris-project.org/) coqdoc(https://plv.mpi-sws.org/coqdoc/iris/)

UniTraX data for experiments. See main repository at https://gitlab.mpi-sws.org/anon/unitrax for more information.

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

This is a demo showing how the the Iris Proof Mode can be used with FSCQ.

The main Coq development.

The Coq development for Iris. project website(https://iris-project.org/) coqdoc(https://plv.mpi-sws.org/coqdoc/iris/)