Call-by-name extensionality and confluence

DOI10.1017/S095679681700003XzbMATH Open1418.68033MaRDI QIDQ5372008FDOQ5372008

Authors: Philip Johnson-Freyd, Paul Downen, Zena M. Ariola 

Publication date: 23 October 2017

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

Recommendations

• A confluent reduction for the extensional typed \(\lambda\)-calculus with pairs, sums, recursion and terminal object
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• Simulating expansions without expansions
• On modular properties of higher order extensional lambda calculi
• Extensional Rewriting with Sums

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Functional programming and lambda calculus (68N18)

Cites Work

• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Title not available (Why is that?)
• The lambda calculus. Its syntax and semantics. Rev. ed.
• \(\lambda\mu\)-calculus and Böhm's theorem
• The duality of computation
• Typing streams in the \({\Lambda}{\mu}\)-calculus
• An approach to call-by-name delimited continuations
• A call-by-name lambda-calculus machine
• Title not available (Why is that?)
• Reduction system for extensional lambda-mu calculus
• Title not available (Why is that?)
• Completeness of continuation models for \(\lambda_\mu\)-calculus
• Unique normal forms for lambda calculus with surjective pairing
• Skew confluence and the lambda calculus with letrec
• Parametric polymorphism and operational equivalence
• The duality of computation under focus
• Polarised intermediate representation of lambda calculus with sums
• The stack calculus
• The Duality of Construction

Cited In (1)

• Relating two semantics of locally scoped names

This page was built for publication: Call-by-name extensionality and confluence

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5372008)