
On this and the following pages, you will be asked to answer some
questions and translate some Nuprl proofs into English. You are
encouraged to enter your answers into a text document, keeping track
of the question number and/or proof number that you are working on.
When you have finished, email this document to Amanda
(hollandm@cs.cornell.edu). If this is inconvenient for you, though,
you can also answer these questions on paper and deliver them to my
mailbox or my office.
To navigate this study, read each page in its entirety, answer all
questions to the best of your ability, and then proceed on to the next
page. Once you have answered the questions on a page, please do not
return to that page or change your answers or translated proof for that
page. As mentioned before, you do not need to complete this study all in
one sitting. You can send me your responses in batches or wait and send
them all at once, but please be sure that your name appears at the top of
any document you send me. You are not required to translate all the proofs
in order for your participation to be valuable. Please be sure, after you
have finished the last proof that you are going to translate, to go to the
"Exiting the Study" page (listed in the menu bar at the side and bottom
of each page) and answer the questions there.
Most of the theorems you will translate refer to externally defined
lemmas and functions. These will be defined for you on the page
introducing the proof. The various tactics used in the proof are defined
for you on then Tactic Definitions page.
If in the process of translating a proof you get stuck because you
cannot understand the Nuprl version, you can indicate this in your
translation and leave a hole in the proof. However, please explain
where it was that you got stuck and what it was that you could not
understand.
Please translate the proof as it appears; by this I mean take the proof
tree as it is and work from there. Do not change the way in which
the proof was carried out. However, you may traverse the given proof
tree in any order that you like and you can omit any information
included in the Nuprl proof that you do not think is necessary for the
English version. As a guideline, write the proof as you would want it
to appear if you were going to have to read it and understand it without
having access to the Nuprl proof at all (and, since these are very simple
theorems, as if you were just learning these facts about mathematics).
In addition, you do not need to translate basic formulas into English,
though you may if you think it makes the proof clearer. Something
of the form "a = 0" can be used in that way in the proof.
If you have a question about any part of this study, about any of
the questions, or about a proof in particular, do not hesitate to
contact me. I do ask that you not discuss anything appearing within
this study with other people who may be participating.
Questions:
 What is your name?
 What is your email address?
 Is English your first language?
 What experience do you have in writing math proofs in English?
(e.g., a few math classes, was a math minor as undergrad or grad student,
have a degree in math, etc.)
 Have you ever read a Nuprl proof before?
 How proficient would you say you are in reading Nuprl proofs?
 Have you ever used the Nuprl system before?
 How proficient would you say you are in using the Nuprl system?
Please proceed on to the next page now.

