2 results
Benedetto Intrigila ; Giulio Manzonetto ; Andrew Polonsky.
The main observational equivalences of the untyped lambda-calculus have been characterized in terms of extensional equalities between B\"ohm trees. It is well known that the lambda-theory H*, arising by taking as observables the head normal forms, equates two lambda-terms whenever their B\"ohm trees […]
Published on January 29, 2019
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 stuck during the reduction. We show that such an extension allows to define a satisfying notion of B\"ohm(-like) tree and […]
Published on July 15, 2020