The following pages link to The virtues of eta-expansion (Q4850162):
Displaying 23 items.
- Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus (Q672060) (← links)
- Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness (Q730088) (← links)
- Natural deduction and coherence for weakly distributive categories (Q1126244) (← links)
- Combining algebraic rewriting, extensional lambda calculi, and fixpoints (Q1349901) (← links)
- On the semantics of the universal quantifier (Q1371430) (← links)
- Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions (Q1575247) (← links)
- On the intuitionistic force of classical search (Q1575923) (← links)
- Relative full completeness for bicategorical Cartesian closed structure (Q2200828) (← links)
- The Simple Type Theory of Normalisation by Evaluation (Q2841227) (← links)
- Game Semantics and Uniqueness of Type Inhabitance in the Simply-Typed λ-Calculus (Q3007657) (← links)
- Big-step normalisation (Q3638919) (← links)
- On modular properties of higher order extensional lambda calculi (Q4571956) (← links)
- A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object (Q4630299) (← links)
- Combining first order algebraic rewriting systems, recursion and extensional lambda calculi (Q4632448) (← links)
- A confluent reduction for the λ-calculus with surjective pairing and terminal object (Q4895554) (← links)
- Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract) (Q5055860) (← links)
- On the power of simple diagrams (Q5055861) (← links)
- Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type (Q5055872) (← links)
- The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type (Q5111301) (← links)
- On the semantics of classical disjunction (Q5939825) (← links)
- Extensional proofs in a propositional logic modulo isomorphisms (Q6052705) (← links)
- Canonicity of proofs in constructive modal logic (Q6541161) (← links)
- Rewriting with extensional polymorphic \(\lambda \)-calculus (Q6560170) (← links)
