[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi again, I have combined my original list with helpful responses from several people to write a blog post here: http://why-lambda.blogspot.co.uk/2015/04/mechanized-formalizations-of-pi.html Thanks to Robert Harper, Dale Miller, Dominic Orchard, Francois Pottier, Ivan Scagnetto, Gabriel Scherer, and Tjark Weber for their suggestions. I'm happy to update it (or add further pointers to a follow-up post) if there are any more responses. --James
