[1]

Minsik Cho, Tung D. Le, Ulrich A. Finkler, Haruiki Imai, Yasushi Negishi, Taro
Sekiyama, Saritha Vinod, Vladimir Zolotov, Kiyokuni Kawachiya, David S. Kung,
and Hillery C. Hunter.
Large model support for deep learning in Caffe and Chainer.
In the 1st SysML Conference, 2018.
Poster presentation.
[ .pdf ]

[2]

Tung D. Le, Taro Sekiyama, Yasushi Negishi, Haruki Imai, and Kiyokuni
Kawachiya.
Involving CPUs into multiGPU deep learning.
In Proceedings of the 9th International Conference on
Performance Engineering, pages 56–67, 2018.
[ DOI 
http ]

[3]

Masaharu Sakamoto, Hiroki Nakano, Kun Zhao, and Taro Sekiyama.
Lung nodule classification by the combination of fusion classifier
and cascaded convolutional neural networks.
ArXiv eprints, December 2017.
[ arXiv ]
Abstract
Lung nodule classification is a class imbalanced problem, as
nodules are found with much lower frequency than
nonnodules. In the class imbalanced problem, conventional
classifiers tend to be overwhelmed by the majority class
and ignore the minority class. We showed that cascaded
convolutional neural networks can classify the nodule
candidates precisely for a class imbalanced nodule
candidate data set in our previous study. In this paper,
we propose Fusion classifier in conjunction with the
cascaded convolutional neural network models. To fuse the
models, nodule probabilities are calculated by using the
convolutional neural network models at first. Then, Fusion
classifier is trained and tested by the nodule
probabilities. The proposed achieved the sensitivity of
94.4% and 95.9% at 4 and 8 false positives per scan in
Free Receiver Operating Characteristics (FROC) curve
analysis, respectively.

[4]

Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi.
On polymorphic gradual typing.
Proceedings of the ACM on Programming Languages,
1(ICFP):40:1–40:29, August 2017.
[ DOI ]
Abstract
We study an extension of typing graduala method to integrate
dynamic typing and static typing smoothly in a language
singleto parametric polymorphism and its theoretical
properties, including conservativity of typing and semantics
over both statically and dynamically typed languages, type
safety, blamesubtyping theorem, and the guarantee gradualthe
socalled refined criteria, advocated by Siek et al. We
develop System FG, which is a gradually typed extension of
System F with the dynamic type and a new type consistency
relation, and translation to a new polymorphic blame calculus
System FC, which is based on previous polymorphic blame
calculi by Ahmed et al. The design of System FG and System FC,
geared to the criteria, is influenced by the distinction
between static and gradual type variables, first observed by
Garcia and Cimini. This distinction is also useful to execute
statically typed code without incurring additional overhead to
manage type names as in the prior calculi. We prove that
System FG satisfies most of the criteria: all but the hardest
property of the gradual guarantee on semantics. We show that a
key conjecture to prove the gradual guarantee leads to the
JackofAllTrades property, conjectured as an important
property of the polymorphic blame calculus by Ahmed et al.

[5]

Taro Sekiyama, Akifumi Imanishi, and Kohei Suenaga.
Towards proof synthesis guided by neural machine translation for
intuitionistic propositional logic.
ArXiv eprints, June 2017.
[ arXiv ]
Abstract
Inspired by the recent evolution of deep neural networks
(DNNs) in machine learning, we explore their application to
PLrelated topics. This paper is the first step towards this
goal; we propose a proofsynthesis method for the
negationfree propositional logic in which we use a DNN to
obtain a guide of proof search. The idea is to view the
proofsynthesis problem as a translation from a proposition to
its proof. We train seq2seq, which is a popular network in
neural machine translation, so that it generates a proof
encoded as a Lung nodule classification is a class imbalanced
problem @Commentterm of a given proposition. We implement the
whole framework and empirically observe that a generated proof
term is close to a correct proof in terms of the tree edit
distance of AST. This observation justifies using the output
from a trained seq2seq model as a guide for proof search.

[6]

Taro Sekiyama, Atsushi Igarashi, and Michael Greenberg.
Polymorphic manifest contracts, revised and resolved.
ACM Transactions on Programming Languages and Systems,
39(1):3:1–3:36, February 2017.
[ DOI 
AuthorIzer ]
Abstract
Manifest contracts track precise program properties by refining
types with predicates—e.g., x:Intx > 0 denotes the
positive integers. Contracts and polymorphism make a natural
combination: programmers can give strong contracts to abstract
types, precisely stating pre and postconditions while hiding
implementation details—for example, an abstract type of
stacks might specify that the pop operation has input type
x:A Stacknot (empty x).
This article studies a polymorphic
calculus with manifest contracts and establishes fundamental
properties including type soundness and relational
parametricity. Indeed, this is not the first work on
polymorphic manifest contracts but existing calculi are not
very satisfactory. Gronski et al. developed the
Sage language, which introduces polymorphism through
the Type:Type discipline, but they do not study parametricity.
Some authors of this paper have produced two separate works:
Belo, Greenberg, Igarashi, and Pierce (ESOP 2011) and
Greenberg (PhD thesis) studied polymorphic manifest contracts
and parametricity, but their calculi have metatheoretical
problems in the type conversion relations—indeed, they
depend on a few conjectures, which turn out to be false. Our
calculus is the first polymorphic manifest calculus with
parametricity, depending on no conjectures—it resolves the
issues in prior calculi with delayed substitution on casts.

[7]

Taro Sekiyama and Atsushi Igarashi.
Stateful manifest contracts.
In Proceedings of the 44th Annual ACM SIGPLANSIGACT
Symposium on Principles of Programming Languages, POPL, pages 530–544, New
York, NY, USA, 2017. ACM.
[ DOI 
AuthorIzer 
material 
slide ]
Abstract
This paper studies hybrid contract verification for an
imperative higherorder language based on a socalled
manifest contract system. In manifest contract
systems, contracts are part of static types and contract
verification is hybrid in the sense that some contracts are
statically verified, typically by subtyping, but others are
dynamically by casts. It is, however, not trivial to extend
existing manifest contract systems, which have been designed
mostly for pure functional languages, to imperative features,
mainly because of the lack of flowsensitivity, which should
be taken into account in verifying imperative programs
statically.
We develop an imperative higherorder manifest
contract system λ^{}H_{ref} for
flowsensitive hybrid contract verification. We introduce a
computational variant of Nanevski et al's Hoare types,
which are flowsensitive types to represent pre and
postconditions of impure computation. Our Hoare types are
computational in the sense that pre and postconditions are
given by Booleans in the same language as programs so that
they are dynamically verifiable.
λ^{}H_{ref} also supports refinement
types as in existing manifest contract systems to describe
flowinsensitive, stateindependent contracts of pure
computation. While it is desirable that any—possibly
statemanipulating—predicate can be used in contracts, abuse
of stateful operations will break the system. To control
stateful operations in contracts, we introduce a regionbased
effect system, which allows contracts in refinement types and
computational Hoare types to manipulate states, as long as
they are observationally pure and readonly,
respectively. We show that dynamic contract checking in our
calculus is consistent with static typing in the sense that
the final result obtained without dynamic contract violations
satisfies contracts in its static type. It in particular
means that the state after stateful computations satisfies
their postconditions.
As in some of prior manifest contract
systems, static contract verification in this work is “post
facto,” that is, we first define our manifest contract system
so that all contracts are checked at run time, formalize
conditions when dynamic checks can be removed safely, and show
that programs with and without such removable checks are
contextually equivalent. We also apply the idea of post facto
verification to regionbased local reasoning, inspired
by the frame rule of Separation Logic.

[8]

Takayuki Osogami, Hiroshi Kajino, and Taro Sekiyama.
Bidirectional learning for timeseries models with hidden units.
In Proceedings of the 34th International Conference on Machine
Learning, pages 2711–2720, 2017.
[ .html 
.pdf ]
Abstract
Hidden units can play essential roles in modeling timeseries
having longterm dependency or onlinearity but make it
difficult to learn associated parameters. Here we propose a
way to learn such a timeseries model by training a backward
model for the timereversed timeseries, where the backward
model has a common set of parameters as the original (forward)
model. Our key observation is that only a subset of the
parameters is hard to learn, and that subset is complementary
between the forward model and the backward model. By training
both of the two models, we can effectively learn the values of
the parameters that are hard to learn if only either of the
two models is trained. We apply bidirectional learning to a
dynamic Boltzmann machine extended with hidden
units. Numerical experiments with synthetic and real datasets
clearly demonstrate advantages of bidirectional learning.

[9]

Masaharu Sakamoto, Hiroki Nakano, Kun Zhao, and Taro Sekiyama.
Multistage neural networks with singlesided classifiers for false
positive reduction and its evaluation using lung xray CT images.
In Proceedings of the 19th International Conference on Image
Analysis and Processing, pages 370–379, 2017.
[ DOI ]
Abstract
Lung nodule classification is a class imbalanced problem because
nodules are found in much lower frequency than nonnodules. In
the class imbalanced problem, conventional classifiers tend to
be overwhelmed by the majority class and ignore the minority
class. We therefore propose cascaded convolutional neural
networks to cope with the class imbalanced problem. In the
proposed approach, multistage convolutional neural networks
perform as singlesided classifiers to filter out obvious
nonnodules. Successively, a convolutional neural network
trained with a balanced data set calculates nodule
probabilities. The proposed method achieved the sensitivity of
92.4% and 94.5% at 4 and 8 false positives per scan in Free
Receiver Operating Characteristics (FROC) curve analysis,
respectively.

[10]

Taro Sekiyama.
An Integrated Theory of TypeBased Static and Dynamic
Verification.
PhD thesis, Kyoto University, 2016.
[ full 
slide ]
Abstract
For development of reliable software, many verification methods
have been studied so far. One of the most successful
approaches is type systems, which have been tied to various
kinds of programming languages from dynamically typed ones
through dependently typed ones. Each of dynamic, static, and
dependent typing has its own pros and cons and is not always
sufficient for development of practical, reliable software.
Our goal is to introduce a fullfledged programming language
where dynamically, statically, and dependently typed code
coexist and interact safely. In this thesis, we focus on
three universal features in programming: delimited control,
parametric polymorphism, and algebraic datatypes. These
features are bases of current programming
languages—delimited control provides control effects such as
exception handling; polymorphism plays a key role in
typebased abstraction and reuse of program components;
algebraic datatypes are an usual tool to represent data
structures. We study how these features are incorporated with
mechanisms for integrating a certified and an uncertified
worlds, based on gradual typing, which combines static and
dynamic typing, and manifest contracts, which does static and
dependent typing. We first study delimited control in
integration of static and dynamic typing; this extension needs
monitoring of capture and call of delimited continuations. We
also investigate parametric polymorphism in a combination of
static and dependent typing and show our extension is sound,
in particular, parametricity does hold. Finally, an extension
with algebraic datatypes lets us compare two major approaches
to giving specifications to data structures from the point of
view of computational efficiency. We believe that these
extensions and insights obtained from them will contribute to
achievement of our goal.

[11]

Yusuke Miyazaki, Taro Sekiyama, and Atsushi Igarashi.
Gradual typing for delimited continuations.
In the 5th Script To Program Evolution Workshop, 2016.
[ full ]

[12]

Taro Sekiyama, Yuki Nishida, and Atsushi Igarashi.
Manifest contracts for datatypes.
In Proceedings of the 42nd Annual ACM SIGPLANSIGACT
Symposium on Principles of Programming Languages, POPL, pages 195–207. ACM,
2015.
[ DOI 
AuthorIzer 
detail 
slide ]
Abstract
We study algebraic datatypes in a manifest contract system, a
software contract system where contract information occurs as
refinement types. We first compare two simple approaches:
refinements on type constructors and refinements on data
constructors. For example, lists of positive integers can be
described by { l:int list  for_all (λy. y > 0) l }
in the former, whereas by a userdefined datatype pos_list
with cons of type {x:int  x > 0} ×pos_list
→pos_list in the latter. The two approaches are
complementary: the former makes it easier for a programmer to
write types and the latter enables more efficient contract
checking. To take the best of both worlds, we propose (1) a
syntactic translation from refinements on type constructors to
equivalent refinements on data constructors and (2)
dynamically checked casts between different but compatible
datatypes such as int list and pos_list. We define a manifest
contract calculus to formalize the semantics of the casts and
prove that the translation is correct.

[13]

Taro Sekiyama, Soichiro Ueda, and Atsushi Igarashi.
Shifting the blame  A blame calculus with delimited control.
In Programming Languages and Systems  13th Asian Symposium,
APLAS, pages 189–207. Springer, 2015.
[ DOI 
full 
slide ]
Abstract
We study integration of static and dynamic typing in the presence
of delimitedcontrol operators. In a program where typed and
untyped parts coexist, the runtime system has to monitor the
flow of values between these parts and abort program execution
if invalid values are passed. However, control operators,
which enable us to implement useful control effects, make such
monitoring tricky; in fact, it is known that, with a standard
approach, certain communications between typed and untyped
parts can be overlooked.
We propose a new castbased mechanism to monitor all
communications between typed and untyped parts for a language
with control operators shift and reset. We extend a blame
calculus with shift/reset to give its semantics (operational
semantics and CPS transformation) and prove two important
correctness properties of the proposed mechanism: Blame
Theorem and soundness of the CPS transformation.

[14]

Taro Sekiyama and Atsushi Igarashi.
Logical relations for a manifest calculus, fixed.
In the 1st ACM SIGPLAN Workshop on HigherOrder Programming with
Effects, HOPE, 2012.
[ slide ]
Abstract
A manifest contract calculus is a lambdacalculus with software
contracts and dynamic contract checking, where software
contracts are part of type information and dynamic contract
checking is performed by casts from one type to another.
Previous work for manifest contract calculi has studied an
optimization to eliminate upcasts, and the correctness of the
optimization by giving logical relations. However, all proofs
of soundness of the logical relations w.r.t. contextual
equivalence are incomplete.
We fix this unfortunate situation and even go further: we extend
a polymorphic manifest contract calculus with a fixedpoint
operator, give logical relations for the extended calculus,
and show their soundness with respect to what we call
semityped contextual equivalence and that an upcast is
logically related to an identity function.
