Stars
libdtrace-ctf is the Compact Type Format library used by DTrace on Linux
Static analyzer for C/C++ based on the theory of Abstract Interpretation.
Algebraic Effects in Haskell using Implicit Parameters
The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor mo…
🚧 My notes and solutions to Coq course by Anton Trunov (source: https://github.com/anton-trunov/coq-lecture-notes) in 2019. WIP.
🚧 Repo to keep track of my notes and solutions to the Mathematical components book.
Code documentation written as code! How novel and totally my idea!
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…
Formal proof of the Four Color Theorem [maintainer=@ybertot]
Showing how some simple mathematical theories naturally give rise to some common data-structures
A Verified Compiler for Gallina, Written in Gallina
Lecture notes for a short course on proving/programming in Coq via SSReflect.
Towards a verified back-end for The Glorious Glasgow Haskell Compilation System
This is a game: how fast will systemd eat your system?
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Easy access to the interface information of installed OCaml libraries for editors like Emacs and Vim.