CLL: A Concurrent Language Built from Logical Principles

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# #, #, 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