UW PLSE

University of Washington Programming Languages and Software Engineering

Seattle, WA

Pinned Repositories

Casper
A compiler for automatically re-targeting sequential Java code to Apache Spark.
Language:Java50 14 45
Cassius
A CSS specification and reasoning engine
Language:Racket91 51 31
crust
A compiler from Rust to C, and a checker for unsafe code
Language:Rust81 43 25
herbgrind
A Valgrind tool for Herbie
Language:C90 9 367
PUMPKIN-PATCH
Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
Language:OCaml51 10 632
pumpkin-pi
An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
Language:Coq49 11 579
ruler
Rewrite Rule Inference Using Equality Saturation
Language:Rust118 5 159
tensat
Re-implementation of the TASO compiler using equality saturation
Language:Rust121 9 718
verdi
A framework for formally verifying distributed systems implementations in Coq
Language:Coq592 67 2556
verdi-raft
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
Language:Coq183 55 1919

UW PLSE's Repositories

uwplse/verdi
A framework for formally verifying distributed systems implementations in Coq
Language:Coq592 67 2556
uwplse/verdi-raft
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
Language:Coq183 55 1919
uwplse/tensat
Re-implementation of the TASO compiler using equality saturation
Language:Rust121 9 718
uwplse/ruler
Rewrite Rule Inference Using Equality Saturation
Language:Rust118 5 159
uwplse/Cassius
A CSS specification and reasoning engine
Language:Racket91 51 31
uwplse/herbgrind
A Valgrind tool for Herbie
Language:C90 9 367
uwplse/PUMPKIN-PATCH
Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
Language:OCaml51 10 632
uwplse/Casper
A compiler for automatically re-targeting sequential Java code to Apache Spark.
Language:Java50 14 45
uwplse/pumpkin-pi
An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
Language:Coq49 11 579
uwplse/szalinski
Szalinski: A Tool for Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
Language:OpenSCAD45 7 214
uwplse/oddity
A graphical, time-traveling debugger for distributed systems
Language:Clojure32 6 271
uwplse/cheerios
Formally verified Coq serialization library with support for extraction to OCaml
Language:Coq23 30 55
uwplse/dexter
a compiler for re-writing image processing functions in C++ to Halide
Language:Java22 7 16
uwplse/rake
compiling DSLs to high-level hardware instructions
Language:Racket21 10 14
uwplse/StructTact
Coq utility and tactic library.
Language:Coq21 31 178
uwplse/memsynth
An advanced automated reasoning tool for memory consistency model specifications.
Language:Alloy20 7 01
uwplse/stng
compiler for fortran stencils using verified lifting,
Language:C++17 8 114
uwplse/potpie
Proof Object Transformation, Preserving Imp Embeddings: the first proof compiler to be formally proven correct
Language:Coq15 6 01
uwplse/coq-plugin-lib
Library of useful utility functions for Coq plugins
Language:OCaml13 7 255
uwplse/reincarnate-aec
Reincarnate Artifact for ICFP 2018
Language:JavaScript13 7 02
uwplse/magic
Demystifying the magic of supertactics
Language:OCaml12 7 86
uwplse/incarnate
incarnate project website
Language:HTML51
uwplse/fix-to-elim
Fixpoint to eliminator translation in Coq
Language:Coq3 5 105
uwplse/nightly-conf
The public nightly server configuration
19
uwplse/pl-hw-blog
A blog project between Gus, Rachit, Sam Coward, and Zach Sisco.
Language:Astro1 8 30
uwplse/pumpkin
Public webpage for Pumpkin Patch
Language:HTML1 8 0
uwplse/aleph
uwplse/bril
an educational compiler intermediate representation
Language:Rust0 01
uwplse/gayatri-marlin
Our changes to Marlin for Gayatri
Language:C
uwplse/outreach-dragon-curves
Language:Processing