molikto / Mlang
Licence: gpl-3.0
Towards changing things and see if it proofs
Stars: ✭ 57
Programming Languages
scala
5932 projects
Labels
Projects that are alternatives of or similar to Mlang
Typedefs
Programming language agnostic type construction language based on polynomials.
Stars: ✭ 337 (+491.23%)
Mutual labels: type-theory
types-and-programming-languages
Exercises from Benjamin Pierce's "Types and Programming Languages" textbook + extras!
Stars: ✭ 92 (+61.4%)
Mutual labels: type-theory
shapesafe
SHAPE/S∀F∃: static prover/type-checker for N-D array programming in Scala, a use case of intuitionistic type theory
Stars: ✭ 17 (-70.18%)
Mutual labels: type-theory
Pikelet
A friendly little systems language with first-class types. Very WIP! 🚧 🚧 🚧
Stars: ✭ 485 (+750.88%)
Mutual labels: type-theory
Isabelle-HoTT
An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle
Stars: ✭ 30 (-47.37%)
Mutual labels: type-theory
Datafun
Research on integrating datalog & lambda calculus via monotonicity types
Stars: ✭ 287 (+403.51%)
Mutual labels: type-theory
tt-in-cubical
Type Theory in Type Theory using Cubical Agda
Stars: ✭ 12 (-78.95%)
Mutual labels: type-theory
path semantics
A research project in path semantics, a re-interpretation of functions for expressing mathematics
Stars: ✭ 136 (+138.6%)
Mutual labels: type-theory
lplzoo
Fine-grain implementations of common lambda calculi in Haskell, tested with QuickCheck
Stars: ✭ 32 (-43.86%)
Mutual labels: type-theory
TypeTopology
Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.
Stars: ✭ 132 (+131.58%)
Mutual labels: type-theory
Cubicaltt
Experimental implementation of Cubical Type Theory
Stars: ✭ 461 (+708.77%)
Mutual labels: type-theory
SymmetryBookFormalization
Univalent mathematics in Agda
Stars: ✭ 117 (+105.26%)
Mutual labels: type-theory
Type-Theory
Lecture note on Lambda Calculus and Types for FLOLAC
Stars: ✭ 26 (-54.39%)
Mutual labels: type-theory
Write You A Haskell
Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
Stars: ✭ 3,064 (+5275.44%)
Mutual labels: type-theory
mlang
A cubical type theory implementation. features you might not found in Coq, Agda, Lean:
- structural record and sum types
- overlapping patterns, so you don't need a lemma to proof nat_plus_commutative
- cumulative universe with lift operator and universe/pi subtyping
see roadmap for details.
see library and tests folder for sample code. for example Brunerie Number
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].