Sciweavers

Share
POPL
2016
ACM

Memoryful geometry of interaction II: recursion and adequacy

3 years 13 days ago
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...
Koko Muroya, Naohiko Hoshino, Ichiro Hasuo
Added 09 Apr 2016
Updated 09 Apr 2016
Type Journal
Year 2016
Where POPL
Authors Koko Muroya, Naohiko Hoshino, Ichiro Hasuo
Comments (0)
books