jasongross Goto Github PK

kami

A Platform for High-Level Parametric Hardware Specification and its Modular Verification

lambda-cat

A work in progress of converting lambda calculus terms to functors

lambdajs

Semantics and tools for JavaScript

language-ecmascript

Haskell library: ECMAScript parser, pretty-printer and additional tools

latex-util

A PSet class and common header file

lean-inductive-inductive-desugar

Python scripts to desugar fully annotated lean inductive inductive definitions to mutual inductives

lean-playground

Some basic learning exercises in lean

lean-tools

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

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/)

lob-paper

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

locality

CTAN Locality Package

logitext

Beautiful, interactive visualizations of logical inference

ltac2

A standalone implementation of Ltac2 as a Coq plugin

masters-thesis

Personal Masters Thesis

math-classes

A library of abstract interfaces for mathematical structures in Coq.

math-comp

Mathematical Components

mathcamp-2015-equality-class

Notes and HW from my 2015 Mathcamp equality-in-Coq class

mctb_scraper

Adaptation of https://github.com/TheBrain0110/worm_scraper and https://github.com/JasonGross/unsong_scraper for https://www.mctb.org/mctb2

metacoq-lob

A WIP formalization of Löb's theorem based on MetaCoq

mirror-core

A framework for extensible, reflective decision procedures.

misc-files

Miscellaneous useful files

ml-lambdajs

JavaScript semantics

monospacifier

Convert variable-pitch fonts to monospace (useful for unicode and indentation-friendly programming)

mozjs

Mirror of Mozilla's mozjs

mtac2

multinomials

Multinomials for the Mathematical Components library.

musica2

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

normalization-bench

Lambda normalization and conversion checking benchmarks for various implementations

notations-demonstrations

Some demonstrations of Coq notations

nsatz-assoc-test

Tests for nsatz on weierstrass associativity