Extraction and verification of programs by analysis of formal proofs
From MaRDI portal
Publication:1823656
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
Cites work
- scientific article; zbMATH DE number 4014708 (Why is no real title available?)
- scientific article; zbMATH DE number 3817038 (Why is no real title available?)
- scientific article; zbMATH DE number 3911684 (Why is no real title available?)
- scientific article; zbMATH DE number 3660776 (Why is no real title available?)
- scientific article; zbMATH DE number 3684934 (Why is no real title available?)
- scientific article; zbMATH DE number 3685488 (Why is no real title available?)
- scientific article; zbMATH DE number 3735770 (Why is no real title available?)
- scientific article; zbMATH DE number 3748395 (Why is no real title available?)
- scientific article; zbMATH DE number 3750146 (Why is no real title available?)
- scientific article; zbMATH DE number 3503206 (Why is no real title available?)
- scientific article; zbMATH DE number 3216178 (Why is no real title available?)
- scientific article; zbMATH DE number 3275554 (Why is no real title available?)
- scientific article; zbMATH DE number 3358455 (Why is no real title available?)
- A General Theorem on Existence Theorems
- A Transformation System for Developing Recursive Programs
- A system which automatically improves programs
- An axiomatic basis for computer programming
- Assumption Classes in Natural Deduction
- Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems
- Constructive mathematics and computer programming
- 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
- On the concepts of completeness and interpretation of formal systems
- Pascal. User manual and report
- Some applications of Henkin quantifiers
- Some negative results concerning prime number generators
- The Skolem method in intuitionistic calculi
Cited in
(45)- A complexity analysis of functional interpretations
- Extracting total Amb programs from proofs
- Studies of a theory of specifications with built-in program extraction
- scientific article; zbMATH DE number 2003148 (Why is no real title available?)
- The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction
- Getting results from programs extracted from classical proofs
- Program extraction from large proof developments
- Extracting imperative programs from proofs: In-place Quicksort
- scientific article; zbMATH DE number 1617311 (Why is no real title available?)
- Analysis of methods for extraction of programs from non-constructive proofs.
- scientific article; zbMATH DE number 408816 (Why is no real title available?)
- Completeness, minimal logic and programs extraction
- Program development by proof transformation.
- Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
- Extracting non-deterministic concurrent programs
- scientific article; zbMATH DE number 2003158 (Why is no real title available?)
- scientific article; zbMATH DE number 1765700 (Why is no real title available?)
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
- Writing constructive proofs yielding efficient extracted programs
- An arithmetic for polynomial-time computation
- scientific article; zbMATH DE number 1973215 (Why is no real title available?)
- Program verification through characteristic formulae
- Minlog -- a tool for program extraction supporting algebras and coalgebras
- Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics
- Program extraction from normalization proofs
- Proofs and programs: A naïve approach to program extraction
- scientific article; zbMATH DE number 512774 (Why is no real title available?)
- Program extraction from proofs: the fan theorem for uniformly coconvex bars
- Representing proof transformations for program optimization
- scientific article; zbMATH DE number 785043 (Why is no real title available?)
- scientific article; zbMATH DE number 176743 (Why is no real title available?)
- Decorating proofs
- Semantics-preserving procedure extraction
- scientific article; zbMATH DE number 4014708 (Why is no real title available?)
- Program Extraction in Constructive Analysis
- scientific article; zbMATH DE number 4187141 (Why is no real title available?)
- Program extraction from proofs of weak head normalization
- Proof pearl: constructive extraction of cycle finding algorithms
- scientific article; zbMATH DE number 2063221 (Why is no real title available?)
- Program extraction from nested definitions
- scientific article; zbMATH DE number 2006631 (Why is no real title available?)
- A large-scale experiment in executing extracted programs
- First order marked types
- scientific article; zbMATH DE number 432701 (Why is no real title available?)
- scientific article; zbMATH DE number 177798 (Why is no real title available?)
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)
