Skip to content

@uwplse UW PLSE

Change the repository type filter

All

    Repositories list

    77 repositories

    • nightly-conf

      Public
      The public nightly server configuration
      11•1•0•0•Updated Nov 6, 2025Nov 6, 2025

    • szalinski

      Public
      Szalinski: A Tool for Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
      cadsynthesis3d-printingcompiler-optimization
      OpenSCAD
      •
      MIT License
      •4•53•12•0•Updated Sep 1, 2025Sep 1, 2025

    • pumpkin-pi

      Public
      An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
      refactoringdependent-typescoqtransportrepaircoq-pluginornamentsdevoidpumpkin-patchproof-reuse
      Coq
      •
      MIT License
      •9•49•28•1•Updated Aug 21, 2025Aug 21, 2025

    • dragoner-curves

      Public
      PLSE outreach activity on dragon curves and L-Systems!
      TypeScript
      •
      MIT License
      •0•1•0•0•Updated Jul 23, 2025Jul 23, 2025

    • verdi

      Public
      A framework for formally verifying distributed systems implementations in Coq
      distributed-systemscoqproofcoq-libraryverdi
      Rocq Prover
      •
      BSD 2-Clause "Simplified" License
      •56•609•5•0•Updated Jun 27, 2025Jun 27, 2025

    • ruler

      Public
      Rewrite Rule Inference Using Equality Saturation
      Rust
      •
      MIT License
      •14•142•5•9•Updated Jun 6, 2025Jun 6, 2025

    • retypeset-classics

      Public
      retyping old papers in modern notation
      TeX
      •0•0•0•0•Updated Jan 26, 2025Jan 26, 2025

    • bril

      Public
      an educational compiler intermediate representation
      Rust
      •
      MIT License
      •316•1•0•0•Updated Jan 24, 2025Jan 24, 2025

    • outreach-dragon-curves

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

    • potpie

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

    • PUMPKIN-PATCH

      Public
      Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
      coqcoq-pluginproof-automationpumpkin-patchproof-repair
      OCaml
      •
      MIT License
      •2•52•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

    • 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.
      coqtacticscoq-library
      Coq
      •
      BSD 2-Clause "Simplified" License
      •8•24•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-valueraftcoqproofconsensusverdi
      Coq
      •
      BSD 2-Clause "Simplified" License
      •19•191•14•1•Updated Dec 8, 2023Dec 8, 2023

    • cheerios

      Public
      Formally verified Coq serialization library with support for extraction to OCaml
      serializationocamlcoqproofserialization-librarycoq-library
      Coq
      •
      BSD 2-Clause "Simplified" License
      •5•24•0•0•Updated Oct 22, 2023Oct 22, 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.
      javasparkcompilerz3synthesisdafny
      Java
      •
      Other
      •5•50•2•0•Updated Jun 15, 2023Jun 15, 2023

    • Cassius

      Public
      A CSS specification and reasoning engine
      Racket
      •
      MIT License
      •1•97•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•24•1•0•Updated Jan 28, 2023Jan 28, 2023

    • rake

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

    • herbgrind

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

    • aleph

      Public
      F#
      •
      MIT License
      •3•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•25•0•0•Updated Dec 6, 2021Dec 6, 2021

    • oddity

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

    • magic

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