#

martin-lof-type-theory

Here are 5 public repositories matching this topic...

martinescardo / HoTT-UF-Agda-Lecture-Notes

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 Apr 16, 2024
Agda

saki-lang / saki-dev

A simple scala-like dependent type programming language

programming-language dependent-types scala3 martin-lof-type-theory dependent-type-theory mygo saki-lang

Updated Nov 30, 2024
Scala

lane-core / kitcat

Kitcat is an experimental Univalent mathematics library for proof theory, category theory, and computer science formalization in Agda

type-theory category-theory agda uni hott univalence agda-library homotopy-type-theory univalent-foundations univalent-mathematics martin-lof-type-theory univalence-axiom

Updated Oct 25, 2024
Agda

saki-lang / mltt-type-checker

An MLTT type checker implemented using Saki-Lang

programming-language type-theory calculus-of-constructions plt mltt martin-lof-type-theory mygo saki-lang

Updated Oct 24, 2024

FilippoFantinato / type-theory

Type Theory course ; Master's Degree in Computer Science @ UniPD

theorem-proving agda unipd martin-lof-type-theory

Updated Dec 25, 2023
Agda

Improve this page

Add a description, image, and links to the martin-lof-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 martin-lof-type-theory topic, visit your repo's landing page and select "manage topics."