KnowledgeBase » SEMINAR » ID = 658

NuPRL Demo

by Mark Bickford
2011-2012

Mark Bickford will demonstrate the Nuprl system in action. He will start by showing how to state and prove simple theorems in logic and number theory and extract efficient programs from the proofs. He will also illustrate some elements of Event Logic in specifying a protocol. If there is time he will show some proofs he created this summer while tracking results of Dexter Kozen and Alexandra Silva as they were developing them. His investigations reveal a need to take a closer look at Brouwer's ideas about continuity as a general property of computable functions.