Extraction and verification of programs by analysis of formal proofs
From MaRDI portal
Publication:1823656
DOI10.1016/0304-3975(88)90125-9zbMATH Open0681.68019OpenAlexW2084093324MaRDI QIDQ1823656FDOQ1823656
Authors: 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
Recommendations
- Program extraction from classical proofs
- The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction
- scientific article; zbMATH DE number 749923
- scientific article; zbMATH DE number 2063221
- Getting results from programs extracted from classical proofs
- An arithmetic for polynomial-time computation
- scientific article; zbMATH DE number 177798
- Extraction of redundancy-free programs from constructive natural deduction proofs
- Refined program extraction from classical proofs
- Publication:5751976
General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60) Structure of proofs (03F07)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- On the computational power of pushdown automata
- An axiomatic basis for computer programming
- Title not available (Why is that?)
- Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Some applications of Henkin quantifiers
- Title not available (Why is that?)
- A Transformation System for Developing Recursive Programs
- On the concepts of completeness and interpretation of formal systems
- A system which automatically improves programs
- Pascal. User manual and report
- The Skolem method in intuitionistic calculi
- Assumption Classes in Natural Deduction
- Constructive mathematics and computer programming
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Some negative results concerning prime number generators
- A General Theorem on Existence Theorems
- Title not available (Why is that?)
Cited In (45)
- Program extraction from proofs: the fan theorem for uniformly coconvex bars
- Title not available (Why is that?)
- Title not available (Why is that?)
- A large-scale experiment in executing extracted programs
- Minlog -- a tool for program extraction supporting algebras and coalgebras
- Extracting imperative programs from proofs: In-place Quicksort
- Title not available (Why is that?)
- An arithmetic for polynomial-time computation
- A complexity analysis of functional interpretations
- Extracting total Amb programs from proofs
- Completeness, minimal logic and programs extraction
- Title not available (Why is that?)
- Title not available (Why is that?)
- First order marked types
- Analysis of methods for extraction of programs from non-constructive proofs.
- Program extraction from large proof developments
- The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction
- Title not available (Why is that?)
- Decorating proofs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Program extraction from nested definitions
- Extracting non-deterministic concurrent programs
- Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
- Program verification through characteristic formulae
- Proof pearl: constructive extraction of cycle finding algorithms
- Representing proof transformations for program optimization
- Program extraction from proofs of weak head normalization
- Title not available (Why is that?)
- Title not available (Why is that?)
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
- Title not available (Why is that?)
- Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics
- Proofs and programs: A naïve approach to program extraction
- Title not available (Why is that?)
- Getting results from programs extracted from classical proofs
- Program Extraction in Constructive Analysis
- Semantics-preserving procedure extraction
- Title not available (Why is that?)
- Program development by proof transformation.
- Title not available (Why is that?)
- Title not available (Why is that?)
- Writing constructive proofs yielding efficient extracted programs
- Program extraction from normalization proofs
- Studies of a theory of specifications with built-in program extraction
This page was built for publication: Extraction and verification of programs by analysis of formal proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1823656)
