arthuraa Goto Github PK

agda-hoas-demo

Experiments with higher-order abstract syntax in Agda

beaq

A Formalization of TeX in Coq

cis670-project

Oh yeah

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-cpo

A Coq library for CPOs

coq-utils

Some basic libraries for Coq.

coq-void

Mathcomp instances for the empty type

cryptis

cufp-2015-tutorial

An introductory tutorial for the Coq proof assistant.

cutelittlethings

deriving

Class instances for Coq inductive types with little boilerplate

dossier

el-get

Manage the external elisp bits and pieces upon which you depend!

emacs-files

Personal configuration files for Emacs

emacs-theme-gruvbox

Gruvbox is a retro groove color scheme for Emacs. Port of the Vim version.

extructures

Finite sets and maps for Coq with extensional equality

extructures-instances

OrdType Instances for Other Mathematical Components Types

finmap

Finite sets, finite maps, multisets and generic sets

finprob

Finite probability theory in Coq

forest-explanations

gimme

XMMS2 client for GNU Emacs

hashcons

Hash consing and memoisation for Haskell

latex-template

A template for LaTeX documents

ll-cut-elim

Cut elimination for Intuitionistic Linear Logic in Coq

math-comp

Mathematical Components

mc326-bplus

memory-safe-language

A formalization of properties of a simple imperative, memory-safe language.

mongomapper

A Ruby Object Mapper for Mongo

netter

Produce Prism models from a simple imperative language

nixpkgs

Nix Packages collection