Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details

All Programming Languages → Coq

Top 218 Coq open source projects

A list of commands, scripts, resources, and more that I have gathered and attempted to consolidate for use as OSCP (and more) study material. Commands in 'Usefulcommands' Keepnote. Bookmarks and reading material in 'BookmarkList' CherryTree. Reconscan Py2 and Py3. Custom ISO building.

✭ 1,916

c python perl shell C++Coq penetration-testing pentest oscp reconscan

A textbook on informal homotopy type theory

✭ 1,679

TeX python Coq Mathematica shell Makefile

3. Unix History Repo

Continuous Unix commit history from 1970 until today

✭ 4,851

assembly Coq Limbo unix freebsd history snapshot evolution berkeley bell-labs

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.

✭ 3,566

ocaml Coq TeX Standard ML shell c coq theorem-proving

5. first-fpga-pcb

FPGA dev board based on Lattice iCE40 8k

✭ 45

Verilog Coq Makefile python

The Ynot Project source code.

✭ 18

Coq ocaml Verilog

A Specification for Dependent Types in Haskell (Core)

✭ 64

No description, website, or topics provided.

✭ 25

General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]

✭ 36

Coq Makefile topology coq coq-library

Setoid-based Category Theory in Coq.

✭ 12

11. coq-simple-io

IO for Gallina

✭ 21

Coq ocaml Makefile shell coq extraction

12. SIMD-architecture

Overall multi-core SIMD microarchitecture

✭ 23

FPGA based transmitter

✭ 67

Verilog Coq VHDL python

Fun plugin to play with the Gallina AST.

✭ 31

ocaml Makefile Coq

15. SNES MiSTer ulx3s

SNES for MiSTer

✭ 15

VHDL Verilog SystemVerilog Coq tcl c

Coq encoding of ZFC and formalization of the textbook Elements of Set Theory

✭ 55

Coq Makefile math coq theorem-proving set-theory formal-languages

A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators

✭ 12

Coq coq proof ltl temporal-logic modal-logic coq-library

Algebraic Combinatorics in Coq

✭ 28

FOS - FPGA Operating System

✭ 49

VHDL c Coq Jupyter Notebook SystemVerilog tcl

A FPGA core for the arcade game, Rygar (1986).

✭ 17

VHDL Verilog SystemVerilog c Coq tcl game fpga arcade mister rygar

清华大学2019计网联合实验第一组

✭ 27

VHDL Coq V Verilog assembly SystemVerilog

A proof of Abel-Ruffini theorem.

✭ 26

Coq Nix Makefile coq ssreflect galois-theory mathcomp abel-ruffini

23. FormalizedCompilerAlgorithms

Formalization in Coq of algorithms used in compilers for the Compiler.org project

✭ 15

24. coq-of-ocaml

Formal verification of OCaml programs

✭ 161

ocaml Coq compiler coq

25. MiSTer-Arcade-SEGASYS1

FPGA implementation of SEGA SYSTEM 1 arcade board

✭ 18

Verilog VHDL SystemVerilog Coq tcl Batchfile

26. session-types-coq

Formalising session types in Coq

✭ 16

TeX Coq Makefile

No description, website, or topics provided.

✭ 13

Coq ocaml python Makefile

Coq course at Chalmers CSE

✭ 32

29. coq-record-update

Library to create Coq record update functions

✭ 33

Coq Makefile sed

A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]

✭ 29

Coq ocaml shell Makefile distributed-systems key-value coq causal-consistency coq-extraction docker-coq-action nix-action

Clafer is a lightweight modeling language

✭ 43

haskell TeX Makefile Yacc Coq emacs lisp

Finite sets, finite maps, multisets and generic sets

✭ 45

Coq Nix Makefile shell coq ssreflect finite-sets mathcomp

33. ltac2-tutorial

Ltac2 tutorial

✭ 27

Coq Makefile coq ltac2

SPARK 2014 repository for the Why3 verification platform.

✭ 17

ocaml Coq c Makefile shell Isabelle

35. chipfail-glitcher

No description, website, or topics provided.

✭ 55

SystemVerilog Verilog Coq Jupyter Notebook VHDL assembly shell

36. VerilogLanguageExtension

Verilog Language Extension for Visual Studio

✭ 16

C#Verilog Coq Makefile vsix verilog visual-studio-extension

Coq library for verified low-level programming

✭ 37

Coq Makefile c assembly Verilog ocaml

38. dot-calculus

Formalization of the Dependent Object Types (DOT) calculus

✭ 59

39. Constructors

Example Coq plugin

✭ 16

IP-core package generator for AXI4/Avalon

✭ 19

python Verilog Coq c tcl Makefile

Prototype implementation of domain-specific language for the design of smart-contracts over cryptocurrencies

✭ 138

javascript haskell TeX Isabelle Coq HTML

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

✭ 15

Coq coq set-theory ssreflect mathcomp docker-coq-action bourbaki

A mechanized proof of type safety for Featherweight Java using Coq

✭ 15

Exercism exercises in Coq.

✭ 15

shell Coq exercism-track

No description, website, or topics provided.

✭ 18

46. normalization-bench

Lambda normalization and conversion checking benchmarks for various implementations

✭ 46

haskell scala Coq lua javascript F#ocaml

Low-level graphics access for V

✭ 23

Coq python Verilog

No description, website, or topics provided.

✭ 14

HTML Coq ocaml Verilog Makefile CSS

A FPGA supported RISC-V CPU with 5-stage pipeline implemented in Verilog HDL

✭ 48

c Verilog C++assembly Coq SystemVerilog verilog-hdl risc-v

50. multinomials

Multinomials for the Mathematical Components library.

✭ 12

Coq Makefile coq polynomials ssreflect mathcomp

1-50 of 218 Coq projects