Alternatives and similar repositories for BrainCoqulus

Users that are interested in BrainCoqulus are comparing it to the libraries listed below

• mit-plv / rupicola
  Gallina to Bedrock2 compilation toolkit
  ☆54Updated this week
• maxsnew / modal-scheme
  A Scheme-like CBPV language with Racket Interoperability
  ☆39Updated last year
• chameco / bramble
  dependently-typed lisp with flexible compiler backends
  ☆27Updated 6 years ago
• mietek / epigram2
  Mirror of Epigram 2, by Conor McBride, et al.
  ☆48Updated 4 years ago
• rocq-community / dblib
  Coq library for working with de Bruijn indices [maintainer=@KevOrr]
  ☆30Updated 3 years ago
• csgordon / cayenne
  Resurrecting Lennart Augustsson's implementation of Cayenne
  ☆38Updated 11 years ago
• RobertHarper / TILT-Compiler
  Standard ML compiler based on typed intermediate languages.
  ☆48Updated 10 years ago
• UlfNorell / x86-agda
  Inline, type safe X86-64 assembly programming in Agda
  ☆69Updated 6 years ago
• dannypsnl / racket-llvm
  racket llvm C-API bindings
  ☆17Updated 5 months ago
• nick8325 / twee
  An equational theorem prover based on Knuth-Bendix completion
  ☆52Updated 2 months ago
• philnguyen / z3-rkt
  Racket bindings for Z3
  ☆24Updated 6 years ago
• reynir / Brainfuck
  Brainfuck formalized in Coq
  ☆26Updated 3 years ago
• dbp / funtal
  FunTAL: mixing a functional language with assembly.
  ☆40Updated 8 years ago
• WhatisRT / meta-cedille
  Minimalistic dependent type theory with syntactic metaprogramming
  ☆57Updated 11 months ago
• Saizan / miller
  Miller/pattern unification in Agda
  ☆65Updated 11 years ago
• SMLFamily / The-Mechanization-of-Standard-ML
  The Mechanization of Standard ML
  ☆73Updated 2 years ago
• melted / idris-chez
  An idris backend compiling to chez scheme
  ☆46Updated 7 years ago
• NoahStoryM / ctp
  Category Theory in Programming
  ☆12Updated last month
• granule-project / gerty
  A small implementation of graded modal dependent type theory. A younger cousin to Granule.
  ☆59Updated last year
• raphael-proust / cps-ssa
  Experiments about intermediate representations in compilers
  ☆25Updated 12 years ago
• CakeML / pure
  A verified compiler for a lazy functional language
  ☆36Updated 3 weeks ago
• Mtac2 / Mtac2
  ☆55Updated 2 months ago
• mmcqd / datatt
  A dependent type theory with user defined data types
  ☆46Updated 3 years ago
• effect-handlers / effect-handlers-bench
  Benchmark repository of polyglot effect handler examples
  ☆24Updated last month
• jsiek / gradual-typing-in-agda
  Formalizations of Gradually Typed Languages in Agda
  ☆57Updated 4 months ago
• jsiek / abstract-binding-trees
  Abstract binding trees (abstract syntax trees plus binders), as a library in Agda
  ☆75Updated 6 months ago
• rzrn / anders
  Anders: Cubical Type Checker
  ☆24Updated last year
• zaklogician / typical-antiphrasis
  Paradoxes of type theory, described didactically. With accompanying proofs in Agda.
  ☆39Updated 4 years ago
• ankitku / TAL0
  Based on paper by Greg Morrisett , TAL-0 is the design of a RISC-style typed assembly language which focuses on control-flow safety.
  ☆22Updated 8 years ago
• plum-umd / abstracting-definitional-interpreters
  Abstracting Definitional Interpreters
  ☆68Updated 7 years ago