"Logics for termination and correctness of functional programs", in
_Logic from Computer Science_, MSRI Pubs.vol.21, Springer 1992, 95-127,
"Polymorphic typed lambda-calculi in a type-free axiomatic framework",
in _Logic and Computation_, Contemporary Mathematics series vol.106,
Amer. Math. Soc., 1990, 101-136.
There is no question in my mind that if the qed project is to be viable,
it has to concentrate on systems with these kinds of features. Relations
to type-checking for computer programs (which in any case are of limited
value), are a secondary matter. Moreover, it should be pretty open-ended
about what basic principles are admitted, as in de Bruin's restaurant.
What will be important is to have a rich formal language which reflects
the everyday world of mathematics, where there is no concern with the
"ultimate" building blocks of mathematical concepts (as many suppose
sets and membership to be). Then one has to inquire what principles
are commonly appealed to in a given body of mathematics when it comes
to representing and checking proofs. The first part would be akin to
what some people have tried to do in AI with the representation of
common-sense knowledge.