Assistant Professor of Computer Science at Illinois. Type theory, proof engineering, proof automation.
- Champaign, IL
- https://dependenttyp.es
- @TaliaRinger
Pinned Loading
-
uwplse/PUMPKIN-PATCH
uwplse/PUMPKIN-PATCH PublicProof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
-
uwplse/pumpkin-pi
uwplse/pumpkin-pi PublicAn extension to PUMPKIN PATCH with support for proof repair across type equivalences.
-
-
-
rocq-prover/rocq
rocq-prover/rocq PublicThe Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…
-
Something went wrong, please refresh the page to try again.
If the problem persists, check the GitHub status page or contact support.
If the problem persists, check the GitHub status page or contact support.