Discover @JasonGross Open Source projects

Jason Gross (@JasonGross)

JasonGross

Stars
205
Global Rank 120,909 (Top 5 %)
Followers 172
Following 11
Registered about 14 years ago
Most used languages

Coq 35.3 %

TeX
11.8 %

Python
8.8 %

Jupyter Notebook
5.9 %

C
5.9 %

Agda 5.9 %

Lean 2.9 %

Perl
2.9 %

Roff 2.9 %

Scala
2.9 %

Haskell
2.9 %

Ruby
2.9 %

Mathematica 2.9 %

JavaScript
2.9 %

Objective-C
2.9 %
Location 🇺🇸 United States
Country Total Rank 27,747
Country Ranking

Agda 11

Coq 27

Lean 115

Roff 526

Mathematica 626

TeX
1,303

Haskell
2,412

Perl
2,605

Ruby
2,800

Scala
3,169

Objective-C
7,328

Jupyter Notebook
8,308

unsong_scraper

Unsong for kindle, based on https://github.com/rhelsing/worm_scraper

coq-tools

Some scripts to help construct small reproducing examples of bugs, implement [Proof using], etc.

lob

Two attempts at formalizing Löb's Theorem, (one based on http://lesswrong.com/lw/t6/the_cartoon_guide_to_l%C3%B6bs_theorem/)

coq-tactics

Collection of tactics I've found useful in Coq

coq-scripts

Various useful scripts for dealing with Coq files

guarantees-based-mechanistic-interpretability

Jupyter Notebook

social-interactions

Musings on social interactions and emotions

slow-coq-examples

Examples of Coq being really slow

doctoral-thesis

Personal PhD Thesis

proviola-source

Proviola, a tool for proof reanimation.

lob-paper

A write-up of https://github.com/JasonGross/lob

neural-net-coq-interp

Some experiments with doing NN interpretability in Coq

Jupyter Notebook

parsing-parses

A dependently typed parser that parses parse trees to prove itself sound and complete

ct4s

Exercises for Category Theory For Scientists (18.S996, Spring 2013, http://math.mit.edu/~dspivak/teaching/sp13/)

18.721

Notes for 18.721

adt-synthesis

Repo for ADT Synthesis work, to eventually be integrated into github

barnowl-deduplicate-messages

BarnOwl plugin to deduplicate BarnOwl messages

Musica2

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

coq-union-find

A repository for playing with union-find in Coq

tester

A web app to test you on vocab

time-worked

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

coq-8.6-wishlist

Presentation of wishlist for Coq for POPL 2014

lean-tools

Some scripts to help construct small reproducing examples of bugs, etc (Port of https://github.com/JasonGross/coq-tools)

HoTT-mathcamp-2015-class

Syllabus and exercises for the class on HoTT I plan to teach at Candada/USA Mathcamp 2015

ESG-SP.212-8.022

benediktahrens-coq-fossil

Clone of http://web.math.unifi.it/~benedikt/r.cgi/coq

gummi

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

iris-coq

The Coq development for Iris (mirrored)

characters

Agda

Clone of Agda from http://code.haskell.org/Agda using https://github.com/purcell/darcs-to-git

test-mit-license

Test repo for autogenerated MIT license

categoricaldata

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

ESG-SP.211-8.012

ESG SP.211-8.012

locality

CTAN Locality Package

outrageous-interpreter

Automatically exported from code.google.com/p/outrageous-interpreter

ClosestPoints

A Coq implementation of an O(n log n) algorithm for finding the closest pair of points in a plane

JasonGross.github.io

My personal website

coq-bug-minimizer-paper-bigdata

Some data associated with https://github.com/JasonGross/coq-bug-minimizer-paper