Toy theorem prover based on the calculus of constructions
-
Updated
Aug 26, 2021 - OCaml
Toy theorem prover based on the calculus of constructions
🦠 An experimental elaborator for dependent type theory using effects and handlers
Fun plugin to play with the Gallina AST.
♾️ A library for universe levels and universe polymorphism
[WIP] A series of tutorials for lambda calculus
A experimental compiler from Kind (Core) to Coq
A logic-based library for correct-by-construction process modelling and composition.
Type checking, type inference, Church, Curry, polymorphe types, Unification theory, ... All type theory related
🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory
Various implementations of normalization by evaluation.
A simple type-theoretic language in OCaml: Mini-TT
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
😎TT
Add a description, image, and links to the type-theory topic page so that developers can more easily learn about it.
To associate your repository with the type-theory topic, visit your repo's landing page and select "manage topics."