A pi calculus term assignment for Dual Intuitionistic Logic
Based on the work of Milner, Abramsky, Bellin and Scott we propose a pi-calculus term assignment for the linear fragment LDIL of Dual Intuitionistic Logic (DIL) restricted to the operator of ``subtraction'' \ which is dual to implication typical of intuitionistic logic. We prove that this translation is sound with respect to cut elimination and show how this system can clarify some logical issues of translations from lambda-calculus into \pi-calculus. A more extensive study of the \pi-calculus fragment corresponding to our term assignment and a model of coherent spaces for Dual Intuitionistic Logic are left for future research.
Return to Conference Programme