scientific article; zbMATH DE number 3216998
From MaRDI portal
zbMath0134.01001MaRDI QIDQ5344164
Publication date: 1959
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Homotopical patch theory, Extracting a DPLL Algorithm, Effective results on a fixed point algorithm for families of nonlinear mappings, Term extraction and Ramsey's theorem for pairs, Polymorphic type inference and containment, Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones, A small complete category, Base-Complexity Classifications of QCB $$_0$$ 0 -Spaces, A parametrised functional interpretation of Heyting arithmetic, Polymorphic extensions of simple type structures. With an application to a bar recursive minimization, Computation on abstract data types. The extensional approach, with an application to streams, Unnamed Item, Hardwiring truth in functional interpretations, The equivalence of bar recursion and open recursion, Program extraction from classical proofs, Arithmetical conservation results, A note on equality in finite‐type arithmetic, Descriptive complexity of \(\mathsf{qc} \mathsf{b}_0\)-spaces, Internal Density Theorems for Hierarchies of Continuous Functionals, On computational properties of Cauchy problems generated by accretive operators, Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language, Constructive forcing, CPS translations and witness extraction in Interactive realizability, On bounded functional interpretations, A Computable Solution to Partee’s Temperature Puzzle, Unnamed Item, Nonflatness and totality, Unnamed Item, Intuitionistic fixed point logic, Unnamed Item, Recursion over realizability structures, On the fundamental conjecture of GLC, VI, An application of proof mining to nonlinear iterations, Well Quasi-orders and the Functional Interpretation, Quantitative continuity and Computable Analysis in Coq, Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs, Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves, The modified realizability topos, Two different strong normalization proofs?, The greatest common divisor: A case study for program extraction from classical proofs, Bar recursion over finite partial functions, Dialectica Interpretation with Fine Computational Control, Functional interpretations of linear and intuitionistic logic, Realizability models and implicit complexity, A realizability interpretation for classical analysis, Total sets and objects in domain theory, Uniform Heyting arithmetic, Unnamed Item, Strongly uniform bounds from semi-constructive proofs, A semantic proof of polytime soundness of light affine logic, Computability in higher types, P\(\omega\) and the completeness of type assignment, Operational set theory and small large cardinals, The metamathematics of ergodic theory, Injecting uniformities into Peano arithmetic, Explaining Deductive Inference, Feferman on Computability, On the Computability of the Fan Functional, Realizability interpretation of proofs in constructive analysis, Extensional models for polymorphism, The semantics of second-order lambda calculus, Functional Interpretations of Intuitionistic Linear Logic, Continuous and monotone machines, Unnamed Item, From Coinductive Proofs to Exact Real Arithmetic, THE CHARACTERIZATION OF WEIHRAUCH REDUCIBILITY IN SYSTEMS CONTAINING, The sequentially realizable functionals, A proof description language and its reduction system, Aspects of Categorical Recursion Theory, Light Dialectica Program Extraction from a Classical Fibonacci Proof, La théorie des fonctions récursives et ses applications. (Exposé d'information générale), On preserving the computational content of mathematical proofs: toy examples for a formalising strategy, Program extraction from normalization proofs
