Design of Proving, Verifying, and Synthesizing System based on Constructive

点击翻译按钮获取中文摘要

This project has investigated the key-idea constructive programming very thoroughly. Constructive programming is a new paradigm in programming methodology, which takes constructive logical system as an underlying theory and provides a rigid and uniform basis for verifying programs, proving mathematical theorems, and synthesizing programs from its logical specifications.Our main results are summarized as follows:1. We designed a well-organized constructive logical system SST. SST is symbolic in the sense that all terms and formulas can be treated mechanically, and therefore, by computers.SST is a suitable logic for writing specifications (datatypes as sets), and for reasoning about properties of programs, since SST is a first order predicate logic for partial terms.2. We established the theoretical results. We first made a model of SST to show SST is consistent. This model reflects our intended domain of S-expressions. We proved the representation theorem for general recursive functions … More in SST. We then defined the formalized realizability interpretation of SST. This interpretation resembles so called q-realizabilty, but we refined it to allow arbitrary inductive definition. We proved the soundness of our realizability interpretation.3. SST contains a pure functional programming language LAMBDA. LAMBDA is formed by taking closed terms in SST. It is purely functional, but for practical conveniences, we extended it to LAMBDA+. We implemented the interpreter of LAMBDA on a workstation.4. We programmed several systems on top of LAMBDA. We made a metaeircular interpreter of LAMBDA itself, a proof-checking system of SST, and a program-extractor LAMBDA. We can reason about the properties of these programs by the proof-checking system itself. The program-extractor extracts a LAMBDA-program from a proof in SST.5. Using the above systems, we examined by examples the idea of constructive programming. We made sample proofs, and checked its validity by the proof-checking system, and extracted computational parts by the program-extractor.As a feed-back of this process, we refined SST and LAMBDA so that these systems become more simple and easy to treat. Less