The following pages link to (Q4281467):
Displaying 17 items.
- Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation (Q651316) (← links)
- Program extraction from normalization proofs (Q817701) (← links)
- Realizability interpretation of proofs in constructive analysis (Q1015381) (← 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)
- A Context-based Approach to Proving Termination of Evaluation (Q2805157) (← links)
- The Simple Type Theory of Normalisation by Evaluation (Q2841227) (← 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)
