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 576 55

  2. verdi-raft verdi-raft Public

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

    Coq 178 18

  3. tensat tensat Public

    Re-implementation of the TASO compiler using equality saturation

    Rust 111 18

  4. ruler ruler Public

    Rewrite Rule Inference Using Equality Saturation

    Rust 107 8

  5. Cassius Cassius Public

    A CSS specification and reasoning engine

    Racket 91 1

  6. herbgrind herbgrind Public

    A Valgrind tool for Herbie

    C 90 7

Repositories

Showing 10 of 75 repositories
  • 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 Jul 5, 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
  • coq-plugin-lib Public

    Library of useful utility functions for Coq plugins

    uwplse/coq-plugin-lib’s past year of commit activity
    OCaml 12 MIT 5 12 3 Updated Jul 4, 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 50 MIT 2 45 1 Updated Jul 3, 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
  • nightly-conf Public

    The public nightly server configuration

    uwplse/nightly-conf’s past year of commit activity
    1 6 0 1 Updated Jun 9, 2024
  • ruler Public

    Rewrite Rule Inference Using Equality Saturation

    uwplse/ruler’s past year of commit activity
    Rust 107 MIT 8 2 5 Updated Jun 4, 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 14 1 0 0 Updated Jun 1, 2024
  • bril Public Forked from sampsyo/bril

    an educational compiler intermediate representation

    uwplse/bril’s past year of commit activity
    Rust 0 MIT 192 0 0 Updated May 29, 2024
  • verdi Public

    A framework for formally verifying distributed systems implementations in Coq

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

Top languages

Loading…

Most used topics

Loading…