Our paper “Con­tin­u­a­tion-Pass­ing to Di­rect Style: Typed and Tight” (Mar­ius Müller, Philipp Schus­ter
Re­searcherPhilipp Schus­ter, Jonathan Brachthäuser
Head of the SE re­search groupJonathan Im­manuel Brachthäuser, and Klaus Os­ter­mann) has been ac­cepted for pub­li­ca­tion at the In­ter­na­tional Con­fer­ence on Ob­ject-Ori­ented Pro­gram­ming, Sys­tems, Lan­guages and Ap­pli­ca­tions (OOP­SLA 2023).

Ab­stract

Trans­lat­ing pro­grams into con­tin­u­a­tion-pass­ing style is a well-stud­ied tool to ex­plic­itly deal with the con­trol struc­ture of pro­grams. This is use­ful, for ex­am­ple, for com­pi­la­tion.

In a typed set­ting, there also is a log­i­cal in­ter­pre­ta­tion of such a trans­la­tion as an em­bed­ding of clas­si­cal logic into in­tu­ition­is­tic logic. A nat­u­rally aris­ing ques­tion is whether there is an in­verse trans­la­tion back to di­rect style. The an­swer to this ques­tion de­pends on how the con­tin­u­a­tion-pass­ing trans­la­tion is de­fined and on the do­main of the in­verse trans­la­tion. In gen­eral, trans­lat­ing pro­grams from con­tin­u­a­tion-pass­ing style back to di­rect style re­quires the use of con­trol op­er­a­tors to ac­count for the use of con­tin­u­a­tions in non-triv­ial ways.

We pre­sent two lan­guages, one in di­rect style and one in con­tin­u­a­tion-pass­ing style. Both lan­guages are typed and equipped with an ab­stract ma­chine se­man­tics. More­over, both lan­guages allow for non-triv­ial con­trol flow.

We fur­ther pre­sent a trans­la­tion to con­tin­u­a­tion-pass­ing style and a trans­la­tion back to di­rect style. We show that both trans­la­tions are type-pre­serv­ing and also pre­serve se­man­tics in a very pre­cise way giv­ing an op­er­a­tional cor­re­spon­dence be­tween the two lan­guages.

More­over, we show that the com­po­si­tions of the trans­la­tions are well-be­haved. In par­tic­u­lar, they are syn­tac­tic one-sided in­verses on the full lan­guage and full syn­tac­tic in­verses when re­stricted to triv­ial con­trol flow.

More about this pub­li­ca­tion

Pub­li­ca­tions