The virtues of eta-expansion

DOI10.1017/S0956796800001301zbMath0833.68072OpenAlexW1988292549MaRDI QIDQ4850162

Neil Ghani, C. Barry Jay

Publication date: 9 October 1995

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796800001301

zbMATH Keywords

\(\lambda\)-calculusrewriting system

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Grammars and rewriting systems (68Q42)

Related Items (21)

Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract) ⋮ On the power of simple diagrams ⋮ Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type ⋮ Combining algebraic rewriting, extensional lambda calculi, and fixpoints ⋮ On the semantics of the universal quantifier ⋮ On modular properties of higher order extensional lambda calculi ⋮ Natural deduction and coherence for weakly distributive categories ⋮ Extensional proofs in a propositional logic modulo isomorphisms ⋮ Relative full completeness for bicategorical Cartesian closed structure ⋮ A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object ⋮ Combining first order algebraic rewriting systems, recursion and extensional lambda calculi ⋮ A confluent reduction for the λ-calculus with surjective pairing and terminal object ⋮ Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus ⋮ Game Semantics and Uniqueness of Type Inhabitance in the Simply-Typed λ-Calculus ⋮ On the semantics of classical disjunction ⋮ Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness ⋮ Big-step normalisation ⋮ The Simple Type Theory of Normalisation by Evaluation ⋮ Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions ⋮ On the intuitionistic force of classical search ⋮ The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type

Cites Work

• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Local adjunctions
• Formal category theory: Adjointness for 2-categories
• Pre-adjunctions in order enriched categories

This page was built for publication: The virtues of eta-expansion