The following pages link to (Q4093416):
Displaying 20 items.
- Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves (Q673628) (← links)
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility (Q896904) (← links)
- On strong normalization and type inference in the intersection type discipline (Q930868) (← links)
- Typing termination in a higher-order concurrent imperative language (Q979082) (← links)
- The calculus of constructions (Q1108266) (← links)
- Polymorphic rewriting conserves algebraic strong normalization (Q1176244) (← links)
- Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi (Q1208732) (← links)
- Typing untyped \(\lambda\)-terms, or reducibility strikes again! (Q1295368) (← links)
- Strong normalization from weak normalization in typed \(\lambda\)-calculi (Q1357009) (← links)
- Behavioural inverse limit \(\lambda\)-models (Q1434350) (← links)
- Non-strictly positive fixed points for classical natural deduction (Q1772778) (← links)
- Typing and computational properties of lambda expressions (Q1819575) (← links)
- Strong normalization and typability with intersection types (Q1924327) (← links)
- A simple proof of second-order strong normalization with permutative conversions (Q2566069) (← links)
- Reducibility: a ubiquitous method in lambda calculus with intersection types (Q2842839) (← links)
- On the Values of Reducibility Candidates (Q3637200) (← links)
- Two extensions of system F with (co)iteration and primitive (co)recursion principles (Q3653093) (← links)
- Modular properties of algebraic type systems (Q4645803) (← links)
- On the Versatility of Open Logical Relations (Q5041087) (← links)
- Algebraic types in PER models (Q5887524) (← links)