KnowledgeBase » 
PUBLICATION
» ID = 747
Coq as a Metatheory for Nuprl with Bar Induction
by Vincent Rahli, Mark Bickford
2015
- Presented at Continuity, Computability, Constructivity – From Logic to Algorithms (CCC 2015), Kochel am See, Germany, September 14, 2015.
- Unofficial PDF
Abstract
These past few years, we have been experimenting in Nuprl with versions of Brouwer’s Bar Induction principle. Until recently we had no formal proof that these rules are valid Nuprl reasoning principles. Thanks to our formalization of Nuprl’s metatheory in Coq, we can now rigorously check whether these principles are consistent with Nuprl. In this paper we present a proof, using our Coq framework, of the validity of Brouwer’s Bar Induction principle on sequences of natural numbers. To prove this result we added all Coq functions from natural numbers to natural numbers to Nuprl’s computation system.