Robert L. Constable
Abstract
We have begun a project to produce interactive formally-grounded courseware for teaching mathematics and computing.
The courseware is created by a modern proof development system, Nuprl, based on its growing em reference library of formal computational mathematics. The project is supported by NSF and some results of the past eighteen months of work are available on the World Wide Web. This proposal requests an increment of funding to supplement the continuing investment of Cornell resources.
We are asking for funds to improve the educational value of the resources we have created. First, we want to add more targeted lessons as entry points to the large corpus of formal material. Second, we want to gather feedback on the existing lessons from a wider range of students and instructors. Third, we want to prepare for using the full Nuprl interactive capability when it becomes available on the Web in 1998 and then deploy it in 1999.
This proposal reviews the technical and pedagogical case for the project, reports on current progress and future plans and explains our ideas for improving the educational value of the material already created.