yforster's Stars
coq/coq
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 development of machine-checked proofs.
helmuthdu/aui
Archlinux Ultimate Install
FStarLang/FStar
A Proof-oriented Programming Language
matijapretnar/eff
A functional programming language based on algebraic effect handlers
jscoq/jscoq
A port of Coq to Javascript -- Run Coq in your Browser
ProofGeneral/PG
This repo is the new home of Proof General
cebe/pdfpc-latex-notes
Latex Package that allows creating a pdfpc compatible notes file directly from your latex presentation \notes.
amintimany/Categories
A formalization of category theory in the Coq proof assistant.
coq-community/coq-dpdgraph
Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
UBA-PSI/psi-thesis-guide
Guidelines for creating a high-quality scientific thesis with tips and examples for layout, figures, and tables
coq-community/aac-tactics
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
coq-community/coq-program-verification-template
Template project for program verification in Coq, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog]
mattam82/Constructors
Example Coq plugin
LPCIC/matita
Matita (proof assistant) with embedded elpi
sigurdschneider/smpl
A Coq plugin providing an extensible tactic similar to first.