type-theory

Star

Here are 133 public repositories matching this topic...

steshaw / plt

Star

λΠ Programming Language Theory

functional-programming logic type-theory category-theory programming-languages proof-theory

Updated Jul 9, 2020
CSS

sdiehl / write-you-a-haskell

Star

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 20, 2019
Haskell

leanprover / lean

Star

Lean Theorem Prover

programming-language dependent-types theorem-proving verification type-theory lean

Updated Aug 6, 2020
C++

agda / agda

Star

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

programming-language dependent-types proof-assistant type-theory agda

Updated Aug 10, 2020
Haskell

moonad / Formality

Star

An efficient proof language

dependent-types functional-programming lambda-calculus theorem-proving type-theory interaction-nets inets formality affine-lambdas proof-language

Updated Aug 9, 2020
JavaScript

HoTT / HoTT

Star

Homotopy type theory

type-theory homotopy-type-theory univalent-foundations

Updated Aug 10, 2020
Coq

mortberg / cubicaltt

Star

Experimental implementation of Cubical Type Theory

type-theory cubical-type-theory homotopy-type-theory univalent-foundations

Updated Mar 24, 2019
Haskell

pikelet-lang / pikelet

Star

(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 Aug 9, 2020
Rust

typedefs / typedefs

Star

Programming language agnostic type construction language based on polynomials.

serialization types marshalling type-theory category-theory serialization-library f-algebras type-definitions

Updated Jul 11, 2020
Idris

rntz / datafun

Star

Research on integrating datalog & lambda calculus via monotonicity types

programming-language query compiler type-theory datalog monotonicity semilattices

Updated Mar 15, 2020
TeX

RedPRL / sml-redprl

Star

The People's Refinement Logic

nuprl proof-assistant type-theory cubical-type-theory

Updated Nov 4, 2019
Standard ML

RedPRL / redtt

Star

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

proof-assistant type-theory cubical-type-theory

Updated Jan 10, 2020
OCaml

martinescardo / HoTT-UF-Agda-Lecture-Notes

Star

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 Jun 29, 2020
Agda

ditto / ditto

Star

A Super Kawaii Dependently Typed Programming Language

programming-language dependent-types proof-assistant type-theory

Updated Jul 12, 2018
Haskell

stepchowfun / proofs

Star

A selection of formal proofs in Coq.

coq proof-assistant type-theory formal-verification

Updated Mar 8, 2020
Coq

err0r500 / foundational-knowledge-for-programmers

Star

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

ilya-klyuchnikov / ttlite

Star

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

programming-language dependent-types coq type-theory idris agda supercompilation

Updated Jun 8, 2020
Scala

advancedresearch / path_semantics

Star

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

research type-theory mathematical-logic

Updated Aug 10, 2020
Rust

TheoWinterhalter / formal-type-theory

Star

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

reflection type-theory formalization

Updated Jan 10, 2018
Coq

owo-lang / voile-rs

Star

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

programming-language dependent-types type-theory extensible

Updated Dec 2, 2019
Rust

brendanzab / rust-nbe-for-mltt

Star

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

martinescardo / TypeTopology

Star

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 Aug 7, 2020
Agda

owo-lang / minitt-rs

Star

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

programming-language dependent-types type-theory

Updated Jan 18, 2020
Rust

bor0 / gidti

Star

Book: Gentle Introduction to Dependent Types with Idris

dependent-types books types lambda-calculus theorem-proving type-theory idris

Updated Feb 23, 2020

RedPRL / cooltt

Star

😎TT

proof-assistant type-theory cubical-type-theory homotopy-type-theory

Updated Aug 3, 2020
OCaml

ak3n / modules-papers

Star

A collection of papers on modules.

modules type-theory papers programming-language-theory

Updated Aug 9, 2020

paarthenon / variant

Star

Variant types in TypeScript

redux flux typescript type-theory variants union discriminated-unions variant dispatching

Updated Jul 19, 2020
TypeScript

molikto / mlang

Star

Towards changing things and see if it proofs

dependent-types proof-assistant type-theory cubical-type-theory

Updated Jun 28, 2020
Scala

owo-lang / narc-rs

Star

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

programming-language dependent-types pattern-matching type-theory

Updated Jan 18, 2020
Rust

lazear / types-and-programming-languages

Star

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

types lambda-calculus type-theory programming-languages tapl types-and-programming-languages

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.

Curate this topic

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."

Learn more