Programming Languages and Verification Group at MIT CSAIL

MIT CSAIL, Building 32–G8

Pinned Repositories

bedrock
Coq library for verified low-level programming
Language:Coq57 10 06
bedrock2
A work-in-progress language and compiler for verified low-level programming
Language:Coq300 15 10745
fiat
Mostly Automated Synthesis of Correct-by-Construction Programs
Language:Coq151 9 1032
fiat-crypto
Cryptographic Primitive Code Generation by Fiat
Language:Coq730 51 412147
kami
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
Language:Coq145 14 925
koika
A core language for rule-based hardware design 🦑
Language:Coq146 24 2012
riscv-coq
RISC-V Specification in Coq
Language:Coq111 15 1217
riscv-semantics
A formal semantics of the RISC-V ISA in Haskell
Language:Haskell160 24 1716
rupicola
Gallina to Bedrock2 compilation toolkit
Language:Coq51 16 911
timl
TiML: A Functional Programming Language with Time Complexity
Language:Standard ML75 12 26

Programming Languages and Verification Group at MIT CSAIL's Repositories

mit-plv/fiat-crypto
Cryptographic Primitive Code Generation by Fiat
Language:Coq730 51 412147
mit-plv/bedrock2
A work-in-progress language and compiler for verified low-level programming
Language:Coq300 15 10745
mit-plv/riscv-semantics
A formal semantics of the RISC-V ISA in Haskell
Language:Haskell160 24 1716
mit-plv/fiat
Mostly Automated Synthesis of Correct-by-Construction Programs
Language:Coq151 9 1032
mit-plv/koika
A core language for rule-based hardware design 🦑
Language:Coq146 24 2012
mit-plv/kami
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
Language:Coq145 14 925
mit-plv/riscv-coq
RISC-V Specification in Coq
Language:Coq111 15 1217
mit-plv/timl
TiML: A Functional Programming Language with Time Complexity
Language:Standard ML75 12 26
mit-plv/bedrock
Coq library for verified low-level programming
Language:Coq57 10 06
mit-plv/rupicola
Gallina to Bedrock2 compilation toolkit
Language:Coq51 16 911
mit-plv/coqutil
Coq library for tactics, basic definitions, sets, maps
Language:Coq42 12 2524
mit-plv/bbv
Bedrock Bit Vector Library
Language:Coq27 16 1123
mit-plv/rewriter
Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
Language:Coq22 11 1421
mit-plv/hemiola
A Coq framework to support structural design and proof of hardware cache-coherence protocols
Language:Coq12 10 00
mit-plv/reification-by-parametricity
Fast Setup for Proof by Reflection, in Two Lines of Ltac.
Language:Mathematica12 12 02
mit-plv/cross-crypto
Connecting computational and symbolic crypto models
Language:Coq8 13 719
mit-plv/engine-bench
Benchmarks for various proof engines
Language:Coq5 10 35
mit-plv/network-configurations
Using Coq to derive network configurations from declarative policies
Language:Coq5 13 0
mit-plv/stencils
A Coq library for verifying dependencies of stencil implementations
Language:Coq4 8 0
mit-plv/blog
A blog for PLV and friends of PLV
Language:CSS3 12 1
mit-plv/certifying-derivation-of-state-machines-from-coroutines
Language:Haskell3 10 02
mit-plv/fiat2
A high level language that will compile to bedrock2 using database-style techniques
Language:Coq3 6 03
mit-plv/softmul
Proving that a system with software trap handlers for unimplemented instructions behaves as if they were implemented in hardware
Language:Coq2 4 0
mit-plv/Fiat_matrix
Language:Coq1 13 01
mit-plv/isolation
Language:Coq1 3 0
mit-plv/bedrock2-ci
Continuous Integration for bedrock2
Language:Makefile10 02
mit-plv/coq-ident-to-string
Ltac2 wizardy to convert a gallina identifier to a coq string.
12 1
mit-plv/foundational-integration-verification-of-a-cryptographic-server
http://adam.chlipala.net/papers/GarageDoorPLDI24/
4 0
mit-plv/spacetalk
Language:Lean3 0