Revisiting Call-by-value Böhm trees in light of their Taylor expansion

Emma Kerinec, Giulio Manzonetto, Michele Pagani

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 st…