scientific article; zbMATH DE number 512774
From MaRDI portal
Publication:4281467
Recommendations
- Program extraction from normalization proofs
- Program extraction from proofs of weak head normalization
- scientific article; zbMATH DE number 1617311
- Practical program extraction from classical proofs
- Program extraction from classical proofs
- Proofs and programs: A naïve approach to program extraction
- Program extraction from large proof developments
- Extraction and verification of programs by analysis of formal proofs
- Refinement of classical proofs for program extraction
- scientific article; zbMATH DE number 749923
Cited in
(27)- Realizability interpretation of proofs in constructive analysis
- Proof normalization with nonstandard objects
- Algebraic proofs of cut elimination
- An arithmetic for non-size-increasing polynomial-time computation
- Towards the computational complexity of \(\mathcal{PR}^ \omega\)-terms
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
- An arithmetic for polynomial-time computation
- Intuitionistic model constructions and normalization proofs
- A context-based approach to proving termination of evaluation
- The simple type theory of normalisation by evaluation
- Eliminating proofs from programs
- Program extraction from proofs of weak head normalization
- scientific article; zbMATH DE number 4014708 (Why is no real title available?)
- Higman's lemma and its computational content
- An application of PER models to program extraction
- scientific article; zbMATH DE number 2006631 (Why is no real title available?)
- Two \textit{different} strong normalization proofs?
- First order marked types
- Logic for exact real arithmetic
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- Modal functional (``Dialectica) interpretation
- Constructive domains with classical witnesses
- Semantic analysis of normalisation by evaluation for typed lambda calculus
- Types for Proofs and Programs
- Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation
- Program extraction from normalization proofs
- Abbreviation templates
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4281467)
