Completeness of algebraic CPS simulations


Simon Perdrix, LIG, CAPP. 16 mai 2012 10:15 limd 2:00:00
Abstract:

The algebraic lambda calculus and the linear algebraic lambda calculus are two extensions of the classical lambda calculus with linear combinations of terms. They arise independently in distinct contexts: the former is a fragment of the differential lambda calculus, the latter is a candidate lambda calculus for quantum computation. Their operational semantics differ in the treatment of applications and algebraic rules. We show how these two languages can simulate each other using an algebraic extension of the well-known call-by-value and call-by-name CPS translations. We prove that the simulations are sound and complete. Joint work with Ali Assaf, Alejandro Díaz-Caro, Christine Tasson and Benoît Valiron.