{"payload":{"pageCount":3,"repositories":[{"type":"Public","name":"nightly-conf","owner":"uwplse","isFork":false,"description":"The public nightly server configuration","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":null,"pullRequestCount":1,"issueCount":0,"starsCount":1,"forksCount":6,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-05-16T16:40:42.467Z"}},{"type":"Public","name":"bril","owner":"uwplse","isFork":true,"description":"an educational compiler intermediate representation","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Rust","color":"#dea584"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":187,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-05-15T20:39:49.733Z"}},{"type":"Public","name":"outreach-dragon-curves","owner":"uwplse","isFork":false,"description":"","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Processing","color":"#0096D8"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-04-26T17:52:01.007Z"}},{"type":"Public","name":"pumpkin-pi","owner":"uwplse","isFork":false,"description":"An extension to PUMPKIN PATCH with support for proof repair across type equivalences.","topicNames":["refactoring","dependent-types","transport","repair","coq-plugin","ornaments","devoid","pumpkin-patch","proof-reuse","proof-repair"],"topicsNotShown":6,"allTopics":["refactoring","dependent-types","transport","repair","coq-plugin","ornaments","devoid","pumpkin-patch","proof-reuse","proof-repair","pumpkin-pi","proof-refactoring","proof-assistants","coq","algebraic-ornaments","equivalences"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":28,"starsCount":49,"forksCount":9,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-04-24T22:39:31.236Z"}},{"type":"Public","name":"potpie","owner":"uwplse","isFork":false,"description":"Proof Object Transformation, Preserving Imp Embeddings: the first proof compiler to be formally proven correct","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":0,"starsCount":13,"forksCount":1,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-03-18T04:14:15.750Z"}},{"type":"Public","name":"pl-hw-blog","owner":"uwplse","isFork":false,"description":"A blog project between Gus, Rachit, Sam Coward, and Zach Sisco.","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Astro","color":"#ff5a03"},"pullRequestCount":0,"issueCount":3,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-12-18T23:22:39.121Z"}},{"type":"Public","name":"StructTact","owner":"uwplse","isFork":false,"description":"Coq utility and tactic library.","topicNames":["coq","coq-library","tactics"],"topicsNotShown":0,"allTopics":["coq","coq-library","tactics"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":10,"starsCount":21,"forksCount":8,"license":"BSD 2-Clause \"Simplified\" License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-12-09T16:22:26.465Z"}},{"type":"Public","name":"verdi-raft","owner":"uwplse","isFork":false,"description":"An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework","topicNames":["distributed-systems","key-value","consensus","raft","coq","proof","verdi"],"topicsNotShown":0,"allTopics":["distributed-systems","key-value","consensus","raft","coq","proof","verdi"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":1,"issueCount":14,"starsCount":178,"forksCount":18,"license":"BSD 2-Clause \"Simplified\" License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-12-08T14:05:25.697Z"}},{"type":"Public","name":"verdi","owner":"uwplse","isFork":false,"description":"A framework for formally verifying distributed systems implementations in Coq","topicNames":["distributed-systems","coq-library","coq","proof","verdi"],"topicsNotShown":0,"allTopics":["distributed-systems","coq-library","coq","proof","verdi"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":5,"starsCount":575,"forksCount":55,"license":"BSD 2-Clause \"Simplified\" License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-12-08T13:45:45.490Z"}},{"type":"Public","name":"ruler","owner":"uwplse","isFork":false,"description":"Rewrite Rule Inference Using Equality Saturation","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Rust","color":"#dea584"},"pullRequestCount":5,"issueCount":2,"starsCount":103,"forksCount":8,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-10-25T19:27:56.917Z"}},{"type":"Public","name":"cheerios","owner":"uwplse","isFork":false,"description":"Formally verified Coq serialization library with support for extraction to OCaml","topicNames":["serialization","coq","proof","serialization-library","coq-library","ocaml"],"topicsNotShown":0,"allTopics":["serialization","coq","proof","serialization-library","coq-library","ocaml"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":0,"starsCount":23,"forksCount":5,"license":"BSD 2-Clause \"Simplified\" License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-10-22T09:38:02.089Z"}},{"type":"Public","name":"szalinski","owner":"uwplse","isFork":false,"description":"Szalinski: A Tool for Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations ","topicNames":["cad","synthesis","3d-printing","compiler-optimization"],"topicsNotShown":0,"allTopics":["cad","synthesis","3d-printing","compiler-optimization"],"primaryLanguage":{"name":"OpenSCAD","color":"#e5cd45"},"pullRequestCount":0,"issueCount":12,"starsCount":41,"forksCount":4,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-07-21T07:09:36.968Z"}},{"type":"Public","name":"incarnate","owner":"uwplse","isFork":false,"description":"incarnate project website","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"HTML","color":"#e34c26"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-06-15T14:30:35.967Z"}},{"type":"Public","name":"Casper","owner":"uwplse","isFork":false,"description":"A compiler for automatically re-targeting sequential Java code to Apache Spark.","topicNames":["java","compiler","z3","synthesis","spark","dafny"],"topicsNotShown":0,"allTopics":["java","compiler","z3","synthesis","spark","dafny"],"primaryLanguage":{"name":"Java","color":"#b07219"},"pullRequestCount":0,"issueCount":2,"starsCount":49,"forksCount":5,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-06-15T05:03:03.493Z"}},{"type":"Public","name":"Cassius","owner":"uwplse","isFork":false,"description":"A CSS specification and reasoning engine","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Racket","color":"#3c5caa"},"pullRequestCount":0,"issueCount":1,"starsCount":90,"forksCount":1,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-02-15T04:34:28.446Z"}},{"type":"Public","name":"dexter","owner":"uwplse","isFork":false,"description":"a compiler for re-writing image processing functions in C++ to Halide","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Java","color":"#b07219"},"pullRequestCount":0,"issueCount":1,"starsCount":22,"forksCount":6,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-01-28T22:15:43.898Z"}},{"type":"Public","name":"rake","owner":"uwplse","isFork":false,"description":"compiling DSLs to high-level hardware instructions","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Racket","color":"#3c5caa"},"pullRequestCount":0,"issueCount":1,"starsCount":18,"forksCount":4,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2022-11-08T00:50:35.078Z"}},{"type":"Public","name":"fix-to-elim","owner":"uwplse","isFork":false,"description":"Fixpoint to eliminator translation in Coq","topicNames":["coq","coq-plugin","pumpkin-patch","fixpoints","induction-principles","eliminators"],"topicsNotShown":0,"allTopics":["coq","coq-plugin","pumpkin-patch","fixpoints","induction-principles","eliminators"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":1,"issueCount":4,"starsCount":3,"forksCount":5,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2022-11-03T20:09:09.893Z"}},{"type":"Public","name":"coq-plugin-lib","owner":"uwplse","isFork":false,"description":"Library of useful utility functions for Coq plugins","topicNames":["library","coq","coq-library","coq-plugin","pumpkin-patch"],"topicsNotShown":0,"allTopics":["library","coq","coq-library","coq-plugin","pumpkin-patch"],"primaryLanguage":{"name":"OCaml","color":"#ef7a08"},"pullRequestCount":2,"issueCount":12,"starsCount":11,"forksCount":5,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2022-11-03T20:07:52.617Z"}},{"type":"Public","name":"herbgrind","owner":"uwplse","isFork":false,"description":"A Valgrind tool for Herbie","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"C","color":"#555555"},"pullRequestCount":1,"issueCount":7,"starsCount":91,"forksCount":7,"license":"GNU General Public License v3.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2022-10-25T12:32:43.182Z"}},{"type":"Public","name":"aleph","owner":"uwplse","isFork":true,"description":"","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"F#","color":"#b845fc"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":2,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2022-08-30T17:27:17.735Z"}},{"type":"Public","name":"stng","owner":"uwplse","isFork":false,"description":"compiler for fortran stencils using verified lifting,","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"C++","color":"#f34b7d"},"pullRequestCount":1,"issueCount":4,"starsCount":17,"forksCount":4,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2022-04-05T05:01:59.370Z"}},{"type":"Public","name":"gayatri-marlin","owner":"uwplse","isFork":false,"description":"Our changes to Marlin for Gayatri","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"C","color":"#555555"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2022-02-03T06:34:36.666Z"}},{"type":"Public","name":"memsynth","owner":"uwplse","isFork":false,"description":"An advanced automated reasoning tool for memory consistency model specifications. ","topicNames":["racket","rosette"],"topicsNotShown":0,"allTopics":["racket","rosette"],"primaryLanguage":{"name":"Alloy","color":"#64C800"},"pullRequestCount":0,"issueCount":0,"starsCount":19,"forksCount":1,"license":"BSD 2-Clause \"Simplified\" License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2021-12-06T19:18:25.990Z"}},{"type":"Public","name":"oddity","owner":"uwplse","isFork":false,"description":"A graphical, time-traveling debugger for distributed systems","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Clojure","color":"#db5855"},"pullRequestCount":3,"issueCount":9,"starsCount":32,"forksCount":1,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2021-11-28T22:12:53.882Z"}},{"type":"Public","name":"magic","owner":"uwplse","isFork":false,"description":"Demystifying the magic of supertactics","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"OCaml","color":"#ef7a08"},"pullRequestCount":0,"issueCount":8,"starsCount":13,"forksCount":6,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2021-11-02T01:47:12.422Z"}},{"type":"Public","name":"PUMPKIN-PATCH","owner":"uwplse","isFork":false,"description":"Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker","topicNames":["coq-plugin","proof-automation","pumpkin-patch","proof-repair","coq"],"topicsNotShown":0,"allTopics":["coq-plugin","proof-automation","pumpkin-patch","proof-repair","coq"],"primaryLanguage":{"name":"OCaml","color":"#ef7a08"},"pullRequestCount":0,"issueCount":45,"starsCount":50,"forksCount":2,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2021-09-02T21:01:30.280Z"}},{"type":"Public","name":"pumpkin","owner":"uwplse","isFork":false,"description":"Public webpage for Pumpkin Patch","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"HTML","color":"#e34c26"},"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2021-08-02T18:55:53.628Z"}},{"type":"Public","name":"tensat","owner":"uwplse","isFork":false,"description":"Re-implementation of the TASO compiler using equality saturation","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Rust","color":"#dea584"},"pullRequestCount":0,"issueCount":2,"starsCount":108,"forksCount":17,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2021-06-28T16:22:03.392Z"}},{"type":"Public","name":"univalent-rewrites","owner":"uwplse","isFork":false,"description":"POPL 2020 PUMPKIN/DEVOID submission","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"TeX","color":"#3D6117"},"pullRequestCount":0,"issueCount":0,"starsCount":2,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2021-05-12T03:15:34.790Z"}}],"repositoryCount":75,"userInfo":null,"searchable":true,"definitions":[],"typeFilters":[{"id":"all","text":"All"},{"id":"public","text":"Public"},{"id":"source","text":"Sources"},{"id":"fork","text":"Forks"},{"id":"archived","text":"Archived"},{"id":"template","text":"Templates"}],"compactMode":false},"title":"Repositories"}