Extraction and verification of programs by analysis of formal proofs
From MaRDI portal
Publication:1823656
DOI10.1016/0304-3975(88)90125-9zbMath0681.68019OpenAlexW2084093324MaRDI QIDQ1823656
Publication date: 1988
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(88)90125-9
Specification and verification (program logics, model checking, etc.) (68Q60) Structure of proofs (03F07) General topics in the theory of software (68N01)
Related Items
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A system which automatically improves programs
- Some applications of Henkin quantifiers
- The Skolem method in intuitionistic calculi
- Pascal. User manual and report
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- On the computational power of pushdown automata
- Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems
- Constructive mathematics and computer programming
- Some negative results concerning prime number generators
- A General Theorem on Existence Theorems
- A Transformation System for Developing Recursive Programs
- Assumption Classes in Natural Deduction
- An axiomatic basis for computer programming
- On the concepts of completeness and interpretation of formal systems