Skip to content
@uwplse

UW PLSE

University of Washington Programming Languages and Software Engineering

Popular repositories Loading

  1. verdi verdi Public

    A framework for formally verifying distributed systems implementations in Coq

    Coq 589 56

  2. verdi-raft verdi-raft Public

    An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

    Coq 183 19

  3. tensat tensat Public

    Re-implementation of the TASO compiler using equality saturation

    Rust 121 18

  4. ruler ruler Public

    Rewrite Rule Inference Using Equality Saturation

    Rust 118 9

  5. Cassius Cassius Public

    A CSS specification and reasoning engine

    Racket 92 1

  6. herbgrind herbgrind Public

    A Valgrind tool for Herbie

    C 90 7

Repositories

Showing 10 of 75 repositories
  • bril Public Forked from sampsyo/bril

    an educational compiler intermediate representation

    uwplse/bril’s past year of commit activity
    Rust 0 MIT 238 0 0 Updated Nov 4, 2024
  • nightly-conf Public

    The public nightly server configuration

    uwplse/nightly-conf’s past year of commit activity
    1 8 0 2 Updated Oct 22, 2024
  • pumpkin-pi Public

    An extension to PUMPKIN PATCH with support for proof repair across type equivalences.

    uwplse/pumpkin-pi’s past year of commit activity
    Coq 49 MIT 9 28 (4 issues need help) 1 Updated Sep 18, 2024
  • potpie Public

    Proof Object Transformation, Preserving Imp Embeddings: the first proof compiler to be formally proven correct

    uwplse/potpie’s past year of commit activity
    Coq 15 1 0 0 Updated Aug 19, 2024
  • PUMPKIN-PATCH Public

    Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

    uwplse/PUMPKIN-PATCH’s past year of commit activity
    OCaml 51 MIT 2 45 1 Updated Jul 17, 2024
  • coq-plugin-lib Public

    Library of useful utility functions for Coq plugins

    uwplse/coq-plugin-lib’s past year of commit activity
    OCaml 13 MIT 5 12 3 Updated Jul 17, 2024
  • fix-to-elim Public

    Fixpoint to eliminator translation in Coq

    uwplse/fix-to-elim’s past year of commit activity
    Coq 3 MIT 5 4 2 Updated Jul 4, 2024
  • reincarnate-aec Public

    Reincarnate Artifact for ICFP 2018

    uwplse/reincarnate-aec’s past year of commit activity
    JavaScript 13 MIT 2 0 0 Updated Jun 24, 2024
  • ruler Public

    Rewrite Rule Inference Using Equality Saturation

    uwplse/ruler’s past year of commit activity
    Rust 118 MIT 9 3 5 Updated Jun 4, 2024
  • verdi Public

    A framework for formally verifying distributed systems implementations in Coq

    uwplse/verdi’s past year of commit activity
    Coq 589 BSD-2-Clause 56 5 0 Updated May 17, 2024
View all repositories