65 Open source projects that are alternatives of or similar to tt-in-cubical

Univalent mathematics in Agda

Category theory formalized in cubical agda

Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.

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

My undergradate thesis on coinductive types in univalent type theory

Towards changing things and see if it proofs

Experimental implementation of Cubical Type Theory

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

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

Lecture notes on univalent foundations of mathematics with Agda

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

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

Reading schedule and our library of pdfs

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

λΠ Programming Language Theory

Research on integrating datalog & lambda calculus via monotonicity types

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

Lecture note on Lambda Calculus and Types for FLOLAC

The MLPolyR programming language, revived

A selection of formal proofs in Coq.

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

🧊 Модальний Гомотопічний Прувер

The theory of algebraic graphs formalised in Agda

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory

A modern proof language

A slow-paced introduction to reflection in Agda. ---Tactics!

A collection of papers on modules.

Language Server for Agda

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

A universe of scope- and type-safe syntaxes (syntices?). Includes generic implementation of type-preserving renaming/substitution with all the proofs you could possibly need.

Homotopy type theory

Agda language support for the Atom editor

A formalization of category theory in cubical Agda

Category theory applied to functional programming (undergraduate project)

Programming language agnostic type construction language based on polynomials.

The People's Refinement Logic

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

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

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

Homepage Theorem Proving in Lean FAQ

Homotopy Type Theory proofs in Idris

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

wherein I implement several substructural logics in Agda

Variant types in TypeScript

A Super Kawaii Dependently Typed Programming Language

Cicada Language

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

A workshop on learning Agda with minimal prerequisites.

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

A categorical semantics library in Agda.

Mtac in Agda

agda-mode on VS Code

A builder for LaTeX, knitr, literate Agda, literate Haskell and Pweave that automatically builds dependencies.

Algebraic proof discovery in Agda

😎TT

A TACtic library for Agda

Accessing Agda's interaction mode via command line & external tactic for Agda.

Functional Reactive Programming with Agda

Book: Gentle Introduction to Dependent Types with Idris

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