Interactive Formal Courseware Project

• NSF Abstract: Using Web Access to Formal Mathematics to Support Instruction in Computational Discrete Mathematics
• NSF Full Report: Using Web Access to Formal Mathematics to Support Instruction in Computational Discrete Mathematics
• Caldwell Library: Propositional Logic by Caldwell Theories
• Extracting Propositional Decidability: A proof of propositional decidability in constructive type theory and its extracted program. James Caldwell
• Automata Libraries
• Lessons in Discrete Mathematics. Stuart Allen
  
  Return to Nuprl Page