Sciweavers

74
Voted
TPHOL
1999
IEEE
15 years 1 months ago
Universal Algebra in Type Theory
We present a development of Universal Algebra inside Type Theory, formalized using the proof assistant Coq. We define the notion of a signature and of an algebra over a signature. ...
Venanzio Capretta