gmalecha Goto Github PK

bbv

Bedrock Bit Vector Library

bedrock-mirror-shard

Port of Bedrock to use MirrorShard library for computational reflection

categorical-unification

Exploration of unification on categorical terms.

category-theory

A formalization of category theory in Coq for personal study and practical work

ceps

Coq Enhancement Proposals

charge

Higher-order separation logic framework in Coq

chargecore

clang

Mirror of official clang git repository located at http://llvm.org/git/clang. Updated every five minutes.

compdata

Haskell library implementing "Data Types a la Carte"

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.

coq-apply-any

An extension to eauto that allows you to apply an arbitrary lemma from a hint database

coq-checkless

Coq plugin for refine which does not perform type checking.

coq-dep-replace

Coq plugin to perform dependent replacement of terms

coq-extensible-records

Implementation of extensible records in Coq

coq-gc

Coq plugin to force garbage collection

coq-interact

programmatic interaction with coq

coq-interaction-trees

Co-inductive interaction trees provide a way to represent (potentially) non-terminating programs with I/O behavior.

coq-k

Some formalization of the K framework in Coq

coq-localize

Coq plugin for making terms self-contained

coq-ltac-iter

Access hint databases from tactics.

coq-markov

Exploring probabilistic programming in Coq

coq-mod-reduce

Modular reduction specifications for cbv

coq-plugin-template

Template for Coq plugins

coq-plugin-utils

Useful utility functions for writing Coq plugins

coq-printf

Implementation of sprintf for Coq

coq-refinement

Relational refinements in Coq based on the work of Maxime Denes.

coq-seal

Implementation of sealing in Coq with macros for generation

coq-simulink

Simulink-like formalism in Coq

coq-smt-check

Invoke SMT solvers from Coq to check obligations

coq-temporal

An implementation of temporal logic in Coq using Charge!