UW PLSE

Repositories

• pumpkin-pi

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

  refactoring dependent-types coq transport repair coq-plugin ornaments
  Coq MIT 5 36 27 (4 issues need help) 2 Updated Oct 30, 2020

• coq-plugin-lib

  Library of useful utility functions for Coq plugins

  library coq coq-library coq-plugin pumpkin-patch
  OCaml MIT 1 4 11 1 Updated Oct 30, 2020

• herbie

  Optimize floating-point expressions for accuracy

  racket developer-tools synthesis numerical-methods floating-point herbie
  HTML 22 436 9 0 Updated Oct 30, 2020

• Cassius

  A CSS specification and reasoning engine
  Racket MIT 1 69 0 1 Updated Oct 22, 2020

• tamago

  Re-implementation of the TASO compiler using equality saturation
  Rust MIT 3 12 0 0 Updated Oct 11, 2020

• fix-to-elim

  Fixpoint to eliminator translation in Coq

  coq coq-plugin pumpkin-patch fixpoints induction-principles eliminators
  Coq MIT 1 2 4 0 Updated Oct 9, 2020

• PUMPKIN-PATCH

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

  coq coq-plugin proof-automation pumpkin-patch proof-repair
  OCaml MIT 0 31 45 0 Updated Sep 29, 2020

• taso

  Forked from yycdavid/taso
  C++ Apache-2.0 1 0 0 0 Updated Sep 18, 2020

• szalinski

  Szalinski: A Tool for Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations

  cad synthesis 3d-printing compiler-optimization
  OpenSCAD MIT 0 10 13 0 Updated Sep 13, 2020

• theia

  Automatically Visualizing Program Execution
  OCaml MIT 1 4 0 5 Updated Sep 8, 2020

• herbgrind

  A Valgrind tool for Herbie
  C GPL-3.0 5 55 3 1 Updated Aug 19, 2020

• dexter

  a compiler for re-writing image processing functions in C++ to Halide
  Java MIT 1 7 1 0 Updated Aug 19, 2020

• scout

  Using High-Level Design Constraints to Automatically Generate Design Alternatives
  Jupyter Notebook MIT 0 1 9 9 Updated Aug 2, 2020

• oddity

  A graphical, time-traveling debugger for distributed systems
  Clojure 0 24 8 3 Updated Jul 30, 2020

• seguard-resources

  SeGuard Public Resources
  HTML Apache-2.0 2 2 1 1 Updated Jul 1, 2020

• verdi-raft

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

  distributed-systems key-value raft coq proof consensus verdi
  Coq BSD-2-Clause 16 140 14 0 Updated Jun 22, 2020

• verdi

  A framework for formally verifying distributed systems implementations in Coq

  distributed-systems coq proof coq-library verdi
  Coq BSD-2-Clause 47 490 5 0 Updated Jun 15, 2020

• StructTact

  Coq utility and tactic library.

  coq tactics coq-library
  Coq BSD-2-Clause 5 18 10 0 Updated Jun 8, 2020

• majortom

  An Oddity shim for "arbitrary" x86-64 Linux binaries
  Rust 0 1 0 0 Updated May 8, 2020

• analytics-data
  Coq 0 1 0 0 Updated May 1, 2020

• timing-with-tvm-for-remy
  Dockerfile 0 0 0 1 Updated Apr 16, 2020

• reincarnate-aec

  Reincarnate Artifact for ICFP 2018
  JavaScript MIT 1 5 0 0 Updated Apr 15, 2020

• epics-tools

  Static analysis tools for EPICS
  Haskell 0 1 0 0 Updated Apr 4, 2020

• pumpkin

  Public webpage for Pumpkin Patch
  HTML 0 1 0 0 Updated Feb 8, 2020

• cheerios

  Formally verified Coq serialization library with support for extraction to OCaml

  serialization ocaml coq proof serialization-library coq-library
  Coq 2 19 0 0 Updated Jan 31, 2020

• coq-change-analytics

  REPLICA: REPL Instrumentation for Coq Analysis

  analytics analysis repl coq replica user-study coq-plugin
  Python LGPL-2.1 0 3 2 0 Updated Jan 2, 2020

• CoqAST

  Fun plugin to play with the Gallina AST.
  OCaml 7 26 2 0 Updated Oct 3, 2019

• iag-synthesis

  Parallel, incremental evaluation of attribute grammars through synthesis
  HTML 2 4 6 0 Updated Sep 26, 2019

• crust

  A compiler from Rust to C, and a checker for unsafe code
  Rust 4 57 2 0 Updated Sep 24, 2019

• oeuf

  gallina frontend for CompCert
  Coq 2 17 0 0 Updated Jul 6, 2019