Author: Freek Wiedijk
Title: Mapping the Classical Type Theory of Farmer's STTWU into the Constructive Type Theory of COQ
Abstract: 
When one considers the foundations of a classical proof
assistant like HOL, it has various "features" that one
doesn't have in a constructive framework: (1) the law of
the excluded middle, (2) extensional equality, and (3) a
choice operator (which for any predicate returns an object
that satisfies the predicate, if there is one.)  To model
such a system in a constructive world it seems that one
cannot avoid having to add "axioms" to obtain these features.

However, for the theory - introduced by William Farmer -
called "STTwU" (simple type theory with undefinedness), this
turns out not to be the case.  This theory is classical,
extensional, and it has a choice operator, but it can be
mapped into a constructive world without having to add
any axioms.

In this talk we will both present a LF context corresponding
to STTwU, as well inhabit that context in Coq.  We use a
stack of tricks to do this: a double negation translation
for the classical logic, setoids for the extensionality,
_partial_ setoids to deal with undefinedness, and finally
dual setoids for the choice operator.

Our work shows that we can have the classical world of
STTwU and still consider our work meaningful to constructive
mathematicians.