Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus

DOI10.1016/S0304-3975(96)80713-4zbMath0874.03017OpenAlexW4210699837MaRDI QIDQ672060

Barnaby P. Hilken

Publication date: 27 February 1997

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(96)80713-4

zbMATH Keywords

word problemconfluenceequational theorycatagorical rewritingsimply typed 2\(\lambda\)-calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items (3)

Coherence for bicategorical cartesian closed structure ⋮ Relative full completeness for bicategorical Cartesian closed structure ⋮ Dynamic game semantics

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The calculus of constructions
• Formal category theory: Adjointness for 2-categories
• Simulating expansions without expansions
• 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
• The virtues of eta-expansion

This page was built for publication: Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus