Search

• < Previous
• 1
• Next >

Revisiting Call-by-value B\"ohm trees in light of their Taylor expansion

The call-by-value lambda calculus can be endowed with permutation rules, arising from linear logic proof-nets, having the advantage of unblocking some redexes that otherwise get stuck during the reduction. We show that such an extension allows to define a satisfying notion of B\"ohm(-like) tree and&nbsp;[&hellip;]