Repository | Book | Chapter
(1987) Mathematical logic and its applications, Dordrecht, Springer.
Not considering philosophical arguments, the main motive for using constructive reasoning when constructing programs is that constructive proofs have computational content. For instance, formulating a specification and proving it in Martin-Löf's type theory, gives a program satisfying the specification. On the other hand, extracting programs from classical proofs is in general not possible. However, the process of deriving a program may not only involve the actual construction of the program but also the verification that an already constructed part of the program satisfies some property and it is then quite possible to use classical logic. A system for program derivation where you may use classical logic is the one developed by Manna and Waldinger [5].
Publication details
DOI: 10.1007/978-1-4613-0897-3_25
Full citation:
Smith, J. M. (1987)., On a nonconstructive type theory and program derivation, in D. G. Skordev (ed.), Mathematical logic and its applications, Dordrecht, Springer, pp. 331-340.
This document is unfortunately not available for download at the moment.