CLL : a concurrent language built from logical principles

Abstract: "We present CLL, a concurrent programming language that symmetrically integrates functional and concurrent logic programming. First, a core functional language is obtained from a proof-term assignment to a variant of intuitionistic linear logic, called FOMLL, via the Curry-Howard isomorphism. Next, we introduce a Chemical Abstract Machine (CHAM) whose molecules are typed terms of this functional language. Rewrite rules for this CHAM are derived by augmenting proof-search rules for FOMLL with proof-terms. We show that this CHAM is a powerful concurrent language and that the linear connectives [x in circle], [reversed E], [+ in circle], - ̊and & correspond to process-calculi connectives for parallel composition, name restriction, internal choice, input prefixing and external choice respectively. We also demonstrate that communication and synchronization between CHAM terms can be performed through proof-search on the types of terms. Finally, we embed this CHAM as a construct in our functional language to allow interleaving functional and concurrent computation in CLL."