steshaw/plt

Programming Language Theory λΠ

Language: CSS - Size: 217 KB - Last synced at: about 10 hours ago - Pushed at: 5 months ago - Stars: 5,291 - Forks: 340

HigherOrderCO/Kind

A modern proof language

Language: Haskell - Size: 34.6 MB - Last synced at: about 3 hours ago - Pushed at: 4 months ago - Stars: 3,670 - Forks: 146

sdiehl/write-you-a-haskell

Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)

Language: Haskell - Size: 938 KB - Last synced at: about 1 month ago - Pushed at: over 4 years ago - Stars: 3,375 - Forks: 256

agda/agda

Agda is a dependently typed programming language / interactive theorem prover.

Language: Haskell - Size: 147 MB - Last synced at: about 6 hours ago - Pushed at: about 11 hours ago - Stars: 2,630 - Forks: 370

leanprover/lean3 📦

Lean Theorem Prover

Language: C++ - Size: 50.3 MB - Last synced at: 13 days ago - Pushed at: over 1 year ago - Stars: 2,151 - Forks: 217

HoTT/Coq-HoTT

A Coq library for Homotopy Type Theory

Language: Coq - Size: 26.3 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 1,310 - Forks: 196

pikelet-lang/pikelet

A friendly little systems language with first-class types. Very WIP! 🚧 🚧 🚧

Language: Rust - Size: 5.56 MB - Last synced at: 14 days ago - Pushed at: almost 4 years ago - Stars: 617 - Forks: 26

mortberg/cubicaltt

Experimental implementation of Cubical Type Theory

Language: Haskell - Size: 2.43 MB - Last synced at: 7 months ago - Pushed at: over 1 year ago - Stars: 569 - Forks: 76

gruhn/typescript-sudoku

Playing Sudoku in TypeScript while the type checker highlights mistakes.

Language: TypeScript - Size: 818 KB - Last synced at: 4 days ago - Pushed at: 9 months ago - Stars: 494 - Forks: 2

eashanhatti/peridot 📦

A fast functional language based on two level type theory

Language: Haskell - Size: 1.14 MB - Last synced at: about 1 year ago - Pushed at: over 2 years ago - Stars: 389 - Forks: 4

rntz/datafun

Research on integrating datalog & lambda calculus via monotonicity types

Language: TeX - Size: 2.65 MB - Last synced at: 6 months ago - Pushed at: almost 3 years ago - Stars: 386 - Forks: 15

typedefs/typedefs

Programming language agnostic type construction language based on polynomials.

Language: Idris - Size: 718 KB - Last synced at: about 1 year ago - Pushed at: over 3 years ago - Stars: 364 - Forks: 18

stepchowfun/proofs

My personal repository of formally verified mathematics.

Language: Coq - Size: 1.28 MB - Last synced at: about 1 month ago - Pushed at: about 2 months ago - Stars: 297 - Forks: 13

martinescardo/TypeTopology

Logical manifestations of topological concepts, and other things, via the univalent point of view.

Language: Agda - Size: 17.6 MB - Last synced at: 11 days ago - Pushed at: 12 days ago - Stars: 254 - Forks: 45

martinescardo/HoTT-UF-Agda-Lecture-Notes

Lecture notes on univalent foundations of mathematics with Agda

Language: Agda - Size: 5.8 MB - Last synced at: 13 days ago - Pushed at: about 1 year ago - Stars: 227 - Forks: 20

RedPRL/sml-redprl 📦

The People's Refinement Logic

Language: Standard ML - Size: 11.3 MB - Last synced at: 5 months ago - Pushed at: over 2 years ago - Stars: 227 - Forks: 18

RedPRL/cooltt

😎TT

Language: OCaml - Size: 3.48 MB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 225 - Forks: 14

RedPRL/redtt

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

Language: OCaml - Size: 3.02 MB - Last synced at: 18 days ago - Pushed at: about 3 years ago - Stars: 208 - Forks: 12

lazear/types-and-programming-languages

Exercises from Benjamin Pierce's "Types and Programming Languages" textbook + extras!

Language: Rust - Size: 567 KB - Last synced at: 16 days ago - Pushed at: almost 5 years ago - Stars: 206 - Forks: 10

paarthenon/variant

Variant types in TypeScript

Language: TypeScript - Size: 6.76 MB - Last synced at: 5 days ago - Pushed at: about 1 year ago - Stars: 186 - Forks: 3

ditto/ditto

A Super Kawaii Dependently Typed Programming Language

Language: Haskell - Size: 323 KB - Last synced at: 10 months ago - Pushed at: almost 7 years ago - Stars: 171 - Forks: 5

advancedresearch/path_semantics

A research project in path semantics, a re-interpretation of functions for expressing mathematics

Language: Rust - Size: 90 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 170 - Forks: 11

veyselusta/programming-language-research

Research on theory of programming languages λ, compilers, interpreters, functional programming, formal methods, logic etc.

Size: 38.1 KB - Last synced at: 5 months ago - Pushed at: 9 months ago - Stars: 169 - Forks: 6

err0r500/foundational-knowledge-for-programmers

List of resources about foundational knowledge for programmers (supposed to last a few decades)

Size: 34.2 KB - Last synced at: about 1 year ago - Pushed at: over 4 years ago - Stars: 163 - Forks: 11

cicada-lang/cicada-solo

Cicada Language (solo version)

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

ilya-klyuchnikov/ttlite

A SuperCompiler for Martin-Löf's Type Theory

Language: Scala - Size: 1.5 MB - Last synced at: about 1 month ago - Pushed at: over 3 years ago - Stars: 120 - Forks: 9

owo-lang/minitt-rs

Dependently-typed lambda calculus, Mini-TT, extended and implemented in Rust

Language: Rust - Size: 336 KB - Last synced at: 22 days ago - Pushed at: over 4 years ago - Stars: 117 - Forks: 4

madnight/awesome-category-theory

A curated list of awesome Category Theory resources.

Size: 602 KB - Last synced at: 6 days ago - Pushed at: 18 days ago - Stars: 115 - Forks: 6

engboris/stellogen

An experimental unification-based programming language with logic-agnostic types, based on Girard's transcendental syntax

Language: OCaml - Size: 2.04 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 103 - Forks: 9

owo-lang/voile-rs

Dependently-typed row-polymorphic programming language, evolved from minitt-rs

Language: Rust - Size: 818 KB - Last synced at: 5 days ago - Pushed at: over 4 years ago - Stars: 97 - Forks: 5

TheoWinterhalter/formal-type-theory

Formalising Type Theory in a modular way for translations between type theories

Language: Coq - Size: 1.48 MB - Last synced at: 7 days ago - Pushed at: over 7 years ago - Stars: 94 - Forks: 4

cicada-lang/cicada-plct

Cicada Language (PLCT little team)

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

brendanzab/rust-nbe-for-mltt

Normalization by evaluation for Martin-Löf Type Theory with dependent records

Language: Rust - Size: 862 KB - Last synced at: 12 months ago - Pushed at: almost 3 years ago - Stars: 90 - Forks: 7

owo-lang/narc-rs

(WIP) Dependently-typed programming language with Agda style dependent pattern matching

Language: Rust - Size: 455 KB - Last synced at: 5 days ago - Pushed at: over 4 years ago - Stars: 80 - Forks: 4

bor0/gidti

Book: Introduction to Dependent Types with Idris

Size: 10.9 MB - Last synced at: about 13 hours ago - Pushed at: about 2 years ago - Stars: 78 - Forks: 4

molikto/mlang 📦

Towards changing things and see if it proofs

Language: Scala - Size: 1.31 MB - Last synced at: about 1 year ago - Pushed at: almost 4 years ago - Stars: 60 - Forks: 3

ice1000/guest0x0

Neon lights in the night tonight and stars that shine in the open sky

Language: Java - Size: 1.11 MB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 43 - Forks: 4

mr-ohman/logrel-mltt

A Logical Relation for Martin-Löf Type Theory in Agda

Language: Agda - Size: 4.2 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 40 - Forks: 10

lukeg101/lplzoo

Fine-grain implementations of common lambda calculi in Haskell, tested with QuickCheck

Language: Haskell - Size: 1.96 MB - Last synced at: 5 days ago - Pushed at: almost 4 years ago - Stars: 36 - Forks: 2

RedPRL/algaett

🦠 An experimental elaborator for dependent type theory using effects and handlers

Language: OCaml - Size: 620 KB - Last synced at: 18 days ago - Pushed at: over 1 year ago - Stars: 35 - Forks: 0

RedPRL/mugen

♾️ A library for universe levels and universe polymorphism

Language: OCaml - Size: 727 KB - Last synced at: 18 days ago - Pushed at: 5 months ago - Stars: 34 - Forks: 1

aripiprazole/lura

🍞 | IDE focused programming language study

Language: C - Size: 1.27 MB - Last synced at: 7 days ago - Pushed at: about 1 year ago - Stars: 34 - Forks: 1

jaycech3n/Isabelle-HoTT

An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle

Language: Standard ML - Size: 405 KB - Last synced at: about 2 months ago - Pushed at: over 2 years ago - Stars: 34 - Forks: 3

ualib/agda-algebras

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

Language: Agda - Size: 65 MB - Last synced at: about 1 month ago - Pushed at: 5 months ago - Stars: 33 - Forks: 7

tribbloid/shapesafe

SHAPE/S∀F∃: static prover/type-checker for N-D array programming in Scala, a use case of intuitionistic type theory

Language: Scala - Size: 7.81 MB - Last synced at: about 1 month ago - Pushed at: about 1 year ago - Stars: 32 - Forks: 4

Blaisorblade/dot-iris

Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization

Language: HTML - Size: 9.98 MB - Last synced at: about 1 month ago - Pushed at: about 2 months ago - Stars: 31 - Forks: 1

annenkov/two-level

Two-Level Type Theory

Language: Lean - Size: 151 KB - Last synced at: 22 days ago - Pushed at: over 5 years ago - Stars: 28 - Forks: 1

hash-org/hashc

The Hash programming language compiler :zap:

Language: Rust - Size: 11.1 MB - Last synced at: 27 days ago - Pushed at: 27 days ago - Stars: 27 - Forks: 2

KonjacSource/ShiTT

ShiTT is a toy proof assistant (almost).

Language: Haskell - Size: 354 KB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 27 - Forks: 1

L-TChen/Type-Theory

Lecture note on Lambda Calculus and Types for FLOLAC

Language: TeX - Size: 1.71 MB - Last synced at: about 1 month ago - Pushed at: 11 months ago - Stars: 27 - Forks: 4

chameco/bramble

dependently-typed lisp with flexible compiler backends

Language: Haskell - Size: 73.2 KB - Last synced at: 3 days ago - Pushed at: almost 6 years ago - Stars: 27 - Forks: 1

HarrisonGrodin/radical-julia

Radical ideas for the Julia language.

Language: Standard ML - Size: 5.86 KB - Last synced at: about 1 month ago - Pushed at: almost 5 years ago - Stars: 26 - Forks: 1

owo-lang/MLPolyR

The MLPolyR programming language, revived

Language: Standard ML - Size: 437 KB - Last synced at: about 2 years ago - Pushed at: over 4 years ago - Stars: 23 - Forks: 1

jaredloomis/Idris-HoTT

Homotopy Type Theory proofs in Idris

Language: Idris - Size: 3.91 KB - Last synced at: 2 months ago - Pushed at: almost 6 years ago - Stars: 22 - Forks: 1

CompSciCabal/reading-material

Reading schedule and our library of pdfs

Size: 23.6 MB - Last synced at: about 1 year ago - Pushed at: about 6 years ago - Stars: 22 - Forks: 1

artemohanjanyan/tt-conspect

Notes for type theory course

Language: TeX - Size: 384 KB - Last synced at: about 2 years ago - Pushed at: over 6 years ago - Stars: 22 - Forks: 6

wdamron/poly

Hindley-Milner type system with extensible records and variants, implemented in Go

Language: Go - Size: 185 KB - Last synced at: 14 days ago - Pushed at: over 4 years ago - Stars: 21 - Forks: 2

ionathanch/TTBFL

A logical relations model of a minimal type theory with bounded first-class universe levels mechanized in Lean.

Language: TeX - Size: 1.3 MB - Last synced at: about 4 hours ago - Pushed at: 16 days ago - Stars: 19 - Forks: 1

RedPRL/kado

🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory

Language: OCaml - Size: 648 KB - Last synced at: 18 days ago - Pushed at: 8 months ago - Stars: 19 - Forks: 1

ixaxaar/monoid.space

Learn pure math with agda :rocket:

Language: HTML - Size: 11.3 MB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 17 - Forks: 0

jbrkr/Category_Theory_Natural_Language_Processing_NLP

List of papers and other resources at the intersection of Category Theory and NLP.

Size: 25.4 KB - Last synced at: about 2 years ago - Pushed at: about 2 years ago - Stars: 17 - Forks: 2

xieyuheng/cat

A categorical semantics library in Agda.

Language: Agda - Size: 114 KB - Last synced at: about 1 month ago - Pushed at: over 5 years ago - Stars: 17 - Forks: 2

langston-barrett/reed-thesis

My undergradate thesis on coinductive types in univalent type theory

Language: TeX - Size: 1.27 MB - Last synced at: 20 days ago - Pushed at: about 7 years ago - Stars: 17 - Forks: 0

smimram/catt

An infinity-categorical coherence typechecker

Language: OCaml - Size: 251 KB - Last synced at: about 1 month ago - Pushed at: 6 months ago - Stars: 16 - Forks: 0

ice1000/anqur

Elaboration with inductive types

Language: Java - Size: 238 KB - Last synced at: about 1 month ago - Pushed at: almost 2 years ago - Stars: 16 - Forks: 2

lebrancconvas/Pure-Mathematics-EBooks

E-Books Library for someone who interested in Pure Mathematics.

Size: 16.6 MB - Last synced at: 3 months ago - Pushed at: over 3 years ago - Stars: 15 - Forks: 3

joom/direct-reflection-for-free

using Data and Typeable to get a direct reflection system for free, when we're implementing a toy language in Haskell

Language: TeX - Size: 810 KB - Last synced at: 2 months ago - Pushed at: about 5 years ago - Stars: 15 - Forks: 1

wkolowski/Typonomikon

Źródła mojej książki o Coqu, programowaniu funkcyjnym, teorii typów, logice konstruktywnej i innych takich.

Language: Coq - Size: 215 MB - Last synced at: 21 days ago - Pushed at: 21 days ago - Stars: 12 - Forks: 0

suhr/tmath

Language: Lean - Size: 276 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 12 - Forks: 3

proost-assistant/ProostLean

An reimplementation of the Proost proof-assistant written in Lean 4

Language: Lean - Size: 173 KB - Last synced at: 6 months ago - Pushed at: about 1 year ago - Stars: 12 - Forks: 0

jonsterling/agda-effectful-forcing

Agda formalization of the paper, "Higher-Order Functions and Brouwer's Thesis". Deduces a Brouwer ordinal from a function ((nat -> nat) -> nat) in System T.

Language: Agda - Size: 1.24 MB - Last synced at: about 1 month ago - Pushed at: over 4 years ago - Stars: 12 - Forks: 0

lambda-11235/ttyped

A simple dependently typed language based on the Calculus of Constructions.

Language: Haskell - Size: 116 KB - Last synced at: about 2 years ago - Pushed at: almost 5 years ago - Stars: 12 - Forks: 1

fsestini/tt-in-cubical

Type Theory in Type Theory using Cubical Agda

Language: Agda - Size: 70.3 KB - Last synced at: 5 months ago - Pushed at: about 6 years ago - Stars: 12 - Forks: 0

plt-amy/dep

A very small implementation of the Calculus of Constructions for experimentation purposes

Language: Haskell - Size: 8.79 KB - Last synced at: about 1 year ago - Pushed at: almost 7 years ago - Stars: 12 - Forks: 0

sumeetdas/fuml

Functional Minimal Language

Size: 33.2 KB - Last synced at: 10 months ago - Pushed at: over 3 years ago - Stars: 11 - Forks: 0

strict-types/strict-encoding

Protobufs for functional programming

Language: Rust - Size: 576 KB - Last synced at: 21 days ago - Pushed at: 21 days ago - Stars: 10 - Forks: 8

andreaslyn/mini-yu

A dependently typed programming language prototype

Language: Haskell - Size: 937 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 9 - Forks: 0

felipeperet/logic Fork of rodrigogribeiro/logic

An adventure on formalizing logics using the Agda programming language

Language: Agda - Size: 57.6 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 9 - Forks: 2

aripiprazole/bidir

🍴 | Complete and Easy implementation in Rust

Language: Rust - Size: 387 KB - Last synced at: 7 days ago - Pushed at: over 1 year ago - Stars: 9 - Forks: 0

AHartNtkn/IotaTT

A PTS Supporting Induction

Language: Haskell - Size: 84 KB - Last synced at: almost 2 years ago - Pushed at: over 7 years ago - Stars: 9 - Forks: 1

CAIMEOX/caimeox.github.io

My Zettelkasten - The Rabbit Hole

Language: XSLT - Size: 13.2 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 8 - Forks: 1

smimram/Mini-TT

A simple type-theoretic language in OCaml: Mini-TT

Language: OCaml - Size: 20.5 KB - Last synced at: about 1 month ago - Pushed at: about 3 years ago - Stars: 8 - Forks: 1

conilas/grammar-experimentation

An experimental programming language containing a higher-order type system

Language: Raku - Size: 654 KB - Last synced at: about 2 years ago - Pushed at: almost 5 years ago - Stars: 8 - Forks: 0

graded-type-theory/graded-type-theory

A Logical Relation for Martin-Löf Type Theory in Agda

Language: Agda - Size: 151 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 7 - Forks: 5

rhennigan/CodeEquivalenceUtilities

Utilities for testing code equivalence

Language: Mathematica - Size: 3.18 MB - Last synced at: about 2 months ago - Pushed at: 11 months ago - Stars: 7 - Forks: 1

Lolirofle/stuff-in-agda

Formal proofs in mathematics/computer science/logic formalized in the Agda language. A hobby project I am working on in my free time.

Language: Agda - Size: 4.67 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 7 - Forks: 1

aripiprazole/ekko

📘 | Writing Haskell in Kotlin article's project

Language: Kotlin - Size: 317 KB - Last synced at: 7 days ago - Pushed at: over 2 years ago - Stars: 7 - Forks: 0

markfarrell/3tier

[Archived] A prototype 3-tier web application written in PureScript.

Language: PureScript - Size: 4.33 MB - Last synced at: about 1 month ago - Pushed at: over 2 years ago - Stars: 7 - Forks: 0

petur-a/masters

Developing a type system for a minimal reversible functional language.

Language: TeX - Size: 1020 KB - Last synced at: about 1 year ago - Pushed at: over 6 years ago - Stars: 7 - Forks: 0

SydneyTypes/PLATYPUS Fork of type-theory/type-theory-study-group

Lunchtime type theory study group in Sydney

Language: TeX - Size: 3.4 MB - Last synced at: 5 months ago - Pushed at: over 7 years ago - Stars: 7 - Forks: 3

moea/types

Type System Modeling in Clojure

Language: Clojure - Size: 50.8 KB - Last synced at: 7 days ago - Pushed at: 9 months ago - Stars: 6 - Forks: 0

TheoWinterhalter/ett-to-wtt

Coq formalisation of a translation from (an) extensional type theory to (a) weak type theory

Language: Coq - Size: 630 KB - Last synced at: 7 days ago - Pushed at: about 2 years ago - Stars: 6 - Forks: 0

fsestini/nbe-mltt-wes

Normalization by Evaluation for a version of Martin-Löf Type Theory with weak explicit substitutions.

Language: Agda - Size: 26.4 KB - Last synced at: 5 months ago - Pushed at: about 2 years ago - Stars: 6 - Forks: 0

joewatt95/lambdacplus

A proof assistant based on the Calculus of Constructions

Language: JavaScript - Size: 33.7 MB - Last synced at: 12 months ago - Pushed at: about 2 years ago - Stars: 6 - Forks: 1

eduhenke/tapl-impl

This repository is meant to be a personal collection of implementations of the concepts from the TaPL(Types and Programming Languages) book.

Language: Haskell - Size: 95.7 KB - Last synced at: 11 months ago - Pushed at: over 2 years ago - Stars: 6 - Forks: 0

TheoWinterhalter/ett-to-itt

Coq formalisation and plugin of a translation from ETT to ITT

Language: Coq - Size: 836 KB - Last synced at: about 1 month ago - Pushed at: about 4 years ago - Stars: 6 - Forks: 0

jaycech3n/Isabelle-Spartan 📦

A dependent type theory logic for Isabelle

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

jonaprieto/athena 📦

Translates Metis ATP proofs to the Agda code

Language: TeX - Size: 15.1 MB - Last synced at: about 1 year ago - Pushed at: about 5 years ago - Stars: 6 - Forks: 2

jonaprieto/hott-cheatsheets 📦

Homotopy type theory cheatsheets to read the HoTT Book

Language: TeX - Size: 17.9 MB - Last synced at: about 2 years ago - Pushed at: almost 6 years ago - Stars: 6 - Forks: 0

nyuichi/shari

A proof assistant based on the internal language of topos with NNO (intuitionistic higher-order arithmetic)

Language: Rust - Size: 5.12 MB - Last synced at: about 1 month ago - Pushed at: about 2 months ago - Stars: 5 - Forks: 0