To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Compiling Linear Logic us… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Compiling Linear Logic using Continuations

Authors Jean-Philippe Bernardy
Dan Rosén
Nicholas Smallbone
Publication year 2014
Published at
Language en
Keywords CPS, Classical Linear Logic, Concurrency, System F
Subject categories Theoretical computer science


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.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?