{"payload":{"pageCount":1,"repositories":[{"type":"Public","name":"riscv-coq","owner":"mit-plv","isFork":false,"description":"RISC-V Specification in Coq","allTopics":[],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":3,"issueCount":4,"starsCount":100,"forksCount":17,"license":"BSD 3-Clause \"New\" or \"Revised\" License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-08-06T17:41:55.038Z"}},{"type":"Public","name":"coqutil","owner":"mit-plv","isFork":false,"description":"Coq library for tactics, basic definitions, sets, maps","allTopics":[],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":1,"issueCount":8,"starsCount":41,"forksCount":24,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-08-06T16:24:38.540Z"}},{"type":"Public","name":"fiat2","owner":"mit-plv","isFork":false,"description":"A high level language that will compile to bedrock2 using database-style techniques","allTopics":[],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":0,"starsCount":2,"forksCount":3,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-08-06T15:15:46.820Z"}},{"type":"Public","name":"fiat-crypto","owner":"mit-plv","isFork":false,"description":"Cryptographic Primitive Code Generation by Fiat","allTopics":[],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":31,"issueCount":117,"starsCount":706,"forksCount":147,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-08-06T10:52:23.660Z"}},{"type":"Public","name":"spacetalk","owner":"mit-plv","isFork":false,"description":"","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-08-02T17:35:39.628Z"}},{"type":"Public","name":"bedrock2","owner":"mit-plv","isFork":false,"description":"A work-in-progress language and compiler for verified low-level programming","allTopics":[],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":12,"issueCount":36,"starsCount":289,"forksCount":43,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-31T20:25:30.052Z"}},{"type":"Public","name":"rewriter","owner":"mit-plv","isFork":false,"description":"Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting","allTopics":[],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":5,"starsCount":23,"forksCount":20,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-29T21:55:44.635Z"}},{"type":"Public","name":"rupicola","owner":"mit-plv","isFork":false,"description":"Gallina to Bedrock2 compilation toolkit","allTopics":["coq"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":1,"issueCount":4,"starsCount":51,"forksCount":11,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-17T08:03:12.101Z"}},{"type":"Public","name":"fiat","owner":"mit-plv","isFork":false,"description":"Mostly Automated Synthesis of Correct-by-Construction Programs","allTopics":[],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":1,"starsCount":145,"forksCount":30,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-05-09T17:19:42.661Z"}},{"type":"Public","name":"cross-crypto","owner":"mit-plv","isFork":true,"description":"Connecting computational and symbolic crypto models","allTopics":[],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":3,"starsCount":8,"forksCount":22,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-04-11T15:26:39.555Z"}},{"type":"Public","name":"foundational-integration-verification-of-a-cryptographic-server","owner":"mit-plv","isFork":false,"description":"<a href=\"http://adam.chlipala.net/papers/GarageDoorPLDI24/\" rel=\"nofollow\">http://adam.chlipala.net/papers/GarageDoorPLDI24/</a>","allTopics":[],"primaryLanguage":null,"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-04-06T21:15:44.199Z"}},{"type":"Public","name":"softmul","owner":"mit-plv","isFork":false,"description":"Proving that a system with software trap handlers for unimplemented instructions behaves as if they were implemented in hardware","allTopics":[],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":0,"starsCount":2,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-03-19T04:32:08.220Z"}},{"type":"Public","name":"bbv","owner":"mit-plv","isFork":false,"description":"Bedrock Bit Vector Library","allTopics":[],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":2,"issueCount":4,"starsCount":27,"forksCount":23,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-03-07T16:56:37.426Z"}},{"type":"Public","name":"kami","owner":"mit-plv","isFork":false,"description":"A Platform for High-Level Parametric Hardware Specification and its Modular Verification","allTopics":["proof-assistant","hardware-description-language","hardware-verification","coq","bluespec"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":2,"starsCount":141,"forksCount":24,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-02-29T18:00:16.517Z"}},{"type":"Public","name":"koika","owner":"mit-plv","isFork":false,"description":"A core language for rule-based hardware design 🦑","allTopics":["semantics","coq","programming-languages","formal-methods","compilation","hardware-description-language"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":8,"starsCount":137,"forksCount":9,"license":"GNU General Public License v3.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-09-18T01:30:04.240Z"}},{"type":"Public","name":"riscv-semantics","owner":"mit-plv","isFork":false,"description":"A formal semantics of the RISC-V ISA in Haskell","allTopics":[],"primaryLanguage":{"name":"Haskell","color":"#5e5086"},"pullRequestCount":0,"issueCount":11,"starsCount":148,"forksCount":15,"license":"BSD 3-Clause \"New\" or \"Revised\" License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-08-13T00:03:11.094Z"}},{"type":"Public","name":"engine-bench","owner":"mit-plv","isFork":false,"description":"Benchmarks for various proof engines","allTopics":[],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":2,"starsCount":5,"forksCount":5,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2022-08-22T19:29:09.478Z"}},{"type":"Public","name":"hemiola","owner":"mit-plv","isFork":false,"description":"A Coq framework to support structural design and proof of hardware cache-coherence protocols","allTopics":["coq","proof-assistant","domain-specific-language","cache-coherence","hardware-verification"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":0,"starsCount":11,"forksCount":0,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2022-05-07T04:43:04.926Z"}},{"type":"Public","name":"certifying-derivation-of-state-machines-from-coroutines","owner":"mit-plv","isFork":false,"description":"","allTopics":[],"primaryLanguage":{"name":"Haskell","color":"#5e5086"},"pullRequestCount":0,"issueCount":0,"starsCount":3,"forksCount":2,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2021-10-30T06:48:32.328Z"}},{"type":"Public","name":"coq-ident-to-string","owner":"mit-plv","isFork":false,"description":"Ltac2 wizardy to convert a gallina identifier to a coq string.","allTopics":[],"primaryLanguage":null,"pullRequestCount":0,"issueCount":1,"starsCount":0,"forksCount":0,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2021-01-15T18:33:05.959Z"}},{"type":"Public","name":"reification-by-parametricity","owner":"mit-plv","isFork":false,"description":"Fast Setup for Proof by Reflection, in Two Lines of Ltac.","allTopics":[],"primaryLanguage":{"name":"Mathematica","color":"#dd1100"},"pullRequestCount":0,"issueCount":0,"starsCount":11,"forksCount":2,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2021-01-12T20:26:12.719Z"}},{"type":"Public","name":"blog","owner":"mit-plv","isFork":false,"description":"A blog for PLV and friends of PLV","allTopics":[],"primaryLanguage":{"name":"CSS","color":"#563d7c"},"pullRequestCount":0,"issueCount":0,"starsCount":3,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2020-11-15T13:56:06.661Z"}},{"type":"Public","name":"network-configurations","owner":"mit-plv","isFork":false,"description":"Using Coq to derive network configurations from declarative policies","allTopics":[],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":0,"starsCount":4,"forksCount":0,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2019-04-30T03:07:36.283Z"}},{"type":"Public","name":"bedrock2-ci","owner":"mit-plv","isFork":false,"description":"Continuous Integration for bedrock2","allTopics":[],"primaryLanguage":{"name":"Makefile","color":"#427819"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":2,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2018-06-27T07:22:00.483Z"}},{"type":"Public","name":"Fiat_matrix","owner":"mit-plv","isFork":false,"description":"","allTopics":[],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":1,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2018-04-26T13:23:10.930Z"}},{"type":"Public","name":"timl","owner":"mit-plv","isFork":false,"description":"TiML: A Functional Programming Language with Time Complexity","allTopics":["functional-programming","time-complexity","standard-ml","sml","mlton"],"primaryLanguage":{"name":"Standard ML","color":"#dc566d"},"pullRequestCount":0,"issueCount":2,"starsCount":75,"forksCount":6,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2017-08-28T14:45:28.447Z"}},{"type":"Public","name":"bedrock","owner":"mit-plv","isFork":false,"description":"Coq library for verified low-level programming","allTopics":[],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":0,"starsCount":57,"forksCount":6,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2017-06-15T16:33:52.312Z"}},{"type":"Public","name":"stencils","owner":"mit-plv","isFork":false,"description":"A Coq library for verifying dependencies of stencil implementations","allTopics":[],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":0,"starsCount":4,"forksCount":0,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2016-05-29T20:29:06.097Z"}}],"repositoryCount":28,"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":"mit-plv repositories"}