Repository for documents and experiments to do with algebraically-indexed types
TeX Coq
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.
20121016-dream-talk
20131030-spls-talk
coq
fibrational
geometry-notes
mechanics
paper
quantlinear
.gitignore
README.md

README.md

Algebraically Indexed Types

Repository for documents and experiments to do with algebraically-indexed types

Directory Structure

  • paper/ contains a draft paper about algebraically-indexed types.
  • coq/ contains a Coq formalization of the framework from the paper, including the Abstraction Theorem
  • geometry-notes/ contains some notes on using algebraically-indexed types to enforce some geometric invariants.
  • fibrational/ contains some preliminary notes on a fibrational category-theoretic model of algebraically-indexed types.