This paper studies the strength of embedding Call-by-Name ({ \tt dCBN}) and Call-by-Value ({ \tt dCBV}) into a unifying framework called the Bang Calculus ({ \tt dBANG}). These embeddings enable establishing (static and dynamic) properties of { \tt dCBN} and { \tt dCBV} through their respective counterparts in { \tt dBANG}. While some specific static properties have been already successfully studied in the literature, the dynamic ones are more challenging and have been left unexplored. We accomplish that by using a standard embedding for the (easy) { \tt dCBN} case, while a novel one must be introduced for the (difficult) { \tt dCBV} case. Moreover, a key point of our approach is the identification of { \tt dBANG} diligent reduction sequences, which eases the preservation of dynamic properties from { \tt dBANG} to { \tt dCBN}/{ \tt dCBV}. We illustrate our methodology through two concrete applications: confluence/factorization for both { \tt dCBN} and { \tt dCBV} are respectively derived from confluence/factorization for { \tt dBANG}.
Categories: cs.LO