Workshop on Categories, Logic and Computation

28 July 2011, Research Institute for Mathematical Sciences, Kyoto University

(Venue: Room 478, General Research Building No.2, Kyoto University)

Programme (Tentative)

09:55-10:00	Opening
10:00-10:40	Naohiko Hoshino (Kyoto University)
	A Modified GoI Interpretation for a Linear Functional Programming Language and Its Adequacy
11:00-11:40	Craig Pastro (Kyushu University)
	Complementing Comonads
(lunch break)
13:30-14:30	Robin Cockett (University of Calgary)
	Differential Categories
15:00-15:40	Masahiro Hamano (JST)
	A Polarized Int Construction
16:00-16:40	Shin-ya Katsumata (Kyoto University)
	Relating Computational Effects by TT-Lifting
17:00-17:40	Ryu Hasegawa (University of Tokyo)
	A Categorical Reduction System and Its Properties
17:40-17:45	Closing
(dinner)

Abstracts

Naohiko Hoshino
A Modified GoI Interpretation for a Linear Functional Programming Language and Its Adequacy
Geometry of Interaction (GoI) introduced by Girard provides a semantics for linear logic and its cut elimination. Several extensions of GoI to programming languages have been proposed, but it is not discussed to what extent they capture behaviour of programs as far as we know. In this talk, we study GoI interpretation of a linear functional programming language (LFP). We observe that we can not extend the standard GoI interpretation to an adequate interpretation of LFP, and we propose a new adequate GoI interpretation of LFP by modifying the standard GoI interpretation. We derive the modified interpretation from a realizability model of LFP. We also relate the interpretation of recursion to cyclic computation (the trace operator in the category of sets and partial maps) in the realizability model.
Craig Pastro
Complementing Comonads
Robin Cockett
Differential Categories
Masahiro Hamano
A Polarized Int Construction
We extend Joyal-Street-Verity's Int construction ('96) in order to model dynamics arising from the polarized proof-theory of Laurent's MLLP. For this, we add multi-points (a semantical counterpart of polarization) to traced monoidal categories. Then the bidirectional information flow for Int morphisms is instantiated by the multipoints and the extended construction is captured by the Int construction in the presence of pull-backs.
Our construction yields a compact model of Hamano-Scott's denotational model of MLLP ('07) and a new compact example is given for the polarized Int construction over multi-pointed (Rel,+). If time permits, we show how the categorical form of Girard's execution formula (implicit in Int) characterizes the focalization property peculiar to polarized proof theory.
This is a joint work with Phil Scott.
Shin-ya Katsumata
Relating Computational Effects by TT-Lifting
We consider the problem of establishing a relationship between two monadic semantics of the lambda_c-calculus extended with algebraic operations. We show that two monadic semantics of any program are related if the relation includes value relations and is closed under the algebraic operations in the lambda_c-calculus.
Ryu Hasegawa
A Categorical Reduction System and Its Properties

Last Updated on 20 July 2011 by Masahito Hasegawa