RedPRL

All

27 repositories

bantorra
Public
📚 A library for managing libraries and resolving unit paths
ocaml ocaml-library
OCaml
•
Apache License 2.0
•0•17•9•1•Updated Nov 21, 2025Nov 21, 2025
mugen
Public
♾️ A library for universe levels and universe polymorphism
ocaml proof-assistant type-theory ocaml-library
OCaml
•
Apache License 2.0
•1•36•1•1•Updated Nov 21, 2025Nov 21, 2025
yuujinchou
Public
👹 A library for hierarchical names and lexical scoping
algebraic-effects ocaml ocaml-library
OCaml
•
Apache License 2.0
•4•26•10•2•Updated Nov 21, 2025Nov 21, 2025
asai
Public
🩺 A library for compiler diagnostics
algebraic-effects ocaml error-handling diagnostics error-reporting
OCaml
•
Apache License 2.0
•2•52•24•3•Updated Nov 21, 2025Nov 21, 2025
algaett
Public
🦠 An experimental elaborator for dependent type theory using effects and handlers
algebraic-effects ocaml proof-assistant type-theory normalization-by-evaluation ocaml-program
OCaml
•
Apache License 2.0
•0•37•8•2•Updated Nov 21, 2025Nov 21, 2025
algaeff
Public
🦠 Reusable components based on algebraic effects
algebraic-effects ocaml ocaml-library
OCaml
•
Apache License 2.0
•1•51•3•2•Updated Nov 21, 2025Nov 21, 2025
ocaml-bwd
Public
🔙 Backward lists for OCaml
ocaml ocaml-library
OCaml
•
Apache License 2.0
•3•22•2•3•Updated Nov 21, 2025Nov 21, 2025
kado
Public
🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory
ocaml proof-assistant type-theory cubical-type-theory ocaml-library homotopy-type-theory
OCaml
•
Apache License 2.0
•1•21•4•1•Updated Nov 20, 2025Nov 20, 2025
cooltt
Public
😎TT
ocaml proof-assistant type-theory cubical-type-theory homotopy-type-theory ocaml-program
OCaml
•
Apache License 2.0
•14•241•28•6•Updated Nov 20, 2025Nov 20, 2025
redprl.github.io
Public
Souce of RedPRL website
HTML
•0•0•1•0•Updated Jun 5, 2025Jun 5, 2025
actions-ocaml
Public
GitHub Action for red* OCaml packages
ocaml github-actions
Apache License 2.0
•1•0•0•0•Updated Feb 6, 2025Feb 6, 2025
agda-mugen
Public
A formalization of the theory behind the mugen library
Agda
•1•19•4•1•Updated Jun 24, 2024Jun 24, 2024
stagedtt
Public
🪆 A Staged Type Theory
OCaml
•
Apache License 2.0
•1•35•2•2•Updated Sep 4, 2023Sep 4, 2023
sml-unparse
Public archive
DEPRECATED. Use https://github.com/RedPRL/sml-final-pretty-printer instead.
Standard ML
•0•0•0•0•Updated Aug 30, 2023Aug 30, 2023
sml-wpp
Public archive
A Pretty Printer, based on Philip Wadler's "A prettier printer". DEPRECATED, use https://github.com/RedPRL/sml-final-pretty-printer instead.
Standard ML
•
GNU Lesser General Public License v2.1
•5•0•0•0•Updated Aug 30, 2023Aug 30, 2023
sml-redprl
Public archive
The People's Refinement Logic
nuprl proof-assistant type-theory cubical-type-theory
Standard ML
•
MIT License
•18•229•7•0•Updated Jan 1, 2023Jan 1, 2023
redtt
Public
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
ocaml proof-assistant type-theory cubical-type-theory
OCaml
•
Apache License 2.0
•12•214•37•1•Updated Mar 25, 2022Mar 25, 2022
sml-typed-abts
Public
second-order abstract syntax
syntax binding abstract-syntax
Standard ML
•10•31•10•1•Updated Sep 15, 2021Sep 15, 2021
sml-dependent-lcf
Public
A library for the next generation of LCF refiners, with support for dependent refinement—Long Live the Anti-Realist Struggle!
proof-refinement lcf tactics refiner
Standard ML
•1•16•3•0•Updated Feb 13, 2018Feb 13, 2018
sml-final-pretty-printer
Public
A Standard ML port of Christiansen, Darais and Ma's Final Pretty Printer
pretty-print
Standard ML
•
MIT License
•0•11•1•0•Updated Jan 12, 2018Jan 12, 2018
sml-telescopes
Public
an abstract data type for telescopes
Standard ML
•1•1•0•0•Updated Dec 31, 2017Dec 31, 2017
cmyacc
Public
CM-Yacc: A parser generator for Standard ML and Haskell
Standard ML
•2•0•0•0•Updated Aug 10, 2017Aug 10, 2017
cmlex
Public
CM-Lex: A lexer generator for Standard ML and Haskell
Standard ML
•3•0•0•0•Updated Aug 10, 2017Aug 10, 2017
sml-cats
Public
Some basic categorical & algebraic structures for Standard ML
Standard ML
•0•9•0•0•Updated Jul 22, 2017Jul 22, 2017
sml-json
Public
Standard ML JSON lib using parcom.
Standard ML
•
MIT License
•0•0•0•0•Updated Jun 24, 2017Jun 24, 2017
sml-parcom
Public
The People’s Revolutionary Parser Commissariat
Standard ML
•9•1•0•0•Updated Jun 24, 2017Jun 24, 2017
sml-lcf
Public archive
A general purpose library for writing Classic LCF-with-validations-style refiners. Deprecated in favor of https://github.com/RedPRL/sml-dependent-lcf
Standard ML
•2•5•1•0•Updated Jun 18, 2017Jun 18, 2017