Skip to content

@uwplse UW PLSE

Change the repository type filter

All

    Repositories list

    75 repositories

    • outreach-dragon-curves

      Public
      JavaScript
      •
      MIT License
      •0•0•0•0•Updated Dec 7, 2024Dec 7, 2024

    • bril

      Public
      an educational compiler intermediate representation
      Rust
      •
      MIT License
      •241•0•0•0•Updated Nov 4, 2024Nov 4, 2024

    • nightly-conf

      Public
      The public nightly server configuration
      8•1•0•2•Updated Oct 22, 2024Oct 22, 2024

    • pumpkin-pi

      Public
      An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
      refactoringdependent-typestransportrepaircoq-pluginornamentsdevoidpumpkin-patchproof-reuseproof-repair
      Coq
      •
      MIT License
      •9•49•28•1•Updated Sep 18, 2024Sep 18, 2024

    • potpie

      Public
      Proof Object Transformation, Preserving Imp Embeddings: the first proof compiler to be formally proven correct
      Coq
      •1•15•0•0•Updated Aug 19, 2024Aug 19, 2024

    • PUMPKIN-PATCH

      Public
      Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
      coq-pluginproof-automationpumpkin-patchproof-repaircoq
      OCaml
      •
      MIT License
      •2•51•45•1•Updated Jul 17, 2024Jul 17, 2024

    • coq-plugin-lib

      Public
      Library of useful utility functions for Coq plugins
      librarycoqcoq-librarycoq-pluginpumpkin-patch
      OCaml
      •
      MIT License
      •5•13•12•3•Updated Jul 17, 2024Jul 17, 2024

    • fix-to-elim

      Public
      Fixpoint to eliminator translation in Coq
      coqcoq-pluginpumpkin-patchfixpointsinduction-principleseliminators
      Coq
      •
      MIT License
      •5•3•4•2•Updated Jul 4, 2024Jul 4, 2024

    • reincarnate-aec

      Public
      Reincarnate Artifact for ICFP 2018
      JavaScript
      •
      MIT License
      •2•13•0•0•Updated Jun 24, 2024Jun 24, 2024

    • ruler

      Public
      Rewrite Rule Inference Using Equality Saturation
      Rust
      •
      MIT License
      •9•119•3•5•Updated Jun 4, 2024Jun 4, 2024

    • verdi

      Public
      A framework for formally verifying distributed systems implementations in Coq
      distributed-systemscoq-librarycoqproofverdi
      Coq
      •
      BSD 2-Clause "Simplified" License
      •56•596•5•0•Updated May 17, 2024May 17, 2024

    • pl-hw-blog

      Public
      A blog project between Gus, Rachit, Sam Coward, and Zach Sisco.
      Astro
      •0•1•3•0•Updated Dec 18, 2023Dec 18, 2023

    • StructTact

      Public
      Coq utility and tactic library.
      coqcoq-librarytactics
      Coq
      •
      BSD 2-Clause "Simplified" License
      •8•21•10•0•Updated Dec 9, 2023Dec 9, 2023

    • verdi-raft

      Public
      An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
      distributed-systemskey-valueconsensusraftcoqproofverdi
      Coq
      •
      BSD 2-Clause "Simplified" License
      •19•187•14•1•Updated Dec 8, 2023Dec 8, 2023

    • cheerios

      Public
      Formally verified Coq serialization library with support for extraction to OCaml
      serializationcoqproofserialization-librarycoq-libraryocaml
      Coq
      •
      BSD 2-Clause "Simplified" License
      •5•23•0•0•Updated Oct 22, 2023Oct 22, 2023

    • szalinski

      Public
      Szalinski: A Tool for Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
      cadsynthesis3d-printingcompiler-optimization
      OpenSCAD
      •
      MIT License
      •4•45•12•0•Updated Jul 21, 2023Jul 21, 2023

    • incarnate

      Public
      incarnate project website
      HTML
      •0•0•0•0•Updated Jun 15, 2023Jun 15, 2023

    • Casper

      Public
      A compiler for automatically re-targeting sequential Java code to Apache Spark.
      javacompilerz3synthesissparkdafny
      Java
      •
      Other
      •5•50•2•0•Updated Jun 15, 2023Jun 15, 2023

    • Cassius

      Public
      A CSS specification and reasoning engine
      Racket
      •
      MIT License
      •1•91•1•0•Updated Feb 15, 2023Feb 15, 2023

    • dexter

      Public
      a compiler for re-writing image processing functions in C++ to Halide
      Java
      •
      MIT License
      •6•23•1•0•Updated Jan 28, 2023Jan 28, 2023

    • rake

      Public
      compiling DSLs to high-level hardware instructions
      Racket
      •4•22•1•0•Updated Nov 8, 2022Nov 8, 2022

    • herbgrind

      Public
      A Valgrind tool for Herbie
      C
      •
      GNU General Public License v3.0
      •7•90•7•1•Updated Oct 25, 2022Oct 25, 2022

    • aleph

      Public
      F#
      •
      MIT License
      •2•0•0•0•Updated Aug 30, 2022Aug 30, 2022

    • stng

      Public
      compiler for fortran stencils using verified lifting,
      C++
      •
      MIT License
      •4•17•4•1•Updated Apr 5, 2022Apr 5, 2022

    • gayatri-marlin

      Public
      Our changes to Marlin for Gayatri
      C
      •0•0•0•0•Updated Feb 3, 2022Feb 3, 2022

    • memsynth

      Public
      An advanced automated reasoning tool for memory consistency model specifications.
      racketrosette
      Alloy
      •
      BSD 2-Clause "Simplified" License
      •1•20•0•0•Updated Dec 6, 2021Dec 6, 2021

    • oddity

      Public
      A graphical, time-traveling debugger for distributed systems
      Clojure
      •1•32•9•3•Updated Nov 28, 2021Nov 28, 2021

    • magic

      Public
      Demystifying the magic of supertactics
      OCaml
      •6•12•8•0•Updated Nov 2, 2021Nov 2, 2021

    • pumpkin

      Public
      Public webpage for Pumpkin Patch
      HTML
      •0•1•0•0•Updated Aug 2, 2021Aug 2, 2021

    • tensat

      Public
      Re-implementation of the TASO compiler using equality saturation
      Rust
      •
      MIT License
      •19•121•2•0•Updated Jun 28, 2021Jun 28, 2021