Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
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...
Những tác giả chính: | Robert Constable, Wojciech Moczydlowski |
---|---|
Định dạng: | Bài viết |
Ngôn ngữ: | English |
Được phát hành: |
Logical Methods in Computer Science e.V.
2008-09-01
|
Loạt: | Logical Methods in Computer Science |
Những chủ đề: | |
Truy cập trực tuyến: | https://lmcs.episciences.org/1140/pdf |
Những quyển sách tương tự
-
Normalization of IZF with Replacement
Bằng: Wojciech Moczydlowski
Được phát hành: (2008-04-01) -
A Normalizing Intuitionistic Set Theory with Inaccessible Sets
Bằng: Wojciech Moczydlowski
Được phát hành: (2007-08-01) -
Classical BI: Its Semantics and Proof Theory
Bằng: James Brotherston, et al.
Được phát hành: (2010-07-01) -
Intuitionistic Layered Graph Logic: Semantics and Proof Theory
Bằng: Simon Docherty, et al.
Được phát hành: (2018-10-01) -
A Finite-Model-Theoretic View on Propositional Proof Complexity
Bằng: Erich Grädel, et al.
Được phát hành: (2022-06-01)