λΠ Programming Language Theory
-
Updated
Sep 26, 2020 - CSS
#
type-theory
Here are 138 public repositories matching this topic...
Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
compiler
functional-programming
book
lambda-calculus
evaluation
type-theory
type
pdf-book
type-checking
haskel
type-system
functional-language
hindley-milner
type-inference
intermediate-representation
-
Updated
Oct 1, 2020 - Haskell
Lean Theorem Prover
-
Updated
Aug 6, 2020 - C++
Agda is a dependently typed programming language / interactive theorem prover.
-
Updated
Oct 21, 2020 - Haskell
An efficient proof language
dependent-types
functional-programming
lambda-calculus
theorem-proving
type-theory
interaction-nets
inets
formality
affine-lambdas
proof-language
-
Updated
Oct 20, 2020 - JavaScript
Homotopy type theory
-
Updated
Oct 21, 2020 - Coq
Experimental implementation of Cubical Type Theory
-
Updated
Mar 24, 2019 - Haskell
(Please don’t repost, this is still a WIP) A friendly little systems language with first-class types and unboxed data.
programming-language
rust
typechecker
dependent-types
compiler
type-theory
systems-language
type-system
systems-programming
bidirectional-typechecking
dependent-record-types
dependent-records
-
Updated
Oct 20, 2020 - Rust
Programming language agnostic type construction language based on polynomials.
serialization
types
marshalling
type-theory
category-theory
serialization-library
f-algebras
type-definitions
-
Updated
Aug 22, 2020 - Idris
Research on integrating datalog & lambda calculus via monotonicity types
-
Updated
Mar 15, 2020 - TeX
The People's Refinement Logic
-
Updated
Nov 4, 2019 - Standard ML
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
-
Updated
Jan 10, 2020 - OCaml
Lecture notes on univalent foundations of mathematics with Agda
dependent-types
type-theory
agda
lecture-notes
mltt
homotopy-type-theory
univalent-foundations
univalent-mathematics
hott-uf
martin-lof-type-theory
univalence-axiom
function-extensionality
propositional-truncation
univalent-type-theory
-
Updated
Oct 11, 2020 - Agda
A Super Kawaii Dependently Typed Programming Language
-
Updated
Jul 12, 2018 - Haskell
A selection of formal proofs in Coq.
-
Updated
Aug 12, 2020 - Coq
List of resources about foundational knowledge for programmers (supposed to last a few decades)
computer-science
awesome
cryptography
networking
algorithms
linear-algebra
type-theory
category-theory
programming-languages
programming-paradigms
awesome-list
computer-architecture
software-architecture
algorithms-and-data-structures
proof-theory
-
Updated
Apr 7, 2020
A research project in path semantics, a re-interpretation of functions for expressing mathematics
-
Updated
Oct 16, 2020 - Rust
A SuperCompiler for Martin-Löf's Type Theory
-
Updated
Jun 8, 2020 - Scala
Dependently-typed row-polymorphic programming language, evolved from minitt-rs
-
Updated
Sep 21, 2020 - Rust
Formalising Type Theory in a modular way for translations between type theories
-
Updated
Jan 10, 2018 - Coq
Normalization by evaluation for Martin-Löf Type Theory with dependent records
rust
dependent-types
type-theory
type-system
type-inference
unification
type-checker
bidirectional-typechecking
debruijn-indices
dependent-record-types
dependent-records
normalization-by-evaluation
semantic-typechecking
-
Updated
Jun 22, 2019 - Rust
Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.
type-theory
agda
ordinal
homotopy-type-theory
univalent-foundations
constructive-mathematics
compact-type
totally-separated-type
injective-type
searchable-set
univalent-mathematics
-
Updated
Oct 5, 2020 - Agda
Dependently-typed lambda calculus, Mini-TT, extended and implemented in Rust
-
Updated
Sep 21, 2020 - Rust
A collection of papers on modules.
-
Updated
Aug 9, 2020
Book: Gentle Introduction to Dependent Types with Idris
-
Updated
Oct 16, 2020
Variant types in TypeScript
-
Updated
Oct 21, 2020 - TypeScript
(WIP) Dependently-typed programming language with Agda style dependent pattern matching
-
Updated
Oct 5, 2020 - Rust
Exercises from Benjamin Pierce's "Types and Programming Languages" textbook + extras!
-
Updated
Jul 26, 2020 - Rust
Improve this page
Add a description, image, and links to the type-theory topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the type-theory topic, visit your repo's landing page and select "manage topics."
search
[issue 7]in code for background, or see this commit 1855e9218c7388ce1b4bf1f19d6679fcaea2324cthis issue only touch the parser and elaborator, don't touch the core