A "proof assistant" is a software package comprising a validity
checker for proofs in a particular logic, accompanied by
semi-decision procedures called "tactics" that assist the
mathematician in filling in the easy parts of the proofs. I
will...
The correspondence between homotopy types and higher categorical
analogs of groupoids which was first conjectured by Alexander
Grothendieck naturally leads to a view of mathematics where sets
are used to parametrize collections of objects without...
In recent research it has become clear that there are
fascinating connections between constructive mathematics,
especially as formulated in the type theory of Martin-Löf, and
homotopy theory, especially in the modern treatment in terms of
Quillen...
