Journal article 567 views 112 downloads
Intuitionistic fixed point logic
,
Hideki Tsuiki
Annals of Pure and Applied Logic, Volume: 172, Issue: 3, Start page: 102903
Swansea University Author:
Ulrich Berger
-
PDF | Accepted Manuscript
Distributed under the terms of a Creative Commons Attribution, Non-Commercial, NoDerivatives (CC-BY-NC-ND) Licence.
Download (571.91KB)
DOI (Published version): 10.1016/j.apal.2020.102903
Abstract
The logical system IFP introduced in this paper supports program extraction from proofs, unifying theoretical and practical advantages: Based on first-order logic and powerful strictly positive inductive and coinductive definitions, IFP support abstract axiomatic mathematics with a large amount of c...
| Published in: | Annals of Pure and Applied Logic |
|---|---|
| ISSN: | 0168-0072 |
| Published: |
Elsevier BV
2021
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa55847 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
The logical system IFP introduced in this paper supports program extraction from proofs, unifying theoretical and practical advantages: Based on first-order logic and powerful strictly positive inductive and coinductive definitions, IFP support abstract axiomatic mathematics with a large amount of classical logic. The Haskell-like target programming language has a denotational and an operational semantics which are linked through a computational adequacy theorem that extends to infinite data. Program extraction is fully verified and highly optimised, thus extracted programs are guaranteed to be correct and free of junk. A case study in exact real number computation underpins IFP's effectiveness. |
|---|---|
| Keywords: |
Proof theory, realizability, program extraction , induction , coinduction , exact real number computation |
| College: |
Faculty of Science and Engineering |
| Issue: |
3 |
| Start Page: |
102903 |