Simulating expansions without expansions
From MaRDI portal
Publication:4322432
DOI10.1017/S0960129500000505zbMath0831.03004MaRDI QIDQ4322432
Roberto Di Cosmo, Delia Kesner
Publication date: 18 February 1996
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
confluence; rewriting system; strong normalization; sums; typed \(\lambda\)-calculus; bounded recursion; expansion rules; extensional equalities; unbounded recursion
Related Items
Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus, Combining algebraic rewriting, extensional lambda calculi, and fixpoints, Developing developments
Cites Work
- Unnamed Item
- The lambda calculus. Its syntax and semantics. Rev. ed.
- On the implementation of abstract data types by programming language constructs
- Strong normalization for typed terms with surjective pairing
- The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
- An algebraic interpretation of the \(\lambda\beta K\)-calculus; and an application of a labelled \(\lambda\)-calculus