Extraction of redundancy-free programs from constructive natural deduction proofs
- 1 July 1991
- journal article
- Published by Elsevier in Journal of Symbolic Computation
- Vol. 12 (1) , 29-69
- https://doi.org/10.1016/s0747-7171(08)80139-3
Abstract
No abstract availableKeywords
This publication has 3 references indexed in Scilit:
- The calculus of constructionsInformation and Computation, 1988
- QPC: QJ-based proof compiler -simple examples and analysis-Published by Springer Nature ,1988
- Metamathematical Investigation of Intuitionistic Arithmetic and AnalysisPublished by Springer Nature ,1973