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/ill-formed-expressions
wilcoxjay/jamesprl
A proof refinement logic in the style of JonPRL for my own edification
wilcoxjay/miniprl-coq
A port of MiniPRL to Coq
wilcoxjay/articles
Miscellaneous articles. The readme is the table of contents.
wilcoxjay/boogie-friends
Tools for interacting with Boogie
wilcoxjay/coqproject
wilcoxjay/crossbot
A slackbot to compete on mini crosswords (or any other daily challenge).
wilcoxjay/crossword
wilcoxjay/dafny
Dafny is a verification-aware programming language
wilcoxjay/Ethan-Cheerios
A reimplementation of UW PLSE's Cheerios formally verified serialization/deserialization library
wilcoxjay/generals-template
Simple LaTeX template for a UW General Exam document
wilcoxjay/goddity
generalized oddity
wilcoxjay/gregjs
Javascript library for displaying Gregorian chant
wilcoxjay/ivy
IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
wilcoxjay/JonPRL
An proof refinement logic for computational type theory based on realizability & meaning explanations. Inspired by Nuprl
wilcoxjay/linear-stlc-handout
handout for reading group presentation on linear lambda calculus
wilcoxjay/ltac2
A standalone implementation of Ltac2 as a Coq plugin
wilcoxjay/miniprl
A small implementation of a proof refinement logic.
wilcoxjay/myvy
wilcoxjay/pjreddie.com
My website!
wilcoxjay/racket-z3-example
wilcoxjay/sml-abt
This is the CMU ABT library, with some minor improvements. DEPRECATED in favor of https://github.com/JonPRL/sml-typed-abts
wilcoxjay/sml-abt-parser
A parser library for ABTs based on parcom. DEPRECATED in favor of https://github.com/jonsterling/sml-typed-abts
wilcoxjay/sml-redprl
Decisively Smash the Formalist Clique!—The People's Refinement Logic
wilcoxjay/sml-telescopes
an abstract data type for telescopes
wilcoxjay/sml-typed-abts
indexed second-order abstract syntax
wilcoxjay/SpaceSearch
wilcoxjay/vapor.cab
vapor.cab
wilcoxjay/verdi
A framework for formally verifying distributed systems implementations in Coq
wilcoxjay/VS-Code-Language-Server-for-Dafny