The following pages link to (Q4281467):
Displaying 22 items.
- Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation (Q651316) (← links)
- Program extraction from normalization proofs (Q817701) (← links)
- Abbreviation templates (Q851527) (← links)
- Realizability interpretation of proofs in constructive analysis (Q1015381) (← links)
- Proof normalization with nonstandard objects (Q1178706) (← links)
- Algebraic proofs of cut elimination (Q1349247) (← links)
- An arithmetic for non-size-increasing polynomial-time computation (Q1827388) (← links)
- Towards the computational complexity of \(\mathcal{PR}^ \omega\)-terms (Q1899150) (← links)
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting) (Q2232317) (← links)
- An arithmetic for polynomial-time computation (Q2500489) (← links)
- Intuitionistic model constructions and normalization proofs (Q2785696) (← links)
- A context-based approach to proving termination of evaluation (Q2805157) (← links)
- The simple type theory of normalisation by evaluation (Q2841227) (← links)
- Eliminating proofs from programs (Q2844809) (← links)
- Program extraction from proofs of weak head normalization (Q2852349) (← links)
- Higman’s Lemma and Its Computational Content (Q3305561) (← links)
- Two different strong normalization proofs? (Q4645812) (← links)
- (Q4989402) (← links)
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs (Q5019018) (← links)
- (Q5028422) (← links)
- (Q5856423) (← links)
- Semantic analysis of normalisation by evaluation for typed lambda calculus (Q5889884) (← links)
