RedPRL/sml-dependent-lcf RedPRL/sml-dependent-lcf

  • Stars
    star
    16
  • Rank 1,311,288 (Top 26 %)
  • Language Standard ML
  • Created about 9 years ago
  • Updated almost 7 years ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
RedPRL/sml-dependent-lcf
github

RedPRL

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

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

More Repositories

1

sml-redprl

The People's Refinement Logic
Standard ML
226
star
2

cooltt

😎TT
OCaml
217
star
3

redtt

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

algaeff

🦠 Reusable components based on algebraic effects
OCaml
47
star
5

stagedtt

🪆 A Staged Type Theory
OCaml
35
star
6

asai

🩺 A library for compiler diagnostics
OCaml
34
star
7

sml-typed-abts

second-order abstract syntax
Standard ML
31
star
8

algaett

🦠 An experimental elaborator for dependent type theory using effects and handlers
OCaml
30
star
9

yuujinchou

👹 A library for hierarchical names and lexical scoping
OCaml
26
star
10

mugen

♾️ A library for universe levels and universe polymorphism
OCaml
24
star
11

ocaml-bwd

🔙 Backward lists for OCaml
OCaml
19
star
12

kado

🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory
OCaml
18
star
13

bantorra

📚 A library for managing libraries and resolving unit paths
OCaml
17
star
14

agda-mugen

A formalization of the theory behind the mugen library
Agda
15
star
15

sml-final-pretty-printer

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

sml-cats

Some basic categorical & algebraic structures for Standard ML
Standard ML
9
star
17

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
5
star
18

sml-telescopes

an abstract data type for telescopes
Standard ML
1
star