JasonGross/coq-scripts

Stars
8
Rank 2,099,232 (Top 42 %)
Language Coq
License
MIT License
Created over 10 years ago
Updated about 1 year ago

JasonGross/coq-scripts

JasonGross

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Various useful scripts for dealing with Coq files

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

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