Combinatorics for theorem proving
Georges Gonthier · 2009
Combinatorial data --- the concrete constructs used for collecting, enumerating, traversing, quoting and marshaling arbitrary objects --- are ubiquitous in both mathematics and software. In mathematics they are often left implicit or hidden in ellipses, as is the (large) set of their properties. In constrast, programmers choose them explicitly, carefully selecting a variant with the right complexity and interface. Theorem proving stands in the middle: as in software, the precise choice of representation for combinatorics greatly impacts how well theories and proofs can be formalized --- but it is more the mathematical properties of the constructs that matter than their operational behavior. This talk will explore some new combinatorics library designs that arise from this new combination of constraints.