Pages that link to "Item:Q3322071"
From MaRDI portal
The following pages link to λ-definable functionals andβη conversion (Q3322071):
Displaying 20 items.
- Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus (Q428894) (← links)
- The relational model is injective for multiplicative exponential linear logic (without weakenings) (Q435194) (← links)
- Linear realizability and full completeness for typed lambda-calculi (Q556821) (← links)
- Extensional models for polymorphism (Q749518) (← links)
- Weak typed Böhm theorem on IMLL (Q866556) (← links)
- A characterization of lambda definable tree operations (Q918191) (← links)
- Word operation definable in the typed \(\lambda\)-calculus (Q1099156) (← links)
- Decidability and confluence of \(\beta\eta\text{top}_ \leqslant\) reduction in \({\mathbb{F}}_ \leqslant\) (Q1322474) (← links)
- Prelogical relations (Q1854557) (← links)
- What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics (Q2037304) (← links)
- Relating type-structures. Partial variations on a theme of Friedman and Statman (Q3026332) (← links)
- Provable isomorphisms of types (Q4017461) (← links)
- Identity of Proofs Based on Normalization and Generality (Q4650310) (← links)
- The range property fails for H (Q4899168) (← links)
- The Typed Böhm Theorem (Q4916173) (← links)
- (Q5013825) (← links)
- On dinaturality, typability and \(\beta\eta\)-stable models (Q5111327) (← links)
- (Q5219128) (← links)
- ETA-RULES IN MARTIN-LÖF TYPE THEORY (Q5240810) (← links)
- Intensional harmony as isomorphism (Q6612873) (← links)