Acknowledgements

Recently, a new logical system linear logic has been developed and come to be used to model various kinds computation. Geometry of Interaction (GoI) is a model of its cut-elimination, and GoI is also employed in such modelings. Since categorical interpre-and general way. Especially, there is a result that models quantum functional program-ming language using GoI. We survey notions on this work, supplementing proofs and propositions