Explore @RedPRL Open Source projects

@RedPRL

RedPRL

Stars
962
Global Org. Rank 15,743 (Top 6 %)
Registered almost 9 years ago
Most used languages

OCaml
57.9 %

Standard ML 36.8 %

Agda 5.3 %

sml-redprl

The People's Refinement Logic

cooltt

redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory

algaeff

🦠 Reusable components based on algebraic effects

stagedtt

🪆 A Staged Type Theory

asai

🩺 A library for compiler diagnostics

sml-typed-abts

second-order abstract syntax

algaett

🦠 An experimental elaborator for dependent type theory using effects and handlers

yuujinchou

👹 A library for hierarchical names and lexical scoping

mugen

♾️ A library for universe levels and universe polymorphism

ocaml-bwd

🔙 Backward lists for OCaml

kado

🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory

bantorra

📚 A library for managing libraries and resolving unit paths

sml-dependent-lcf

A library for the next generation of LCF refiners, with support for dependent refinement—Long Live the Anti-Realist Struggle!

agda-mugen

A formalization of the theory behind the mugen library

sml-final-pretty-printer

A Standard ML port of Christiansen, Darais and Ma's Final Pretty Printer

sml-cats

Some basic categorical & algebraic structures for Standard ML

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

sml-telescopes

an abstract data type for telescopes