simongregersen
Follow
Stars
Probabilistic separation logics for verifying higher-order probabilistic programs.
Formal Analysis of the PQXDH Protocol
Program logic for developing and verifying distributed systems
A new markup-based typesetting system that is powerful and easy to learn.
A formalization of a Proof-of-Stake Nakamoto-style blockchain in Coq
A LaTeX package to make theorem names link to coqdoc webpages. Works with ntheorem, amsthm and the LLNCS and LIPIcs classes.
We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.
OpenOrienteering Mapper is a software for creating maps for the orienteering sport.
Foundational Cryptography Framework for machine-checked proofs of cryptography.
A collection of tools for writing technical documents that mix Coq code and prose.
Library to create Coq record update functions
A Probability Theory Library for the Coq Theorem Prover
A program logic for concurrent randomized programs
Strong non-interference for fine-grained concurrent programs
A dependently typed programming language, a successor to Idris
Instrumentation framework for Node.js compliant to ECMAScript 2020 based on GraalVM.
Learn Lisp The Hard Way source-code and full book text