saki-lang/saki-dev

A simple scala-like dependent type programming language

Language: Scala - Size: 605 KB - Last synced at: 4 days ago - Pushed at: 5 days ago - Stars: 17 - Forks: 2

yiyunliu/mltt-consistency

Logical relation for predicative CC omega with booleans and an intensional identity type

Language: TeX - Size: 7.93 MB - Last synced at: 3 days ago - Pushed at: about 2 months ago - Stars: 12 - Forks: 2

GrahamStrickland/math_lean

Examples and exercises from "Mathematics in Lean" - Jeremy Avigad & Patrick Massot

Language: Lean - Size: 16.6 KB - Last synced at: 14 days ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 0

smimram/decaml

Dependent variant of OCaml

Language: OCaml - Size: 181 KB - Last synced at: 7 days ago - Pushed at: about 1 month ago - Stars: 4 - Forks: 0

forked-from-1kasper/anders

Anders: Cubical Type Checker

Language: OCaml - Size: 4.02 MB - Last synced at: 19 days ago - Pushed at: over 1 year ago - Stars: 24 - Forks: 1

gfngfn/lw-staged-deptype

Language: Haskell - Size: 542 KB - Last synced at: 15 days ago - Pushed at: about 2 months ago - Stars: 3 - Forks: 0

mtumilowicz/scala3-dependent-types-polymorphic-functions-workshop

Introduction to typelevel programming: phantom types, dependent types, path dependent types and Curry-Howard isomorphism.

Language: Scala - Size: 324 KB - Last synced at: about 2 months ago - Pushed at: 3 months ago - Stars: 1 - Forks: 0

forked-from-1kasper/hurricane

Hurricane: HoTT-I Type System

Language: OCaml - Size: 44.9 KB - Last synced at: about 2 months ago - Pushed at: about 3 years ago - Stars: 1 - Forks: 0

GrahamStrickland/functional_lean

Examples and exercises from "Functional Programming in Lean" - David Thrane Christiansen

Language: Lean - Size: 31.3 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0

cicada-lang/cicada-plct

Cicada Language (PLCT little team)

Language: TypeScript - Size: 2.51 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 92 - Forks: 7

cicada-lang/cicada-solo

Cicada Language (solo version)

Language: TypeScript - Size: 6.83 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 128 - Forks: 5

williamdemeo/agda-algebras Fork of ualib/agda-algebras

The Agda Universal Algebra Library (html docs available at the url below)

Language: Agda - Size: 54.5 MB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 1 - Forks: 1

fredrik-bakke/forest

Language: Shell - Size: 1.14 MB - Last synced at: 9 days ago - Pushed at: 6 months ago - Stars: 3 - Forks: 0

Russoul/Nova

A programming language based on extensional Martin Lof Type Theory

Language: Idris - Size: 377 KB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 1 - Forks: 0

lunalunaa/pi-forall-kt

A dependently typed programming language

Language: Kotlin - Size: 151 KB - Last synced at: over 1 year ago - Pushed at: over 3 years ago - Stars: 4 - Forks: 0

xieyuheng/x-json

A dependently typed programming language embedded in JSON, that can be used as a schema checker for JSON data.

Language: TypeScript - Size: 70.3 KB - Last synced at: 21 days ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

ReubenHillyard/alpha

Type-checking and type-inference for a spartan dependent type theory.

Language: Rust - Size: 13.7 KB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0

jaycech3n/Isabelle-Spartan 📦

A dependent type theory logic for Isabelle

Language: Standard ML - Size: 361 KB - Last synced at: almost 2 years ago - Pushed at: about 4 years ago - Stars: 6 - Forks: 1

AD1024/dtlc

Dependently typed lambda calculus - A Simple Proof Assistant

Language: OCaml - Size: 58.6 KB - Last synced at: about 2 years ago - Pushed at: over 4 years ago - Stars: 8 - Forks: 0