dangrayson Goto Github PK

a-star

Software and drivers for the Pololu A-Star 32U4 Micro.

bibtex2html

book

A textbook on informal homotopy type theory

cgc1

Conservative Garbage Collector in C++11

cgc1-1

Conservative Garbage Collector in C++11

checker

an attempt at making a prototype proof checker for experimental purposes

coq

This is my fork of the coq github source repository, for working on improvements for HoTT.

coq-builder

A system of makefiles for building coq and the programs it requires.

coq-tex

Process coq code in a tex file, adding coq's output to the tex file so it appears in the final document.

coq-tools

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

cubicaltt

debounce-mac

Frustrated that OS X doesn't have a simple software keyboard debouncer. Here's my hack.

dedekind-reals

A formalization of the Dedekind reals in Coq

epkg

Here I present a simple bug fix to epkg, the encap-based generic package manager. The problem was that it was setting the umask before creating files and directories.

foundations2

Development of the univalent foundations of mathematics in Coq

homebrew-core

🍻 Default formulae for the missing package manager for macOS

hott

Homotopy type theory

interactiveshell-1

Build web apps for interactive command-line tools

internals

In this repository we record some files used to demonstrate the internal operation of the Macaulay2 build system and source code.

ktheory

formalization of theorems of higher algebraic K-theory

libmidi44

m2

The primary source code repository for Macaulay2

m2-merge

run M2 on code embedded in a TeX file and insert the output

macaulay2.github.io

The Macaulay2 web site

mutopiaproject

Open source sheet music

pendulumtimer

a timer for pendulum clocks

pianomusic

piano scores with my personal annotations for my piano lessons

proofgeneral

ProofGeneral, adapted for use with "checker", my prototype proof assistant

rezk_completion

Rezk completion

typetheory