Abstract: I will provide a brief introduction to impartial game theory consisting of examples of games as well as elementary operations on them. This will be followed by a presentation of their syntactic counterparts in Coq, culminating in formal proofs of several basic theorems.

Abstract: Having studied the equivariant cohomology of smooth toric varieties, we will see to what extent it determines the non-equivariant cohomology. In the equivariantly formal case, one gets the Jurkiewicz-Danilov theorem (with integer coefficients). In general, a complete answer is only known for rational coefficients.