Research
Journal / Conference Papers
 Shinya Katsumata, Exequiel Rivas, Tarmo Uustalu.
Interaction laws of monads and comonads.
In Proceedings of the 35th Annual ACM/IEEE Symposium on
Logic in Computer Science, LICS 2020, To appear.
(c) IEEE.
 Koki Nishizawa, Shinya Katsumata, Yuichi Komorida.
Stone Dualities from Opfibrations.
In Proceedings of Relational and Algebraic Methods in Computer Science  18th International Conference, RAMiCS 2020, LNCS 12062, Springer, 2020.
(c) Springer.
 Juraj Kolcák, Jérémy Dubut, Ichiro Hasuo, Shinya Katsumata, David Sprunger, Akihisa Yamada.
Relational Differential Dynamic Logic.
In Proceedings of Tools and Algorithms for the Construction
and Analysis of Systems  26th International Conference, TACAS
2020, LNCS 12078, Springer, 2020.
(c) Springer.
 Tetsuya Sato, Gilles Barthe, Marco Gaboardi, Justin Hsu, ShinYa Katsumata.
approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy.
In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, .
(c) IEEE.
 Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, ShinYa Katsumata.
Probabilistic Relational Reasoning via Metrics.
In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, .
(c) IEEE.
 Yuichi Komorida, ShinYa Katsumata, Nick Hu, Bartek Klin, Ichiro Hasuo.
Codensity Games for Bisimilarity.
In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, .
(c) IEEE.
 David Sprunger, ShinYa Katsumata.
Differentiable Causal Computations via Delayed Trace.
In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, .
(c) IEEE.
 Thorsten Wißmann, Jérémy Dubut, Shinya Katsumata, Ichiro Hasuo.
Path Category for Free  Open Morphisms from Coalgebras with Nondeterministic Branching.
In
Proceedings of Foundations of Software Science and Computation Structures  22nd International Conference, FOSSACS 2019
, LNCS 11425, pp.523540, Springer, 2018.
(c) Springer.
(Paper page)
 Shinya Katsumata, Tetsuya Sato, Tarmo Uustalu.
Codensity Lifting of Monads and its Dual.
In Logical Methods in Computer Science, 14(4), 2018.
(Paper page)
 Shinya Katsumata.
A DoubleCategory Theoretic Analysis of Graded Linear Exponential Comonad.
In Proceedings of Foundations of Software Science and Computation Structures  21st International Conference, FOSSACS 2018, LNCS 10803, pp. 110127, Springer, 2018.
(c) Springer.
(Paper page)
 David Sprunger, Shinya Katsumata, Jérémy Dubut, Ichiro Hasuo.
Fibrational Bisimulations and Quantitative Reasoning.
In
Proceedings of Coalgebraic Methods in Computer Science  14th IFIP WG 1.3 International Workshop, CMCS 2018
, LNCS 1202, pp. 190213, Springer, 2018.
(c) Springer.

Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shinya Katsumata, Ikram Cherigui
.
A Semantic Account of Metric Preservation.
In Proceedings of the 41th Symposium on Principles of Programming Languages POPL 2017, pp. 545556, ACM, 2017.

Marco Gaboardi, Shinya Katsumata, Dominic Orchard, Flavien Breuvart, Tarmo Uustalu
.
Combining Effects and Coeffects via Grading.
In Proceedings of the 21th ACM SIGPLAN International Conference on Functional Programming, pp. 476489, ACM, 2016.
(c) ACM.
(Paper page)
 Soichiro Fujii, Shinya Katsumata, PaulAndré Melliès.
Towards a Formal Theory of Graded Monads.
In Proceedings of the 19th International Conference on Foundations of Software Science and Computation Structures 2016, LNCS 9634, pp. 513530. Springer, Heidelberg, 2016.
(c) Springer.
Abstract:
We initiate a formal theory of graded monads whose purpose is to adapt
and to extend the formal theory of monads developed by Street in the
early 1970's. We establish in particular that every graded monad can
be factored in two different ways as a strict action transported along
a left adjoint functor. We also explain in what sense the first
construction generalizes the EilenbergMoore construction while the
second construction generalizes the Kleisli construction. Finally, we
illustrate the EilenbergMoore construction on the graded state monad
induced by any object V in a symmetric monoidal closed
category~$\Ccategory$.
 Shinya Katsumata and Tetsuya Sato.
Codensity Liftings of Monads.
In Proceedings of the 6th Conference on Algebra and Coalgebra in Computer Science, Volume 35 of LIPIcs.
(Paper page)
Abstract:
We introduce a method to lift monads on the base category of a
fibration to its total category using codensity monads. This
method, called codensity lifting, is applicable to various
fibrations which were not supported by the categorical
TTlifting. After introducing the codensity lifting, we
illustrate some examples of codensity liftings of monads along the
fibrations from the category of preorders, topological spaces and
extended psuedometric spaces to the category of sets, and also the
fibration from the category of binary relations between measurable
spaces. We next study the liftings of algebraic operations to
the codensitylifted monads. We also give a characterisation of the
class of liftings (along posetal fibrations with fibred small
limits) as a limit of a certain large diagram.
 Shinya Katsumata.
Parametric Effect Monads and Semantics of Effect Systems.
In Proceedings of the 41th Symposium on Principles of Programming Languages POPL 2014, pp. 633645, ACM, 2014.
(Paper page,Slides for PPL2014(Japanese))
Abstract:
We study fundamental properties of a generalisation of monad
called parametric effect monad, and apply it to the
interpretation of general effect systems whose effects have
sequential composition operators. We show that parametric effect
monads admit analogues of the structures and concepts that exist
for monads, such as Kleisli triples, the state monad and the
continuation monad, Plotkin and Power's algebraic operations,
and the categorical TTlifting. We also show a systematic
method to generate both effects and a parametric effect monad
from a monad morphism. Finally, we introduce two effect systems
with explicit and implicit subeffecting, and discuss their
denotational semantics and the soundness of effect systems.
 Shinya Katsumata and Tetsuya Sato.
Preorders on Monads and Coalgebraic Simulations.
In Proceedings of the 16th International Conference on Foundations of Software Science and Computation Structures 2013, LNCS 7794, pp.145160. Springer, Heidelberg, 2013.
(c) Springer.
(Paper page,PDF,Corrections)
Abstract:
We study the construction of preorders on Setmonads by the semantic
TTlifting. We show the universal property of this construction, and
characterise the class of preorders on a monad as a limit of a
Card^opchain. We apply these theoretical results to identifying
preorders on some concrete monads, including the powerset monad,
maybe monad, and their composite monad. We also relate the
construction of preorders and coalgebraic formulation of
simulations.
 Koji Nakazawa and Shinya Katsumata.
Extensional Models of Untyped LambdaMu Calculus.
In Proceedings of the Fourth International Workshop on Classical Logic and Computation 2012, Electronic Proceedings in Theoretical Computer Science, volume 97, pp. 3547, 2012.
(Paper page)
 Shinya Katsumata.
Relating computational effects by TTlifting.
In Information and Computation (Special issue on ICALP 2011), Volume 222, pp. 228246, 2013.
(ScienceDirect,PDF)
 Shinya Katsumata.
Relating Computational Effects by TTLifting.
In Proceedings of the 38th International Colloquium on Automata, Languages and Programming, LNCS 6756, pp. 174185, 2011.
(c) Springer.
(Springer,PDF)
Abstract:
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.
 Shinya Katsumata.
Categorical Descriptional Composition.
In Proceedings of the 8th Asian Symposium on Programming Languages and Systems, LNCS 6461, pp. 222238, Springer 2010.
(c) Springer.
(Springer,PDF)
Abstract:
Descriptional composition is a method to fuse two term
transformation algorithms described by attribute couplings
(AC, attribute grammars over terms) into one. In this article,
we provide a general categorical framework for the
descriptional composition based on traced symmetric monoidal
categories and the Int construction by Joyal et al. We
demonstrate that this framework can handle the descriptional
composition of SSURACs, nondeterministic SSURACs, quasiSSUR
ACs and quasiSSUR stack ACs.
 Masahito Hasegawa and Shinya Katsumata.
A note on the biadjunction between 2categories of traced monoidal categories and tortile monoidal categories.
In Mathematical Proceedings of Cambridge Philosophical Society, volume 148, pp. 107109, 2009.
(c) Cambridge Philosophical Society.
(PDF)
 Shinya Katsumata.
A Characterisation of Lambda Definability with Sums via TTClosure Operators.
In Proceedings of the 17th Annual Conference on Computer Science Logic, LNCS 5213, pp. 278292. Springer 2008.
(c) Springer.
(Springer,PDF)
Abstract:
We give a new characterisation of morphisms that are definable by the
interpretation of the simply typed lambda calculus with sums in any biCartesian
closed category. The TTclosure operator will be used to construct the category
in which the collection of definable morphisms at sum types can be characterised
as the coproducts of such collections at lower types.
 Shinya Katsumata.
Attribute Grammars and Categorical Semantics.
In Proceedings of the 35th International Colloquium on Automata, Languages and Programming, LNCS 5126, pp. 271282. Springer 2008.
(c) Springer.
(Springer,PDF)
Abstract:
This is the conference version of the manuscript
A New Foundation of Attribute Grammars in Traced Symmetric Monoidal Categories.
 Shinya Katsumata and Susumu Nishimura.
Algebraic Fusion of Functions with an Accumulating Parameter and Its Improvement.
In Journal of Functional Programming (Special issue on ICFP 2006), volume 18, issue 56, pp. 781819, 2008.
(Cambridge Journals)
Abstract:
This is the journal version of the following paper.
 Shinya Katsumata and Susumu Nishimura.
Algebraic Fusion of Functions with an Accumulating Parameter and Its Improvement.
In Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, pp. 227238, ACM, 2006.
(c) ACM.
(author's version in PDF,ACM)
Abstract:
We present a unifying solution to the problem of fusion of
functions, where both the producer function and the consumer
function have one accumulating parameter. The key idea in this
development is to formulate the producer function as a function
which computes over a monoid of {\em data context}s.
Upon this formulation, we develop a fusion method called {\em
algebraic fusion} based on the elementary theory of universal
algebra and monoids. The producer function is fused with a monoid
homomorphism that is derived from the definition of the consumer
function, and is turned into a higherorder function~$f$ that
computes over the monoid of endofunctions.
We then introduce a general concept called {\em improvement}, in
order to reduce the cost of computing over the monoid of
endofunctions (i.e., function closures). An improvement of the
function $f$ via a monoid homomorphism $h$ is a function $g$ that
satisfies $f=h\circ g$.
This provides a principled way of finding a firstorder function
representing a solution to the fusion problem. It also presents a
clean and unifying account for varying fusion methods that have
been proposed so far. Furthermore, we show that our method
extends to support partial and infinite data structures, by means
of an appropriate monoid structure. (The trip to the conference
was partially supported by Kyoto Daigaku Kyouiku Kenkyuu Shinkou
Zaidan.)
 Shinya Katsumata.
A Semantic Formulation of TTlifting and Logical Predicates for Computational Metalanguage.
In Proceedings of the 14th Annual Conference on Computer Science Logic, LNCS 3634, pp. 87102. Springer 2005.
(c) Springer.
(PDF)
Abstract:
A semantic formulation of Lindley and Stark's TTlifting is
given. We first illustrate our semantic formulation of the
TTlifting in Sets with several examples, and apply it to the logical
predicates for Moggi's computational metalanguage. We then abstract
the semantic TTlifting as the lifting of strong monads across
bifibrations with lifted symmetric monoidal closed structures.
(This work further develops the example I considered in chapter 4
of my PhD thesis. The trip to the conference was partially
supported by Saneyoshi Shogakukai.)
 Shinya Katsumata.
A Generalisation of Prelogical Predicates to Simply Typed Formal Systems.
In Proceedings of the 31st International Colloquium on Automata, Languages and Programming, LNCS 3142, pp. 831845. Springer 2004.
(c) Springer.
(PDF)
Abstract:
We generalise the notion of prelogical predicates to arbitrary
simply typed formal systems and their categorical models. We establish
the basic lemma of prelogical predicates and composability of binary
prelogical relations in this generalised setting. This generalisation
takes place in a framework for typed higherorder abstract syntax and
semantics.
 Jo Hannay, Shinya Katsumata and Donald Sannella.
Semantic and Syntactic Approaches to Simulation Relations.
In Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science, LNCS 2747, pp. 6891. Springer 2003.
(c) Springer.
Abstract:
Simulation relations are tools for establishing the correctness
of data refinement steps. In the simplytyped lambda calculus, logical
relations are the standard choice for simulation relations, but they
suffer from certain shortcomings; these are resolved by use of the
weaker notion of prelogical relations instead. Developed from a
syntactic setting, abstraction barrierobserving simulation relations
serve the same purpose, and also handle polymorphic operations.
Meanwhile, secondorder prelogical relations directly generalise
prelogical relations to polymorphic lambda calculus (System F). We
compile the main refinementpertinent results of these various notions
of simulation relation, and try to raise some issues for aiding their
comparison and reconciliation.
 Shinya Katsumata.
Behavioural equivalence and Indistinguishability in HigherOrder Typed Languages.
In Proceedings of the 16th International Workshop on Recent Trends in Algebraic Development Techniques, LNCS 2755, pp. 284298. Springer 2002.
(c) Springer.
(PDF)
Abstract:
We extend the study of the relationship between behavioural
equivalence and indistinguishability relation to the simply typed
lambda calculus, where higherorder types are available. The
relationship between these two notions is established in terms of
factorisability. The main technical tool of this study is prelogical
relations, which give a precise characterisation of behavioural
equivalence. We then consider a higherorder logic to reason about
models of the simply typed lambda calculus, and relate the resulting
standard satisfaction relation to behavioural satisfaction.
 Alan Mycroft, Atsushi Ohori and Shinya Katsumata.
Comparing TypeBased and ProofDirected Decompilation.
In Proceedings of the 8th Working Conference on Reverse Engineering, pp. 362367. IEEE Press 2001.
(c) IEEE.
Abstract:
In the past couple of years interest in decompilation has widened
from its initial concentration on reconstruction of control flow
into wellfoundedintheory methods to reconstruct type
information. Mycroft described TypeBased Decompilation and
Katsumata and Ohori described ProofDirected Decompilation. This
note summarises the two approaches and identifies their
commonality, strengths and weaknesses; it concludes by suggesting
how they may be integrated.
 Shinya Katsumata and Atsushi Ohori.
ProofDirected Decompilation of LowLevel Code.
In Proceedings of the 10th European Symposium on Programming, LNCS 2028, pp. 352366. Springer 2001.
(c) Springer.
Abstract:
We present a proof theoretical method for decompiling
lowlevel code to the typed lambda calculus. We first define a proof
system for a lowlevel code language based on the idea of CurryHoward
isomorphism. This allows us to regard an executable code as a proof in
intuitionistic propositional logic. As being a proof of intuitionistic
logic, it can be translated to an equivalent proof of natural deduction
proof system. This property yields an algorithm to translate a given
code into a lambda term. Moreover, the resulting lambda term is not a
trivial encoding of a sequence of primitive instructions, but reflects
the behavior of the given program. This process therefore serves as
proofdirected decompilation of a lowlevel code language to a
highlevel language. We carry out this development for a subset of Java
Virtual Machine instructions including most of its features such as
jumps, object creation and method invocation. The proofdirected
decompilation algorithm has been implemented, which demonstrates the
feasibility of our approach.
Manuscripts
 Naohiko Hoshino and Shinya Katsumata.
Int Construction and Semibiproducts.
(RIMS1676)
Abstract:
We study a relationship between the Int construction of Joyal et
al. and a weakening of biproducts called semibiproducts. We then
provide an application of geometry of interaction interpretation for
the multiplicative additive linear logic (MALL for short) of Girard.We
consider not biproducts but semibiproducts because in general the Int
construction does not preserve biproducts. We show that Int
construction is left biadjoint to the forgetful functor from the 2
category of compact closed categories with semibiproducts to the
2category of traced symmetric monoidal categories with
semibiproducts. We then illustrate a traced distributive symmetric
monoidal category with biproducts B(Pfn) and relate the interpretation
of MALL in Int(B(Pfn)) to token machines defined over weighted MALL
proofs.
 Shinya Katsumata.
A New Foundation of Attribute Grammars in Traced Symmetric Monoidal Categories.
(PDF)
Abstract:
In this paper we propose a new categorical formulation of
attribute grammars in traced symmetric monoidal categories. The
new formulation, called monoidal attribute grammars, concisely
captures the essence of the classical attribute grammars. We
study monoidal attribute grammars in two categories: Rel^+ and
wCPPO. It turns out that in Rel^+ monoidal attribute grammars
correspond to the graphtheoretic representation of attribute
dependencies, while in wCPPO monoidal attribute grammars are
equivalent to Chirica and Martin's Ksystems. We also show that
in traced symmetric monoidal closed categories every monoidal
attribute grammar is equivalent to the one which does not use
inherited attributes.
Talks
Besides the presentations in conferences, I gave the following
presentations in research workshops and colloquium.

A DoubleCategory Theoretic Analysis of Graded Linear Exponential Comonad.
Foundations of Software Science and Computation Structures  21st International Conference, FOSSACS 2018
,
14 Apr, 2018.

Graded monads and the semantics of effect systems.
QSLC (Quantative Semantics of Logic and Computation) workshop, affiliated workshop of Computer Science Logic 2016, Aix Marseille University, France,
2 Sept, 2016.

On Graded coalgebras of graded linear exponential comonad.
CRECOGI (Concurrent, Resourceful and Effectful COmputation, by Geometry of Interaction) workshop, affiliated workshop of Computer Science Logic 2016, AixMarseille University, France,
28 Aug, 2016.

From DCC to local DCC.
理論計算機科学と圏論ワークショップ CSCAT 2015, 理化学研究所計算科学研究機構, 神戸,
17 Mar, 2016.

From DCC to local DCC.
Shonan Meeting on Logic and Verification Methods in Security and Privacy, Shonan Kokusai Village, Kanagawa,
28 Oct, 2015.

On Graded Monads.
CRECOGI (Concurrent, Resourceful and Effectful COmputation, by Geometry of Interaction)
kickoff workshop, RIMS, Kyoto university, Kyoto,
11 Jul, 2015.

ファイブレーションと余稠密モナドによるモナドの持ち上げ.
理論計算機科学と圏論ワークショップ CSCAT 2015, 鹿児島大学,
15 Mar, 2015.

モナド、代数理論と計算効果.
Workshop on Programming and Programming Languages, Matsuyama,
4 Mar, 2015.

Parametric Effect Monads and Semantics of Effect Systems.
Programming Languages Interest Group, The University of Edinburgh, Edinburgh,
3 Nov, 2014.

Parametric Effect Monads and Semantics of Effect Systems.
University of Dundee, Dundee,
30 Oct, 2014.

Relating Computational Effects by TTLifting (invited talk).
Twelfth International Symposium on Functional and Logic Programming, Ishikawa Prefectural Museum of Art, Kanazawa, Japan,
6 June, 2014.

Logical Relations for Monads and Categorical TTLifting (invited talk).
Mathematically Structured Functional Programming, Grenoble, France,
12 Apr, 2014.

Parametric Effect Monads and Semantics of Effect Systems.
Workshop on Programming and Programming Languages, Aso,
6 Mar, 2014.

Parametric Effect Monads and Semantics of Effect Systems.
Institute of Cybernetics at Tallinn University of Technology, Tallinn, Estonia,
28 Nov, 2013.

Relating Computational Effects by TTLifting (invited talk).
House of the Brotherhood of the Blackheads, Tallinn, Estonia,
21 Nov, 2013.

Lecture on Categorical Approach to Logic.
Kisoron Summer School, Keio University, Tokyo,
5  8 Aug, 2013.

A Generic Soundness Result for Effect Systems (Poster).
Asian Symposium on Programming Languages and Systems, Kyoto,
12 Dec, 2012.

効果システムの健全性について (Poster).
Workshop on Programming and Programming Languages, Shirahama,
9 Mar, 2012.

A Generic Soundness Result for Effect Systems.
Logic and Interaction 2012, Marseille, France,
13 Feb, 2012.

A Categorical Approach to Attribute Grammars.
ALOCO Seminar on Formal Methods for Componentbased Programming, Yaouunde university, Cameroon,
13 Jan, 2012.

Relating Computational Effects by TTLifting.
Workshop on linear logic (GoI, TSMCs and Implicit Complexity), Kyoto university,
7 Nov, 2011.

A Categorical Approach to Attribute Grammars.
Tokyo Programming Seminar, National Institute of Informatics, Tokyo,
23 Jun, 2011.

Relating Computational Effects by TTLifting.
Adventures of Categories, Research Institute for Mathematical Sciences, Kyoto university,
1 Jun, 2011.

Relating Computational Effects by TTLifting.
Asian Workshop on Foundations of Software, Shanghai,
May, 2011.

モナド的意味論の比較問題について(ポスター).
Workshop on Programming and Programming Languages, Sapporo,
March, 2011.

A Gentle Introduction to Denotational Semantics.
Workshop on Adventures in Categories, Research Institute for Mathematical Sciences, Kyoto university,
November, 2010.

Fullness of Monadic Translation by TTLifting.
LOLA 2010 Syntax and Semantics of LowLevel Languages, Edinburgh university,
July, 2010.

A Categorical Geometory of Interaction for Additives.
Laboratoire Preuves, Programmes et SystemÈes universitÉ Paris Diderot  Paris 7,
March, 2010.

Logical Predicates for Monads by TTLifting.
Workshop on Category Theory, Computer Science and Topology, Shinshu university,
October, 2009.

Attribute Grammars and Categorical Semantics.
Workshop on Geometry of Interaction, Traced Monoidal Categories and
Implicit Complexity,
August, 2009.

A note on the biadjunction between 2categories of traced monoidal categories and tortile monoidal categories.
Workshop on Computer Science and Category Theory, Chiba university,
March, 2009.

Attribute Grammars and Categorical Semantics.
Workshop on Mathematics for Pressing Problems in Computer Science, Research Institute for Mathematical Sciences, Kyoto university,
June, 2008.

Attribute Grammars and Traced Symmetric Monoidal Categories.
Workshop on Computer Science and Category Theory, Tohoku university,
March, 2008.

TTlifting and Logical Predicates for Computational Types.
Workshop on Computer Science and Category Theory, Kyoto university,
March, 2007.

An Algebraic Approach to Shortcut Fusion of Functions with an Accumulating Parameter.
Workshop on Programming and Programming Languages, Ogoto,
March, 2007.

An Algebraic Approach to Shortcut Fusion of Functions with an Accumulating Parameter.
TOPS Seminar, the university of Tokyo,
January, 2006.

Behavioural Equivalence and Indistinguishability in HigherOrder Typed Languages.
Advanced Industrial Science and Technolgy, Amagasaki,
August, 2003.
PhD Thesis
Shinya Katsumata.
A Generalisation of PreLogical Predicates and Its Applications.
PhD thesis, School of Informatics, Edinburgh University, submitted 2004, accepted 2005.
(PDF)
Abstract:
This thesis proposes a generalisation of prelogical
predicates to simply typed formal systems and their
categorical models. We analyse the three elements involved
in prelogical predicates  syntax, semantics and
predicates  within a categorical framework for typed
binding syntax and semantics. We then formulate
generalised prelogical predicates and show two
distinguishing properties: a) equivalence with the basic
lemma and b) closure of binary prelogical relations under
relational composition. To test the adequacy of this
generalisation, we derive prelogical predicates for
various calculi and their categorical models including
variations of lambda calculi and nonlambda calculi such
as manysorted algebras as well as firstorder logic. We
then apply generalised prelogical 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
Shinya 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 imlcategory. We then give a
translation from Milner's lambda^let calculus to lambda^S
calculus, which reveales that Leroy's typedicrected
boxing and unboxing corresponds to the type isomorphism
definable in lambda^S between types with substitution and
the corresponding simple types.