CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Compiling Linear Logic using Continuations

Jean-Philippe Bernardy (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Dan Rosén (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Nicholas Smallbone (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))

As System F is the logical foundation of functional programming, it has long been expected that Classical Linear Logic (CLL) is the logical foundation of concurrent programming. In particular, thanks to an involutive negation, its language of propositions correspond to protocols. This means that CLL provides the principles to integrate concurrency into functional programming languages. Aiming towards this integration, we translate the concurrency features of CLL into continuations, essentially via a negation-model of CLL into System F. Practically, the translation can be used to embed CLL programs into functional languages such as Haskell. We explain the properties of the interface between the two languages. In particular, using an example, we illustrate how the par (⅋) operator can solve practical functional programming problems.

Nyckelord: CPS, Classical Linear Logic, Concurrency, System F

Submitted to RTA-TLCA 2014.

Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2014-03-20.
CPL Pubid: 195331


Läs direkt!

Länk till annan sajt (kan kräva inloggning)