Pinned Repositories
coq-lit
Literate coq blog posts
ill-formed-expressions
jamesprl
A proof refinement logic in the style of JonPRL for my own edification
mechanized-metatheory2
miniprl-coq
A port of MiniPRL to Coq
mypyvy
A language for symbolic transitions system, inspired by Ivy.
notes
pretty
tactics
some Coq tactics I've found useful
wilcoxjay's Repositories
wilcoxjay/mypyvy
A language for symbolic transitions system, inspired by Ivy.
wilcoxjay/notes
wilcoxjay/mechanized-metatheory2
wilcoxjay/mypyvy-tool-paper
A tool paper about mypyvy
wilcoxjay/slides
wilcoxjay/autograder_samples
Examples of autograders for running on Gradescope
wilcoxjay/boogie
Boogie
wilcoxjay/book
Web browser engineering (a book)
wilcoxjay/CASL
wilcoxjay/chrome-extension
wilcoxjay/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.
wilcoxjay/coq-wigderson
Formalization of Wigderson's graph coloring algorithm in Coq
wilcoxjay/crowbar
Property fuzzing for OCaml
wilcoxjay/dafny-jrnl
Combining Perennial and Dafny with a verified journal
wilcoxjay/dslabs
Distributed Systems Labs and Framework
wilcoxjay/duckdb-web
DuckDB-Web - Source code of duckdb.org
wilcoxjay/dune
A composable build system for OCaml.
wilcoxjay/eggcc
wilcoxjay/egglog
egraphs + datalog!
wilcoxjay/ena
An implementation of union-find / congruence-closure in Rust. Extracted from rustc for independent experimentation.
wilcoxjay/gui
wilcoxjay/impy
Tool support for Dafny-TLA
wilcoxjay/jpl
wilcoxjay/knausj_talon
Config for talon for Mac, Windows and Linux. Very much in progress.
wilcoxjay/lambda-compile
LilyBin score compilation for AWS Lambda
wilcoxjay/symbol_table
A string interner
wilcoxjay/teaching-toolshed
Library of useful class for writing scripts to manage classes.
wilcoxjay/thesis
thesis
wilcoxjay/typeshed
Collection of library stubs for Python, with static types
wilcoxjay/yarpgen
Yet Another Random Program Generator