Extraction and verification of programs by analysis of formal proofs

DOI10.1016/0304-3975(88)90125-9zbMath0681.68019OpenAlexW2084093324MaRDI QIDQ1823656

Werner Alexi

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

zbMATH Keywords

correctnessterminationprogramprogram verificationprogram synthesis algorithm

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Structure of proofs (03F07) General topics in the theory of software (68N01)

Related Items

A complexity analysis of functional interpretations

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