In general, "formalising mathematical vernacular" is a good source for work relevant to your question. The field generally started in earnest with de Bruijn's Automath project.
Harvey Friedman has done some nice work on leveraging his theory of explicit definitions for set theory (cf. The Logical Strength of Mathematical Statements I, 1976) to give a language for doing mathematics in a way that is fairly natural and that can be easily translated into proofs over ZFC.
I'm afraid I don't have a good reference for this: he gave an invited talk to the ASL 2006 conference in Nijmegen.
Postscript
I remembered there were coauthors: the system was written up in a series of papers for a system called A language for knowledge management, due to Steve Kieffer (for a Master's project), Jeremy Avigad, and Harvey Friedman.
