A Coq library for Homotopy Type Theory
-
Updated
Nov 22, 2024 - Coq
#
type-theory
Here are 15 public repositories matching this topic...
My personal repository of formally verified mathematics.
-
Updated
Oct 29, 2024 - Coq
Formalising Type Theory in a modular way for translations between type theories
-
Updated
Jan 10, 2018 - Coq
Źródła mojej książki o Coqu, programowaniu funkcyjnym, teorii typów, logice konstruktywnej i innych takich.
-
Updated
Oct 18, 2024 - Coq
Coq formalisation of a translation from (an) extensional type theory to (a) weak type theory
-
Updated
Apr 28, 2023 - Coq
Coq formalisation and plugin of a translation from ETT to ITT
-
Updated
Apr 10, 2021 - Coq
Personal research notes
dependent-types
functional-programming
proof-assistant
type-theory
cubical-type-theory
programming-languages
term-rewriting
nominal-set
homotopy-type-theory
-
Updated
Oct 18, 2024 - Coq
"A Basis for Event-Driven Programming" based on Linear Temporal Type Theory
-
Updated
May 21, 2021 - Coq
Code and examples based on the tutorial 'A Tutorial on [Co-]Inductive Types in Coq' by Eduardo Giménez and Pierre Castéran
-
Updated
May 9, 2017 - Coq
Strong normalization and parametricity for System Fω in Coq
-
Updated
Sep 10, 2024 - Coq
Some Notes on Types and Categories.
-
Updated
Aug 23, 2024 - Coq
Collection of explainatory example proofs for popular proof assistants.
-
Updated
Aug 21, 2018 - Coq
Code and examples based on the book 'Certified Programming with Dependent Types' (version: June 30, 2016) by Adam Chlipala.
-
Updated
May 4, 2017 - Coq
All coq code and exercises from Software Fundations by Michael Clarkson.
-
Updated
Mar 8, 2023 - Coq
Improve this page
Add a description, image, and links to the type-theory topic page so that developers can more easily learn about it.
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."