JasonGross

JasonGross's Stars

• ytdl-org/youtube-dl

  Command-line program to download videos from YouTube.com and other video sites

  Language:Python134k2.2k26.7k10.2k

• avgupta456/github-trends

  🚀 Level up your GitHub profile readme with customizable cards including LOC statistics!

  Language:Python15.7k11198106

• leanprover/lean4

  Lean 4 programming language and theorem prover

  Language:Lean4.9k672k446

• agda/agda

  Agda is a dependently typed programming language / interactive theorem prover.

  Language:Haskell2.5k665.6k365

• HoTT/book

  A textbook on informal homotopy type theory

  Language:TeX2k121634360

• latex3/latex3

  The expl3 (LaTeX3) Development Repository

  Language:TeX1.9k711.1k192

• UniMath/UniMath

  This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

  Language:Coq96957526173

• HoTT/HoTT-Agda

  Development of homotopy type theory in Agda

  Language:Agda422562559

• MetaCoq/metacoq

  Metaprogramming, verified meta-theory and implementation of Coq in Coq

  Language:Coq4051715784

• cpitclaudel/company-coq

  A Coq IDE build on top of Proof General's Coq mode

  Language:Emacs Lisp3511024028

• Andromedans/andromeda

  A proof assistant for general type theories

  Language:OCaml2982319734

• math-comp/analysis

  Mathematical Components compliant Analysis Library

  Language:Coq2121838149

• ezyang/logitext

  Beautiful, interactive visualizations of logical inference

  Language:UrWeb15011611

• jonsterling/JonPRL

  An proof refinement logic for computational type theory. Inspired by Nuprl. [For up-to-date development, see JonPRL's successor, RedPRL: https://github.com/redprl/sml-redprl]

  Language:Standard ML110191169

• dlicata335/hott-agda

  Language:Agda841916

• uwplse/PUMPKIN-PATCH

  Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

  Language:OCaml5110632

• vrahli/NuprlInCoq

  Implementation of Nuprl's type theory in Coq

  Language:Coq44833

• machine-intelligence/provability

  Language:Haskell3525011

• plclub/lngen

  Tool for generating Locally Nameless definitions and proofs in Coq, working together with Ott

  Language:Haskell301029

• 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:OCaml27151205

• mattam82/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:OCaml5430

• SkySkimmer/coq-ltac2-compiler

  Language:OCaml5390

• benediktahrens/Foundations

  Development of the univalent foundations of mathematics in Coq

  Language:Coq3401

• barras/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:OCaml2302

• JasonGross/Musica2

  Fork of sourceforge Mathematica Musica package updated to work with Mathematica 8

  Language:Objective-C2201

• asya-bergal/setoid_rewrite_debug

  a python script to help debug setoid_rewrite failures in coq

  Language:Python1301

• JasonGross/categoricaldata

  fork of http://code.categoricaldata.net/categoricaldata/

  Language:Scala120

• JasonGross/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:OCaml120

• JasonGross/gummi

  A fork of the LaTeX editor gummi (http://dev.midnightcoding.org/projects/gummi)

  Language:C120

• JasonGross/time-worked

  A few python scripts for logging how much time I've worked on some project.

  Language:Python121