Next: Proposed Work Up: Introduction Previous: Brief Overview

Previous Work

The initial proposal submitted in 1995 requested three years of funding to create a repository of material for mathematics and computer science education as well as funding to disseminate and evaluate the materials. We were funded for two years with the goal of creating course material. Now, eighteen months into the project, we have produced the first version of most of this body of material.

The courseware project began to unfold just as the World Wide Web exploded on the national scene. The emergence of the Web substantially altered our plans. We recognized the imperative that our material be made available on the Web. We designed and built software which produced html code for any Nuprl library and put these libraries on our Web site. We created an example of integrated formal and informal material by formalizing sections of automata theory from Hopcroft and Ullman's classic text book Formal Languages and Their Relation to Automata. We also made available material on logic based on Smullyan's approach in his superb text book First-Order Logic. The Web-based material includes these new documents and libraries

  1. Formalizing Automata Theory I: Finite Automata
  2. Extracting Propositional Decidability: A proof of propositional decidability in constructive type theory and its extracted program.
  3. Simple Imperative Programming Languages

The results from 1 are being published [24], and the overall project was the subject of the publication [21] from the NSF Showcase Project. The PI spoke on this subject at the 1996 Frontiers in Education conference as an NSF Showcase Project.


karla@cs.cornell.edu
Wed Jul 2 11:48:15 EDT 1997