spitters

spitters's Stars

• hacspec/hax

  A Rust verification tool

  Language:OCaml19820

• Fontex5/Thesis-Project-MPC-Energy-Trading

  Language:Rust2

• tip-org/tools

  Language:Haskell217

• zkpstandard/wg-plonkish

  Language:Shell82

• bshvass/fiat-crypto

  Cryptographic Primitive Code Generation by Fiat

  Language:Coq42

• cfrg/draft-irtf-cfrg-hash-to-curve

  Hashing to Elliptic Curves

  Language:Python7927

• cfrg/draft-irtf-cfrg-bls-signature

  Language:Python3216

• Concordium/Concordium-Free-Open-Grants-Program

  Concordium Free & Open Grants Program aims to power innovative opensource applications in the Concordium Ecosystem.

  3721

• The-DevX-Initiative/RCIG_Coordination_Repo

  A Coordination repo for all things Rust Cryptography oriented

  Language:HTML26034

• RasmusHoldsbjergCSAU/QuadraticFieldExtensions

  Quadratic Extensions of Prime order Fields - Formalization in Coq

  Language:C21

• WasmCert/WasmCert-Coq

  A mechanisation of Wasm in Coq

  Language:Coq9511

• tchajed/coq-ltac2-experiments

  All the code I've ever written in Ltac2

  Language:Coq11

• UniMath/SymmetryBook

  This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.

  Language:HTML39623

• gmalecha/coq-smt-check

  Invoke SMT solvers from Coq to check obligations

  Language:OCaml103

• RedPRL/redtt

  "Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory

  Language:OCaml20412

• coq/stdlib2

  Language:Coq399

• coq-community/manifesto

  Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.

  686

• astump/cedille-core

  Language:Haskell81

• SkySkimmer/HoTTClasses

  HoTT proofs using experimental induction-induction (mostly about real numbers) (used to contain the HoTT.Classes proofs)

  Language:Coq145

• SkySkimmer/HoTT-algebra

  Coq formalisation of algebra in Homotopy Type Theory

  Language:Coq71

• EasyCrypt/easycrypt

  EasyCrypt: Computer-Aided Cryptographic Proofs

  Language:OCaml31949

• coq-community/corn

  Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]

  Language:Coq11144

• LimitPointSystems/SheafSystem

  The SheafSystem™ suite of data representation and management tools is based on our patented sheaf data model. The SheafSystem™ uses advanced mathematics - posets, lattices, sheaves, and fiber bundles - to revolutionize the handling of the complex, structure rich data sets of scientific computing. SheafSystem™ tools make it easy to construct, manipulate, store, retrieve, and inter-operate diverse representations of physical data.

  Language:C++43

• gkovacs/pdfocr

  Adds text to PDF files using the cuneiform OCR software

  Language:Ruby32549

• michalkonecny/polypaver

  A theorem prover specialised in deciding inequalities of non-linear real and floating-point expressions using rigorous polynomial approximations. Includes tools for verifying floating-point SPARK 2005 programs.

  Language:Haskell41

• HoTT/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.

  Language:OCaml275

• EvgenyMakarov/corn

  Language:Coq2

• guillaumebrunerie/HoTT

  This repository is now obsolete

  Language:Coq11

• coq-community/math-classes

  A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

  Language:Coq16243

• HoTT/Coq-HoTT

  A Coq library for Homotopy Type Theory

  Language:Coq1.3k193