Journal / Conference Papers



Besides the presentations in conferences, I gave the following presentations in research workshops and colloquium.

PhD Thesis

Shin-ya Katsumata. A Generalisation of Pre-Logical Predicates and Its Applications.
PhD thesis, School of Informatics, Edinburgh University, submitted 2004, accepted 2005. (PDF)
Abstract: This thesis proposes a generalisation of pre-logical predicates to simply typed formal systems and their categorical models. We analyse the three elements involved in pre-logical predicates --- syntax, semantics and predicates --- within a categorical framework for typed binding syntax and semantics. We then formulate generalised pre-logical predicates and show two distinguishing properties: a) equivalence with the basic lemma and b) closure of binary pre-logical relations under relational composition. To test the adequacy of this generalisation, we derive pre-logical predicates for various calculi and their categorical models including variations of lambda calculi and non-lambda calculi such as many-sorted algebras as well as first-order logic. We then apply generalised pre-logical predicates to characterising behavioural equivalence. Examples of constructive data refinement of typed formal systems are shown, where behavioural equivalence plays a crucial role in achieving data abstraction.

MSc Thesis

Shin-ya Katsumata. A Simply Typed lambda Calculus with Type Substitution.
M.Sc. thesis, Research Institute for Mathematical Sciences, Kyoto University, 2000.
Abstract: In this paper, we propose a lambda^S calculus, a simply typed lambda calculus with a rule of type substitution. A distinguishing feature of the lambda^S calculus is to treat type substitution not as meta operation but as logical rule. This yileds a finer equational theory that properly accounts for implicit polymorphism such as the one embodied in ML. We define a type system and an equational theory of the lambda^S calculus and show that it is sound with respect to a categorical semantics on Mitchell and Scedrov's iml-category. We then give a translation from Milner's lambda^let calculus to lambda^S calculus, which reveales that Leroy's type-dicrected boxing and unboxing corresponds to the type isomorphism definable in lambda^S between types with substitution and the corresponding simple types.