Programming Languages and Verification Group at MIT CSAIL

All

29 repositories

spacetalk
Public
Lean
•0•0•0•0•Updated Dec 24, 2024Dec 24, 2024
coqutil
Public
Coq library for tactics, basic definitions, sets, maps
Coq
•
MIT License
•24•42•9•1•Updated Dec 23, 2024Dec 23, 2024
bedrock2
Public
A work-in-progress language and compiler for verified low-level programming
Coq
•
MIT License
•45•300•39•14•Updated Dec 23, 2024Dec 23, 2024
fiat-crypto
Public
Cryptographic Primitive Code Generation by Fiat
Coq
•
Other
•147•725•121•27•Updated Dec 18, 2024Dec 18, 2024
fiat2
Public
A high level language that will compile to bedrock2 using database-style techniques
Coq
•
MIT License
•3•3•0•0•Updated Dec 10, 2024Dec 10, 2024
rupicola
Public
Gallina to Bedrock2 compilation toolkit
coq
Coq
•
MIT License
•11•51•4•3•Updated Dec 10, 2024Dec 10, 2024
rewriter
Public
Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
Coq
•
Other
•21•22•6•1•Updated Dec 6, 2024Dec 6, 2024
cross-crypto
Public
Connecting computational and symbolic crypto models
Coq
•
MIT License
•22•8•3•0•Updated Nov 25, 2024Nov 25, 2024
fiat
Public
Mostly Automated Synthesis of Correct-by-Construction Programs
Coq
•
Other
•32•150•1•0•Updated Nov 20, 2024Nov 20, 2024
isolation
Public
Coq
•
GNU General Public License v3.0
•0•1•0•0•Updated Oct 15, 2024Oct 15, 2024
koika
Public
A core language for rule-based hardware design 🦑
semantics coq programming-languages formal-methods compilation hardware-description-language
Coq
•
GNU General Public License v3.0
•11•145•8•1•Updated Oct 13, 2024Oct 13, 2024
kami
Public
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
proof-assistant hardware-description-language hardware-verification coq bluespec
Coq
•
MIT License
•24•144•2•0•Updated Sep 23, 2024Sep 23, 2024
engine-bench
Public
Benchmarks for various proof engines
Coq
•
MIT License
•5•5•2•0•Updated Sep 18, 2024Sep 18, 2024
riscv-coq
Public
RISC-V Specification in Coq
Coq
•
BSD 3-Clause "New" or "Revised" License
•17•111•5•4•Updated Aug 7, 2024Aug 7, 2024
foundational-integration-verification-of-a-cryptographic-server
Public
http://adam.chlipala.net/papers/GarageDoorPLDI24/
0•0•0•0•Updated Apr 6, 2024Apr 6, 2024
softmul
Public
Proving that a system with software trap handlers for unimplemented instructions behaves as if they were implemented in hardware
Coq
•0•2•0•0•Updated Mar 19, 2024Mar 19, 2024
bbv
Public
Bedrock Bit Vector Library
Coq
•
MIT License
•23•27•4•3•Updated Mar 7, 2024Mar 7, 2024
riscv-semantics
Public
A formal semantics of the RISC-V ISA in Haskell
Haskell
•
BSD 3-Clause "New" or "Revised" License
•16•159•11•0•Updated Aug 13, 2023Aug 13, 2023
hemiola
Public
A Coq framework to support structural design and proof of hardware cache-coherence protocols
coq proof-assistant domain-specific-language cache-coherence hardware-verification
Coq
•
MIT License
•0•12•0•0•Updated May 7, 2022May 7, 2022
certifying-derivation-of-state-machines-from-coroutines
Public
Haskell
•
MIT License
•2•3•0•0•Updated Oct 30, 2021Oct 30, 2021
coq-ident-to-string
Public
Ltac2 wizardy to convert a gallina identifier to a coq string.
MIT License
•0•0•1•0•Updated Jan 15, 2021Jan 15, 2021
reification-by-parametricity
Public
Fast Setup for Proof by Reflection, in Two Lines of Ltac.
Mathematica
•
MIT License
•2•12•0•0•Updated Jan 12, 2021Jan 12, 2021
blog
Public
A blog for PLV and friends of PLV
CSS
•0•3•0•0•Updated Nov 15, 2020Nov 15, 2020
network-configurations
Public
Using Coq to derive network configurations from declarative policies
Coq
•
MIT License
•0•5•0•0•Updated Apr 30, 2019Apr 30, 2019
bedrock2-ci
Public
Continuous Integration for bedrock2
Makefile
•2•0•0•0•Updated Jun 27, 2018Jun 27, 2018
Fiat_matrix
Public
Coq
•
Other
•1•1•0•0•Updated Apr 26, 2018Apr 26, 2018
timl
Public
TiML: A Functional Programming Language with Time Complexity
functional-programming time-complexity standard-ml sml mlton
Standard ML
•6•75•2•0•Updated Aug 28, 2017Aug 28, 2017
bedrock
Public
Coq library for verified low-level programming
Coq
•
Other
•6•57•0•0•Updated Jun 15, 2017Jun 15, 2017
stencils
Public
A Coq library for verifying dependencies of stencil implementations
Coq
•
Other
•0•4•0•0•Updated May 29, 2016May 29, 2016