Pinned Repositories
algaeff
🦠 Reusable components based on algebraic effects
algaett
🦠 An experimental elaborator for dependent type theory using effects and handlers
asai
🩺 A library for compiler diagnostics
cooltt
😎TT
mugen
♾️ A library for universe levels and universe polymorphism
redtt
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
sml-redprl
The People's Refinement Logic
sml-typed-abts
second-order abstract syntax
stagedtt
🪆 A Staged Type Theory
yuujinchou
👹 A library for hierarchical names and lexical scoping
RedPRL's Repositories
RedPRL/sml-redprl
The People's Refinement Logic
RedPRL/cooltt
😎TT
RedPRL/redtt
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
RedPRL/algaeff
🦠 Reusable components based on algebraic effects
RedPRL/stagedtt
🪆 A Staged Type Theory
RedPRL/asai
🩺 A library for compiler diagnostics
RedPRL/mugen
♾️ A library for universe levels and universe polymorphism
RedPRL/sml-typed-abts
second-order abstract syntax
RedPRL/algaett
🦠 An experimental elaborator for dependent type theory using effects and handlers
RedPRL/yuujinchou
👹 A library for hierarchical names and lexical scoping
RedPRL/kado
🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory
RedPRL/ocaml-bwd
🔙 Backward lists for OCaml
RedPRL/bantorra
📚 A library for managing libraries and resolving unit paths
RedPRL/sml-dependent-lcf
A library for the next generation of LCF refiners, with support for dependent refinement—Long Live the Anti-Realist Struggle!
RedPRL/agda-mugen
A formalization of the theory behind the mugen library
RedPRL/sml-final-pretty-printer
A Standard ML port of Christiansen, Darais and Ma's Final Pretty Printer
RedPRL/sml-cats
Some basic categorical & algebraic structures for Standard ML
RedPRL/sml-lcf
A general purpose library for writing Classic LCF-with-validations-style refiners. Deprecated in favor of https://github.com/RedPRL/sml-dependent-lcf
RedPRL/sml-parcom
The People’s Revolutionary Parser Commissariat
RedPRL/sml-telescopes
an abstract data type for telescopes
RedPRL/actions-ocaml
GitHub Action for red* OCaml packages
RedPRL/cmlex
CM-Lex: A lexer generator for Standard ML and Haskell
RedPRL/cmyacc
CM-Yacc: A parser generator for Standard ML and Haskell
RedPRL/redprl.github.io
Souce of RedPRL website
RedPRL/sml-json
Standard ML JSON lib using parcom.
RedPRL/sml-unparse
DEPRECATED. Use https://github.com/RedPRL/sml-final-pretty-printer instead.
RedPRL/sml-wpp
A Pretty Printer, based on Philip Wadler's "A prettier printer". DEPRECATED, use https://github.com/RedPRL/sml-final-pretty-printer instead.