Stars
Display plugin of Jianpu notation for Lilypond
print Jianpu notation in the Lilypond music typesetter
MPRI-2.4 Dependently-typed Functional Programming
An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
Univalent Parametricity for Effective Transport
Repository for my experimentation project with AutoInAgda
A Coq development of the theory of Indexed W types with function extensionality.
BibTeX bibliographies for proof engineering-related papers
Experimental implementation of Cubical Type Theory