Memoryful geometry of interaction II: recursion and adequacy

A general framework of Memoryful Geometry of Interaction (mGoI) is introduced recently by the authors. It provides a sound translation of lambda-terms (on the high-level) to their realizations by stream transducers (on the low-level), where the internal states of the latter (called memories) are exploited for accommodating algebraic effects of Plotkin and Power. The translation is compositional, hence “denotational,” where transducers are inductively composed using an adaptation of Barbosa’s coalgebraic component calculus. In the current paper we extend the mGoI framework and provide a systematic treatment of recursion—an essential feature of programming languages that was however missing in our previous work. Specifically, we introduce two new fixed-point operators in the coalgebraic component calculus. The two follow the previous work on recursion in GoI and are called Girard style and Mackie style: the former obviously exhibits some nice domain-theoretic properties, while...

• Type: Journal
• Year: 2016
• Where: POPL
• Authors: Koko Muroya, Naohiko Hoshino, Ichiro Hasuo
• Keywords: POPL 2016, Programming Languages