RedPRL

Repositories

• cooltt

  😎TT

  proof-assistant type-theory cubical-type-theory homotopy-type-theory
  OCaml Apache-2.0 7 85 21 2 Updated Mar 9, 2021

• redprl.github.io
  HTML 0 0 1 0 Updated Jun 17, 2020

• redtt

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

  proof-assistant type-theory cubical-type-theory
  OCaml Apache-2.0 11 176 67 (2 issues need help) 3 Updated Jan 10, 2020

• sml-redprl

  The People's Refinement Logic

  nuprl proof-assistant type-theory cubical-type-theory
  Standard ML MIT 18 215 12 0 Updated Nov 4, 2019

• sml-typed-abts

  second-order abstract syntax

  syntax binding abstract-syntax
  Standard ML 8 29 14 2 Updated Feb 26, 2018

• sml-dependent-lcf

  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 12 5 0 Updated Feb 13, 2018

• sml-final-pretty-printer

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

  pretty-print
  Standard ML MIT 0 9 1 0 Updated Jan 12, 2018

• sml-telescopes

  an abstract data type for telescopes
  Standard ML 1 1 1 0 Updated Dec 31, 2017

• cmyacc

  Forked from RobertHarper/cmyacc

  CM-Yacc: A parser generator for Standard ML and Haskell
  Standard ML 1 0 0 0 Updated Aug 10, 2017

• cmlex

  Forked from codeon/cmlex

  CM-Lex: A lexer generator for Standard ML and Haskell
  Standard ML 2 0 0 0 Updated Aug 10, 2017

• sml-cats

  Some basic categorical & algebraic structures for Standard ML
  Standard ML 0 10 0 0 Updated Jul 22, 2017

• sml-json

  Standard ML JSON lib using parcom.
  Standard ML MIT 0 0 0 0 Updated Jun 24, 2017

• sml-parcom

  Forked from standardml/parcom

  The People’s Revolutionary Parser Commissariat
  Standard ML 7 1 0 0 Updated Jun 24, 2017

• 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
  Standard ML 2 4 1 0 Updated Jun 18, 2017

• sml-unparse

  DEPRECATED. Use https://github.com/RedPRL/sml-final-pretty-printer instead.
  Standard ML 0 0 0 0 Updated Sep 22, 2016

• sml-wpp

  Forked from kfl/wpp

  A Pretty Printer, based on Philip Wadler's "A prettier printer". DEPRECATED, use https://github.com/RedPRL/sml-final-pretty-printer instead.
  Standard ML LGPL-2.1 4 0 0 0 Updated Sep 21, 2016