JasonGross/andromeda
A minimalist implementation of type theory, suitable for experimentation
Discovered public repositories for JasonGross in the GitHub catalog.
A minimalist implementation of type theory, suitable for experimentation
Implemention of geometric packing algorithm for 6.850 - Geometric Computing - class
Repo to recreate coqdoc bug https://coq.inria.fr/bugs/show_bug.cgi?id=3292
Copies of academic papers referenced on my personal website
A PSet class and common header file
A Coq implementation of an O(n log n) algorithm for finding the closest pair of points in a plane
A habit tracker app which treats your goals like a Role Playing Game.
Collection of tactics I've found useful in Coq
My personal website
Repo for ADT Synthesis work, to eventually be integrated into github
Clone of Agda from http://code.haskell.org/Agda using https://github.com/purcell/darcs-to-git
Clone of agda standard library http://www.cse.chalmers.se/~nad/repos/lib/ using https://github.com/purcell/darcs-to-git
Presentation of wishlist for Coq for POPL 2014
Automatically test a large number of category theory libraries
Clone of http://web.math.unifi.it/~benedikt/r.cgi/coq
Shared resources useful for multiple HabitRPG repositories. Assets (sprites, imgs, etc), CSS, algorithms, and more.
Proviola, a tool for proof reanimation.
A work in progress of converting lambda calculus terms to functors
Two attempts at formalizing Löb's Theorem, (one based on http://lesswrong.com/lw/t6/the_cartoon_guide_to_l%C3%B6bs_theorem/). Write-up at https://github.com/JasonGross/lob-paper
My resume and CV
A Dependently Typed Functional Programming Language
Homotopy type theory
A textbook on informal homotopy type theory
Categories parametrized by morphism equality, in Agda
Some scripts to help construct small reproducing examples of bugs, implement [Proof using], etc.
Exercises for Category Theory For Scientists (18.S996, Spring 2013, http://math.mit.edu/~dspivak/teaching/sp13/)
Development of the univalent foundations of mathematics in Coq
Demo for an Ur/Web app using the C FFI to compile LaTeX documents
A playground for building category theory on top of commutative diagrams in 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.
A few python scripts for logging how much time I've worked on some project.
fork of http://code.categoricaldata.net/categoricaldata/
Fork of sourceforge Mathematica Musica package updated to work with Mathematica 8
A fork of the LaTeX editor gummi (http://dev.midnightcoding.org/projects/gummi)
Musings on social interactions and emotions
A web app to test you on vocab
BarnOwl plugin to deduplicate BarnOwl messages
Notes for 18.721
Public repository.
Fork of Paul Irish's image loaded method for jQuery
CTAN Locality Package
A multi-protocol curses IM client.
Public repository.
ESG SP.211-8.012