68 Open source projects that are alternatives of or similar to TypeTopology

Univalent mathematics in Agda

Formal Topology in Univalent Foundations (WIP).

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

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

My undergradate thesis on coinductive types in univalent type theory

Homotopy Type Theory proofs in Idris

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

Type Theory in Type Theory using Cubical Agda

A formalization of category theory in cubical Agda

λΠ Programming Language Theory

Homepage Theorem Proving in Lean FAQ

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

Homotopy type theory

The People's Refinement Logic

Programming language agnostic type construction language based on polynomials.

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

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

A Super Kawaii Dependently Typed Programming Language

The MLPolyR programming language, revived

Variant types in TypeScript

An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.

Algebraic proof discovery in Agda

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

Cicada Language

A modern proof language

A workshop on learning Agda with minimal prerequisites.

The theory of algebraic graphs formalised in Agda

Towards changing things and see if it proofs

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

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

Experimental implementation of Cubical Type Theory

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

Research on integrating datalog & lambda calculus via monotonicity types

Implementation of Conway's Surreal Numbers

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

Lecture notes on univalent foundations of mathematics with Agda

Lecture note on Lambda Calculus and Types for FLOLAC

Category theory formalized in cubical agda

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

A selection of formal proofs in Coq.

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

Functional Reactive Programming with Agda

Language Server for Agda

😎TT

Category theory applied to functional programming (undergraduate project)

Book: Gentle Introduction to Dependent Types with Idris

wherein I implement several substructural logics in Agda

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

Mtac in Agda

A collection of papers on modules.

An Emacs mode for working with Agda code in an Org-mode like fashion, more or less.

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

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

agda-mode on VS Code

Reading schedule and our library of pdfs

Constructive Interpretations of HoTT

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

A categorical semantics library in Agda.

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.

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