JasonGross/lob JasonGross/lob

  • Stars
    star
    22
  • Rank 1,048,934 (Top 21 %)
  • Language Agda
  • License
    MIT License
  • Created about 11 years ago
  • Updated over 1 year ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
JasonGross/lob
github

JasonGross

Reviews

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

Repository Details

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

More Repositories

1

unsong_scraper

Unsong for kindle, based on https://github.com/rhelsing/worm_scraper
Ruby
63
star
2

coq-tools

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

coq-tactics

Collection of tactics I've found useful in Coq
Coq
11
star
4

coq-scripts

Various useful scripts for dealing with Coq files
Coq
8
star
5

guarantees-based-mechanistic-interpretability

Jupyter Notebook
7
star
6

social-interactions

Musings on social interactions and emotions
7
star
7

slow-coq-examples

Examples of Coq being really slow
Coq
5
star
8

doctoral-thesis

Personal PhD Thesis
TeX
4
star
9

proviola-source

Proviola, a tool for proof reanimation.
Python
4
star
10

lob-paper

A write-up of https://github.com/JasonGross/lob
Agda
4
star
11

neural-net-coq-interp

Some experiments with doing NN interpretability in Coq
Jupyter Notebook
4
star
12

parsing-parses

A dependently typed parser that parses parse trees to prove itself sound and complete
Coq
3
star
13

ct4s

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

18.721

Notes for 18.721
TeX
3
star
15

adt-synthesis

Repo for ADT Synthesis work, to eventually be integrated into github
Coq
2
star
16

barnowl-deduplicate-messages

BarnOwl plugin to deduplicate BarnOwl messages
Perl
2
star
17

Musica2

Fork of sourceforge Mathematica Musica package updated to work with Mathematica 8
Objective-C
2
star
18

coq-union-find

A repository for playing with union-find in Coq
Coq
2
star
19

tester

A web app to test you on vocab
JavaScript
2
star
20

time-worked

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

coq-8.6-wishlist

Presentation of wishlist for Coq for POPL 2014
TeX
1
star
22

lean-tools

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

HoTT-mathcamp-2015-class

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

ESG-SP.212-8.022

TeX
1
star
25

benediktahrens-coq-fossil

Clone of http://web.math.unifi.it/~benedikt/r.cgi/coq
Coq
1
star
26

gummi

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

iris-coq

The Coq development for Iris (mirrored)
Coq
1
star
28

characters

C
1
star
29

Agda

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

test-mit-license

Test repo for autogenerated MIT license
1
star
31

categoricaldata

fork of http://code.categoricaldata.net/categoricaldata/
Scala
1
star
32

ESG-SP.211-8.012

ESG SP.211-8.012
1
star
33

locality

CTAN Locality Package
1
star
34

outrageous-interpreter

Automatically exported from code.google.com/p/outrageous-interpreter
Coq
1
star
35

ClosestPoints

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

JasonGross.github.io

My personal website
Mathematica
1
star
37

coq-bug-minimizer-paper-bigdata

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