Programming Language Theory λΠ
-
Updated
Jun 27, 2022 - CSS
Programming Language Theory λΠ
Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
A next-gen functional language
Lean Theorem Prover
Agda is a dependently typed programming language / interactive theorem prover.
A Coq library for Homotopy Type Theory
A friendly little systems language with first-class types. Very WIP!
Experimental implementation of Cubical Type Theory
A fast functional language based on two level type theory
Programming language agnostic type construction language based on polynomials.
Research on integrating datalog & lambda calculus via monotonicity types
My personal repository of formally verified mathematics.
The People's Refinement Logic
Lecture notes on univalent foundations of mathematics with Agda
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Variant types in TypeScript
A Super Kawaii Dependently Typed Programming Language
Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.
List of resources about foundational knowledge for programmers (supposed to last a few decades)
Add a description, image, and links to the type-theory topic page so that developers can more easily learn about it.
To associate your repository with the type-theory topic, visit your repo's landing page and select "manage topics."