mit-pdos / mcqcLinks
A Gallina compiler with C++17 as an intermediate representation
☆43Updated 4 years ago
Alternatives and similar repositories for mcqc
Users that are interested in mcqc are comparing it to the libraries listed below
Sorting:
- Gallina to Bedrock2 compilation toolkit☆65Updated 3 weeks ago
- Hoare Type Theory☆84Updated 7 months ago
- ☆56Updated last week
- Benchmark repository of polyglot effect handler examples☆34Updated 5 months ago
- Coq library for verified low-level programming☆61Updated 8 years ago
- Coq library for tactics, basic definitions, sets, maps☆51Updated last month
- LL(1) parser generator verified in Coq☆48Updated 6 years ago
- Inline, type safe X86-64 assembly programming in Agda☆69Updated 7 years ago
- A dependent type theory with user defined data types☆47Updated 4 years ago
- Racket Equivalence Graph Library☆19Updated 3 years ago
- Formalization of C++ for verification purposes.☆89Updated last week
- ☆38Updated 4 years ago
- The SAW core language.☆55Updated 4 years ago
- embedding MLIR in LEAN☆48Updated last year
- Reference type checker for the Lean theorem prover☆64Updated 8 years ago
- An enhanced unification algorithm for Coq☆58Updated 2 months ago
- Artifact for paper "When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism" (https://popl24.si…☆15Updated last year
- An Agda formalization of System F and the Brown-Palsberg self-interpreter☆26Updated 5 years ago
- A language-generic implementation of equality saturation in Haskell☆22Updated 7 years ago
- Convert Haskell source code to Coq source code.☆93Updated 7 months ago
- Best of POPL (BOP) Reading Group Memoirs☆67Updated 4 years ago
- Graded Dependent Type systems☆25Updated 2 years ago
- Based on paper by Greg Morrisett , TAL-0 is the design of a RISC-style typed assembly language which focuses on control-flow safety.☆23Updated 9 years ago
- A formalisation of the Calculus of Constructions☆70Updated last year
- An interactive theorem prover based on lambda-tree syntax☆98Updated 3 weeks ago
- A Seamless, Interactive Tactic Learner and Prover for Coq☆82Updated last month
- EGraphs in OCaml☆79Updated 2 years ago
- CN separation logic refinement type system for C☆44Updated last month
- Formalizations of Gradually Typed Languages in Agda☆59Updated last month
- A deterministic parser with fused lexing☆75Updated 2 years ago