overview We propose to improve the educational value of the resources we have created in three ways: implement more formally-grounded lessons and improve the existing ones in response to feedback, link Nuprl Web material to the Cornell/Xerox CoNote system to enable students to comment directly on the lessons, and build interactive lessons in Nuprl that can be released on the Web as the Nuprl research group moves more functionality onto the Web. We elaborate these points.
lessons In section 2 we present part of a lesson built on top of a library called functions_1. The appendix shows a lesson on induction grounded in the library number_theory_1. There are other lessons at the Web site, but we need to create several more to take advantage of the existing libraries of discrete mathematics and to provide instructors of various kinds of courses with material. In particular, we intend to produce lessons for discrete mathematics (CS, Math, EE), for logic (CS, Math, Philosophy), automata and formal languages (CS, Linguistics). We aim to create two special lessons, one on Gödel's theorem which can be so nicely presented in the Nuprl logic, and one on Automata theory, specifically state minimization.
student feedback The CoNote system is software developed by Cornell and the Xerox Design Research Institute at Cornell to enable a group of users of html documents to share annotations of the document. By adding CoNote anchor points to our lessons and providing a CoNote server with the Web material, readers of the courseware will be able to add comments and questions directly to the lessons. We can use this capability to enhance the value of the lessons by leaving the good annotations in place (like a frequently asked questions, FAQ, capability), and we can use it to collect feedback for improving the lessons themselves. We could even assign students and staff to monitor lessons on a weekly basis and answer the frequently asked questions. A small amount of funding would enable this (one hour a week for five students for an academic year-see FAQ response in the budget).
interactivity Students using the Nuprl system itself would have access to a wide range of interactive capabilities. They can create proofs or modify existing ones. They can be led through new proofs. They can solve exercises. They can step through rewrites and other symbolic computations step by step as well as stepping through ordinary compuations.
Throughout 1998 the Nuprl research group will provide more of the full interactive capability directly on the Web. This will allow us to put the highly interactive lessons in the Courseware Library. (For the sake of this proposal we could call this NuprlW.)