hazardouspeach Goto Github PK

alienmuseumgame

Game for CodeDay 2014

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.

coq-library-undecidability

A library of mechanised undecidability proofs in the Coq proof assistant.

coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq

coq2vec

A module for encoding coq terms into fixed-width vectors

coq_serapy

Python bindings for Coq Serapi. Primarily designed for use in Proverbot9001. Works for Coq versions 8.9-8.12.

coq_serapy_scraper

A library for scraping proof data from a Coq .v file into static text, using the coq_serapy interface to Coq (a python binding for coq-serapi).

coqrel

Binary logical relations library for the Coq proof assistant

coquelicot

fpdebug

Dynamic Program Analysis based on Valgrind to find Floating-Point Accuracy Problems

gestalt-ratio-rust

A crate implementing gestalt pattern matching for Rust.

goboard

a simple go server

hardware

Verification and synthesis of hardware linear arithmetic structures.

hawkthorne-journey

Digital Estate Planning: The Game

hazardouspeach.github.io

Alex Sanchez-Stern's website

lin-alg-8.10

Linear Algebra

musescore-doubletime

A plugin for Musescore 3.0 for doubling the length of all notes in a sequence, ported from https://musescore.org/en/project/doubletime

neutrons-bench

The parts of uwplse/neutrons that are okay to share

pylspclient

LSP client implementation in Python, compatible with coq-lsp and coq_serapy

pytorch-types

quicksort-complexity

Proofs of Quicksort's worst- and average-case complexity

scripts

Some scripts I find useful

vst

Verified Software Toolchain

zchinese

A proof of the Chinese Remainder Lemma