Computer Science – Logic in Computer Science
Scientific paper
2008-06-07
LMCS 4 (3:5) 2008
Computer Science
Logic in Computer Science
17 pages
Scientific paper
10.2168/LMCS-4(3:5)2008
Church's Higher Order Logic is a basis for influential proof assistants -- HOL and PVS. Church's logic has a simple set-theoretic semantics, making it trustworthy and extensible. We factor HOL into a constructive core plus axioms of excluded middle and choice. We similarly factor standard set theory, ZFC, into a constructive core, IZF, and axioms of excluded middle and choice. Then we provide the standard set-theoretic semantics in such a way that the constructive core of HOL is mapped into IZF. We use the disjunction, numerical existence and term existence properties of IZF to provide a program extraction capability from proofs in the constructive core. We can implement the disjunction and numerical existence properties in two different ways: one using Rathjen's realizability for IZF and the other using a new direct weak normalization result for IZF by Moczydlowski. The latter can also be used for the term existence property.
Constable Robert
Moczydlowski Wojciech
No associations
LandOfFree
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic<br> Semantics does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic<br> Semantics, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic<br> Semantics will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-11739