publications | Taro Sekiyama

The list of publications including Japanese papers and talks. They are also found in:

2024

JFP

Signature restriction for polymorphic algebraic effects

Taro Sekiyama, Takeshi Tsukada, and Atsushi Igarashi

Journal of Functional Programming (JFP), vol. 34 , 2024

This article extends the paper published at ICFP’20 with the same title.

Abs DOI Code

The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. In the literature, there are two kinds of approaches to this problem: one is to restrict how effects are triggered and the other is to restrict how they are implemented. This work explores a new approach to ensuring the safety of the use of polymorphic effects in polymorphic type assignment. A novelty of our work is to restrict effect interfaces. To formalize our idea, we employ algebraic effects and handlers, where an effect interface is given by a set of operations coupled with type signatures. We propose signature restriction, a new notion to restrict the type signatures of operations and show that signature restriction ensures type safety of a language equipped with polymorphic effects and unrestricted polymorphic type assignment. We also develop a type-and-effect system to enable the use of both of the operations that satisfy and those that do not satisfy the signature restriction in a single program.
POPL

Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers

Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, and Tachio Terauchi

Proceedings of the ACM on Programming Languages (PACML), vol. 8 (POPL) , 2024

Abs DOI PDF Supp Code Slides

Algebraic effects and handlers are a mechanism to structure programs with computational effects in a modular way. They are recently gaining popularity and being adopted in practical languages, such as OCaml. Meanwhile, there has been substantial progress in program verification via refinement type systems. While a variety of refinement type systems have been proposed, thus far there has not been a satisfactory refinement type system for algebraic effects and handlers. In this paper, we fill the void by proposing a novel refinement type system for languages with algebraic effects and handlers. The expressivity and usefulness of algebraic effects and handlers come from their ability to manipulate delimited continuations, but delimited continuations also complicate programs’ control flow and make their verification harder. To address the complexity, we introduce a novel concept that we call answer refinement modification (ARM for short), which allows the refinement type system to precisely track what effects occur and in what order when a program is executed, and reflect such information as modifications to the refinements in the types of delimited continuations. We formalize our type system that supports ARM (as well as answer type modification, or ATM) and prove its soundness. Additionally, as a proof of concept, we have extended the refinement type system to a subset of OCaml 5 which comes with a built-in support for effect handlers, implemented a type checking and inference algorithm for the extension, and evaluated it on a number of benchmark programs that use algebraic effects and handlers. The evaluation demonstrates that ARM is conceptually simple and practically useful. Finally, a natural alternative to directly reasoning about a program with delimited continuations is to apply a continuation passing style (CPS) transformation that transforms the program to a pure program without delimited continuations. We investigate this alternative in the paper, and show that the approach is indeed possible by proposing a novel CPS transformation for algebraic effects and handlers that enjoys bidirectional (refinement-)type-preservation. We show that there are pros and cons with this approach, namely, while one can use an existing refinement type checking and inference algorithm that can only (directly) handle pure programs, there are issues such as needing type annotations in source programs and making the inferred types less informative to a user.
PLDI

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric

Atsushi Igarashi, Shota Ozaki, Taro Sekiyama, and Yudai Tanabe

Proceedings of the ACM on Programming Languages (PACML), vol. 8 (PLDI) , 2024

Abs DOI PDF Supp Video Slides

Since the arrival of gradual typing, which allows partially typed code in a single program, efficient implementations of gradual typing have been an active research topic. In this paper, we study the space-efficiency problem of gradual typing in the presence of parametric polymorphism. Based on the existing work that showed the impossibility of a space-efficient implementation that supports fully parametric polymorphism, this paper will show that a space-efficient implementation is, in principle, possible by slightly relaxing parametricity. We first develop λCmp, which is a coercion calculus with mostly parametric polymorphism, and show its relaxed parametricity. Then, we present λSmp, a space-efficient version of λCmp, and prove that λSmp programs can be executed in a space-efficient manner and that translation from λCmp to λSmp is type- and semantics-preserving.
ICFP

Abstracting Effect Systems for Algebraic Effect Handlers

Takuma Yoshioka, Taro Sekiyama, and Atsushi Igarashi

Proceedings of the ACM on Programming Languages (PACML), vol. 8 (ICFP) , 2024

Abs DOI arXiv Supp Slides

Many effect systems for algebraic effect handlers are designed to guarantee that all invoked effects are handled adequately. However, respective researchers have developed their own effect systems that differ in how to represent the collections of effects that may happen. This situation results in blurring what is required for the representation and manipulation of effect collections in a safe effect system. In this work, we present a language λEA equipped with an effect system that abstracts the existing effect systems for algebraic effect handlers. The effect system of λEA is parameterized over effect algebras, which abstract the representation and manipulation of effect collections in safe effect systems. We prove the type-and-effect safety of λEA by assuming that a given effect algebra meets certain properties called safety conditions. As a result, we can obtain the safety properties of a concrete effect system by proving that an effect algebra corresponding to the concrete system meets the safety conditions. We also show that effect algebras meeting the safety conditions are expressive enough to accommodate some existing effect systems, each of which represents effect collections in a different style. Our framework can also differentiate the safety aspects of the effect collections of the existing effect systems. To this end, we extend λEA and the safety conditions to lift coercions and type-erasure semantics, propose other effect algebras including ones for which no effect system has been studied in the literature, and compare which effect algebra is safe and which is not for the extensions.
OOPSLA

Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification

Taro Sekiyama, and Hiroshi Unno

Proceedings of the ACM on Programming Languages (PACML), vol. 8 (OOPSLA2) , 2024

Abs DOI Supp Code Slides

Model checking is one of the successful program verification methodologies. Since the seminal work by Ong, the model checking of higher-order programs―called higher-order model checking, or HOMC for short―has gained attention. It is also crucial for making HOMC applicable to real-world software to address programs involving computational effects. Recently, Dal Lago and Ghyselen considered an extension of HOMC to algebraic effect handlers, which enable programming the semantics of effects. They showed a negative result for HOMC with algebraic effect handlers―it is undecidable. In this work, we explore a restriction on programs with algebraic effect handlers which ensures the decidability of HOMC while allowing implementations of various effects. We identify the crux of the undecidability as the use of an unbounded number of algebraic effect handlers being active at the same time. To prevent it, we introduce answer-type modification (ATM), which can bound the number of algebraic effect handlers that can be active at the same time. We prove that ATM can ensure the decidability of HOMC and show that it accommodates a wide range of effects. To evaluate our approach, we implemented an automated verifier EffCaml based on the presented techniques and confirmed that the program examples discussed in this paper can be automatically verified.
COMPSAC

Formal Support for Threat Modeling with Attack Decision Diagrams

Misato Nakabayashi, Taro Sekiyama, Ichiro Hasuo, and Yutaka Ishikawa

In Proceedings of the 48th IEEE Annual Computers, Software, and Applications Conference (COMPSAC), 2024

Abs DOI Slides

System threat analysis requires a wide range of knowledge and is time-consuming. In this study, we propose FSTM system, a method to visualize threats in the system to support threat modeling using a formal verification tool. Concretely, given a security requirement and a system model, we represent what kind of attacks are enabled to prevent the system from satisfying the security requirement using an AND-OR tree based on exhaustive formal verification. To generate an exhaustive AND-OR tree, a large number of system models modified to enable various attack patterns and verification costs are required because verification results must be obtained for all threat patterns. We used the property that we call monotonicity of security to reduce the number of verifications and automatically generate a verification model for each threat pattern from a single verification model. We implemented FSTM system using Tamarin Prover, a formal verification tool, and evaluated it with case studies.
ISNCC

Rabbit: A Language to Model and Verify Data Flow in Networked Systems

Terunobu Inaba, Yutaka Ishikawa, Atsushi Igarashi, and Taro Sekiyama

In Proceedings of the 2024 International Symposium on Networks, Computers and Communications (ISNCC), 2024

Abs DOI Slides

Threat modeling is an effective approach to fortifying security, where system designers model a target system and investigate potential security weaknesses during the design phase. To investigate security flaws in the system rigorously, the model has to be detailed to the extent that the flow of each asset is minutely tracked. For this purpose, we propose Rabbit, a language to model a networked system with the ability to describe data flows within the system. Rabbit also aims to formally verify security properties under the specified system model and attacker model. In this paper, we model a simple client-server system and demonstrate the possibility of automatic verification using Rabbit. In an experiment we conducted, we have found a non-trivial execution path that violates a desired security property, demonstrating the potential of automatic security verification using Rabbit.

2023

POPL

Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations

Taro Sekiyama, and Hiroshi Unno

Proceedings of the ACM on Programming Languages (PACML), vol. 7 (POPL) , 2023

Abs DOI arXiv PDF Supp Video Code

Type-and-effect systems are a widely used approach to program verification, verifying the result of a computation using types, and its behavior using effects. This paper extends an effect system for verifying temporal, value-dependent properties on event sequences yielded by programs, to the delimited control operators shift0/reset0. While these delimited control operators enable useful and powerful programming techniques, they hinder reasoning about the behavior of programs because of their ability to suspend, resume, discard, and duplicate delimited continuations. This problem is more serious in effect systems for temporal properties because these systems must be capable of identifying what event sequences are yielded by captured continuations. Our key observation for achieving effective reasoning in the presence of the delimited control operators is that their use modifies answer effects, which are temporal effects of the continuations. Based on this observation, we extend an effect system for temporal verification to accommodate answer-effect modification. Allowing answer-effect modification enables easily reasoning about traces that captured continuations yield. Another novel feature of our effect system is the support for dependently typed continuations, which allows us to reason about programs more precisely. We prove soundness of the effect system for finite event sequences via type safety and that for infinite event sequences using a logical relation.
HASP

Automated Security Analysis for Real-World IoT Devices

Lélio Brun, Ichiro Hasuo, Yasushi Ono, and Taro Sekiyama

In Proceedings of the 12th International Workshop on Hardware and Architectural Support for Security and Privacy (HASP), 2023

Abs DOI PDF Slides

Automatic security protocol analysis is a fruitful research topic that demonstrates the application of formal methods to security analysis. Several endeavors in the last decades successfully verified security properties of large-scale network protocols like TLS, sometimes unveiling unknown vulnerabilities. In this work, we show how to apply these techniques to the domain of IoT, where security is a critical aspect. While most existing security analyses for IoT tackle individually either protocols, firmware or applications, our goal is to treat IoT systems as a whole. We focus our work on a case study, the Armadillo-IoT G4 device, highlighting the specific challenges we must tackle to analyze the security of a typical IoT device. We propose a model using the Tamarin prover, that allows us to state certain key security properties about the device and to prove them automatically.

2022

Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning

Minchao Wu, Takeshi Tsukada, Hiroshi Unno, Taro Sekiyama, and Kohei Suenaga

ArXiv e-prints, vol. abs/2107.09766 , 2022

Abs arXiv

Loop-invariant synthesis is the basis of program verification. Due to the undecidability of the problem in general, a tool for invariant synthesis necessarily uses heuristics. Despite the common belief that the design of heuristics is vital for the performance of a synthesizer, heuristics are often engineered by their developers based on experience and intuition, sometimes in an ad-hoc manner. In this work, we propose an approach to systematically learning heuristics for template-based CounterExample-Guided Inductive Synthesis (CEGIS) with reinforcement learning. As a concrete example, we implement the approach on top of PCSat, which is an invariant synthesizer based on template-based CEGIS. Experiments show that PCSat guided by the heuristics learned by our framework not only outperforms existing state-of-the-art CEGIS-based solvers such as HoICE and the neural solver Code2Inv, but also has slight advantages over non-CEGIS-based solvers such as Eldarica and Spacer in linear Constrained Horn Clause (CHC) solving.
HOPE

Dependent Temporal Type-and-Effect System with Delimited Continuations

Taro Sekiyama, and Hiroshi Unno

In The 10th ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE), Ljubljana, Slovenia, 2022

Abs arXiv

Type-and-effect systems are a widely-used approach to program verification, verifying the result of a computation using types, and the behavior using effects. This paper extends an effect system for verifying temporal, value-dependent properties on event sequences yielded by programs to the delimited control operators shift0/reset0. While these delimited control operators enable useful and powerful programming techniques, they hinder reasoning about the behavior of programs because of their ability to suspend, resume, discard, and duplicate delimited continuations. This problem is more serious in effect systems for temporal properties because these systems must be capable of identifying how computations yielding event sequences are manipulated by the control operators. Our key observation for achieving effective reasoning in the presence of the delimited control operators is that the use of them modifies not only answer types but also the temporal effects of contexts. This observation enables the integration of an effect system for temporal verification with a type system that accommodates answer-type modification. Another novel feature of our effect system is the support for dependently-typed continuations, which allows us to reason about programs more precisely. We prove soundness of the effect system for finite event sequences via type safety and that for infinite event sequences using a logical relation.

2021

ICFP

CPS transformation with affine types for call-by-value implicit polymorphism

Taro Sekiyama, and Takeshi Tsukada

Proceedings of the ACM on Programming Languages (PACML), vol. 5 (ICFP) , 2021

Abs DOI PDF Supp Video Slides

Transformation of programs into continuation-passing style (CPS) reveals the notion of continuations, enabling many applications such as control operators and intermediate representations in compilers. Although type preservation makes CPS transformation more beneficial, achieving type-preserving CPS transformation for implicit polymorphism with call-by-value (CBV) semantics is known to be challenging. We identify the difficulty in the problem that we call scope intrusion. To address this problem, we propose a new CPS target language Λopen that supports two additional constructs for polymorphism: one only binds and the other only generalizes type variables. Unfortunately, their unrestricted use makes Λopen unsafe due to undesired generalization of type variables. We thus equip Λopen with affine types to allow only the type-safe generalization. We then define a CPS transformation from Curry-style CBV System F to type-safe Λopen and prove that the transformation is meaning and type preserving. We also study parametricity of Λopen as it is a fundamental property of polymorphic languages and plays a key role in applications of CPS transformation. To establish parametricity, we construct a parametric, step-indexed Kripke logical relation for Λopen and prove that it satisfies the Fundamental Property as well as soundness with respect to contextual equivalence.
SAS

Toward Neural-Network-Guided Program Synthesis and Verification

Naoki Kobayashi, Taro Sekiyama, Issei Sato, and Hiroshi Unno

In Proceedings of the 28th Static Analysis Symposium (SAS), 2021

Abs DOI arXiv PDF Video Code

We propose a novel framework of program and invariant synthesis called neural network-guided synthesis. We first show that, by suitably designing and training neural networks, we can extract logical formulas over integers from the weights and biases of the trained neural networks. Based on the idea, we have implemented a tool to synthesize formulas from positive/negative examples and implication constraints, and obtained promising experimental results. We also discuss an application of our method for improving the qualifier discovery in the framework of ICE-learning-based CHC solving, which can in turn be applied to program verification and inductive invariant synthesis. Another potential application is to a neural-network-guided variation of Solar-Lezama’s program synthesis by sketching.
Scheme

Is Space-Efficient Polymorphic Gradual Typing Possible?

Shota Ozaki, Taro Sekiyama, and Atsushi Igarashi

In The 28th Scheme and Functional Programming Workshop, 2021

Abs PDF Video

Gradual typing, proposed by Siek and Taha, is a way to combine static and dynamic typing in a single programming language. Since its inception, researchers have studied techniques for efficient implementation. In this paper, we study the problem of space-efficient gradual typing in the presence of parametric polymorphism. We develop a polymorphic extension of the coercion calculus, an intermediate language for gradual typing. Then, we show that it cannot be made space-efficient by following the previous approaches, due to subtle interaction with dynamic sealing, a standard technique to ensure parametricity in polymorphic gradual typing.
CPS Transformation with Affine Types for Implicit Polymorphism

Taro Sekiyama

2021

Dagstuhl Seminar 21292: Scalable Handling of Effects

2020

WGT

Gradual Typing for Extensibility by Rows

Taro Sekiyama, and Atsushi Igarashi

In The 1st ACM SIGPLAN Workshop on Gradual Typing (WGT), 2020

Abs arXiv PDF Supp

This work studies gradual typing for row types and row polymorphism. Key ingredients in this work are the dynamic row typ e, which represents a statically unknown part of a row, and consistency for row typ es, which allows injecting static row types into the dynamic row type and, conversely, projecting the dynamic row type to any static row type. While consistency captures the behavior of the dynamic row type statically, it makes the semantics of a gradually typed language incoherent when combined with row equivalence which identifies row types up to field reordering. To solve this problem, we develop consistent equivalence, which characterizes composition of consistency and row equivalence. Using consistent equivalence, we propose a polymorphic blame calculus FρC for row types and row polymorphism. In FρC, casts perform not only run-time checking with the dynamic row type but also field reordering in row types. To simplify our technical development for row polymorphism, we adopt scop ed labels, which are employed by the language Koka and are also emerging in the context of effect systems. We give the formal definition of FρC with these technical developments and prove its type soundness. We also sketch the gradually typed surface language FρG and type-preserving translation from FρG to FρC and discuss conservativity of FρG over typing of a statically typed language with row types and row polymorphism.
ICFP

Signature restriction for polymorphic algebraic effects

Taro Sekiyama, Takeshi Tsukada, and Atsushi Igarashi

Proceedings of the ACM on Programming Languages (PACML), vol. 4 (ICFP) , 2020

Abs DOI arXiv PDF Supp Video Code Slides

The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. Existing approaches to this problem are classified into two groups: one for restricting how effects are triggered and the other for restricting how they are implemented. This work explores a new approach to ensuring the safety of polymorphic effects in polymorphic type assignment. A novelty of our work lies in finding a restriction on effect interfaces. To formalize our idea, we employ algebraic effects and handlers, where an effect interface is given by a set of operations coupled with type signatures. We propose signature restriction, a new notion to restrict the type signatures of operations, and show that signature restriction is sufficient to ensure type safety of an effectful language equipped with unrestricted polymorphic type assignment. We also develop a type-and-effect system to enable the use of both operations that satisfy and do not satisfy the signature restriction in a single program.
AAAI

Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces

Takamasa Okudono, Masaki Waga, Taro Sekiyama, and Ichiro Hasuo

In Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI), 2020

Abs DOI arXiv Slides

We present a method to extract a weighted finite automa ton (WFA) from a recurrent neural network (RNN). Our method is based on the WFA learning algorithm by Balle and Mohri, which is in turn an extension of Angluin’s classic L∗algorithm. Our technical novelty is in the use of regression methods for the so-called equivalence queries, thus exploiting the internal state space of an RNN to prioritize counterexam ple candidates. This way we achieve a quantitative/weighted extension of the recent work by Weiss, Goldberg and Yahav that extracts DFAs. We experimentally evaluate the accuracy, expressivity and efficiency of the extracted WFAs.

2019

POPL

Dynamic type inference for gradual Hindley–Milner typing

Yusuke Miyazaki, Taro Sekiyama, and Atsushi Igarashi

Proceedings of the ACM on Programming Languages (PACML), vol. 3 (POPL) , 2019

Abs DOI arXiv PDF Video Code

Garcia and Cimini study a type inference problem for the ITGL, an implicitly and gradually typed language with let-polymorphism, and develop a sound and complete inference algorithm for it. Soundness and completeness mean that, if the algorithm succeeds, the input term can be translated to a well-typed term of an explicitly typed blame calculus by cast insertion and vice versa. However, in general, there are many possible translations depending on how type variables that were left undecided by static type inference are instantiated with concrete static types. Worse, the translated terms may behave differently—some evaluate to values but others raise blame. In this paper, we propose and formalize a new blame calculus λBDTI that avoids such divergence as an intermediate language for the ITGL. A main idea is to allow a term to contain type variables (that have not been instantiated during static type inference) and defer instantiation of these type variables to run time. We introduce dynamic type inference (DTI) into the semantics of λBDTI so that type variables are instantiated along reduction. The DTI-based semantics not only avoids the divergence described above but also is sound and complete with respect to the semantics of fully instantiated terms in the following sense: if the evaluation of a term succeeds (i.e., terminates with a value) in the DTI-based semantics, then there is a fully instantiated version of the term that also succeeds in the explicitly typed blame calculus and vice versa. Finally, we prove the gradual guarantee, which is an important correctness criterion of a gradually typed language, for the ITGL.
ESOP

Handling Polymorphic Algebraic Effects

Taro Sekiyama, and Atsushi Igarashi

In Proceedings of the 28th European Symposium on Programming (ESOP), 2019

Abs DOI arXiv PDF Supp

Algebraic effects and handlers are a powerful abstraction mechanism to represent and implement control effects. In this work, we study their extension with parametric polymorphism that allows abstracting not only expressions but also effects and handlers. Although polymorphism makes it possible to reuse and reason about effect implementations more effectively, it has long been known that a naive combination of polymorphic effects and let-polymorphism breaks type safety. Although type safety can often be gained by restricting let-bound expressions—e.g., by adopting value restriction or weak polymorphism—we propose a complementary approach that restricts handlers instead of let-bound expressions. Our key observation is that, informally speaking, a handler is safe if resumptions from the handler do not interfere with each other. To formalize our idea, we define a call-by-value lambda calculus that supports let-polymorphism and polymorphic algebraic effects and handlers, design a type system that rejects interfering handlers, and prove type safety of our calculus.
Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks

Taro Sekiyama, and Kohei Suenaga

In 第21回プログラミングおよびプログラミング言語ワークショップ (PPL), 岩手, 花巻, 2019

既発表論文紹介
Dynamic type inference for gradual Hindley–Milner typing

Yusuke Miyazaki, Taro Sekiyama, and Atsushi Igarashi

In 第21回プログラミングおよびプログラミング言語ワークショップ (PPL), 岩手, 花巻, 2019

既発表論文紹介
Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks

Taro Sekiyama, and Kohei Suenaga

In The 21th JSSST Workshop on Programming and Programming Languages (PPL), 2019

既発表論文紹介
Dynamic type inference for gradual Hindley–Milner typing

Yusuke Miyazaki, Taro Sekiyama, and Atsushi Igarashi

In The 21th JSSST Workshop on Programming and Programming Languages (PPL), 2019

既発表論文紹介
Integration of Type-Based Static and Dynamic Verification

Taro Sekiyama

2019

PKU-UTokyo-NII Joint Forum
Weighted Automata Extraction from Recurrent Neural Networks via Regression

太朗関山

2019

第22回情報論的学習理論ワークショップ (企画セッション1：機械学習と離散数学)
Weighted Automata Extraction from Recurrent Neural Networks via Regression

Taro Sekiyama

2019

The 22th Information-Based Induction Sciences Workshop (IBIS), Session: Machine Learning and Discrete Mathematics

2018

SysML

Large Model Support for Deep Learning in Caffe and Chainer

Minsik Cho, Tung D. Le, Ulrich A. Finkler, Haruki Imai, Yasushi Negishi, Taro Sekiyama, Saritha Vinod, Vladimir Zolotov, Kiyokuni Kawachiya, David S. Kung, and Hillery C. Hunter

In The 1st SysML Conference, 2018

Abs PDF

Deep learning is both compute- and data-intense, and recent breakthroughs have largely been fueled by the fp32 compute capacity of modern GPUs. This has made GPUs the prevalent tool for training deep neural networks, but GPUs have only small amounts of costly 3D-stacked HBM DRAM as their local memory. Working out of a small memory imposes a limit on the maximum learning capacity a neural network can have (i.e., the number of learnable parameters) and the maximum size and number of samples a network can consume at a given time. The field of deep learning is evolving in many new directions, and research teams are exploring both very large neural networks and attempting to apply deep learning to real datasets, including high-resolution images. Those exploring both the boundaries of neural networks and use of real datasets today generally will find that their deep learning software won’t support what they wish to train, and if it does, they find performace to be intolerably slow. In this paper, we present the idea of large model support, and its implementation in two popular deep learning frameworks, Caffe and Chainer. The key idea is to use GPU memory as an application-level cache w.r.t. the host memory so that a large network (e.g., many parameters or many layers) can be trained with real-world samples (e.g., HD-images). Although our large model support scheme may degrade the performance of training due to the communication overhead between the system CPUs and GPUs, the overhead in general is observed to reduce significantly with the use of a faster communication link between the CPU and GPU (NVLink and next-Gen NVLink). Our experimental results show that our large model support in Caffe and Chainer performs very well, and can train 2 to 6 times larger ImageNet models.
ICPE

Involving CPUs into Multi-GPU Deep Learning

Tung D. Le, Taro Sekiyama, Yasushi Negishi, Haruki Imai, and Kiyokuni Kawachiya

In Proceedings of the 9th International Conference on Performance Engineering (ICPE), 2018

Abs DOI PDF

The most important part of deep learning, training the neural network, often requires the processing of a large amount of data and can takes days to complete. Data parallelism is widely used for training deep neural networks on multiple GPUs in a single machine thanks to its simplicity. However, its scalability is bound by the number of data transfers, mainly for exchanging and accumulating gradients among the GPUs. In this paper, we present a novel approach to data parallel training called CPU-GPU data parallel (CGDP) training that utilizes free CPU time on the host to speed up the training in the GPUs. We also present a cost model for analyzing and comparing the performances of both the typical data parallel training and the CPU-GPU data parallel training. Using the cost model, we formally show why our approach is better than the typical one and clarify the remaining issues. Finally, we explain how we optimized CPU-GPU data parallel training by introducing chunks of layers and present a runtime algorithm that automatically finds a good configuration for the training. The algorithm is effective for very deep neural networks, which are the current trend in deep learning. Experimental results showed that we achieved speedups of 1.21, 1.04, 1.21 and 1.07 for four state-of-the-art neural networks: AlexNet, GoogLeNet-v1, VGGNet-16, and ResNet-152, respectively. Weak scaling efficiency greater than 90 was achieved for all networks across four GPUs.
ISBI

Lung nodule classification by the combination of fusion classifier and cascaded convolutional neural networks

Masaharu Sakamoto, Hiroki Nakano, Kun Zhao, and Taro Sekiyama

In 15th IEEE International Symposium on Biomedical Imaging (ISBI), 2018

Abs DOI arXiv

Lung nodule classification is a class imbalance problem, as nodules are found with much lower frequency than non-nodules. In the class imbalance 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 method 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.
APLAS

Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks

Taro Sekiyama, and Kohei Suenaga

In Proceedings of the 16th Asian Symposium on Programming Languages and Systems (APLAS), 2018

Abs DOI arXiv

This work explores the application of deep learning, a machine learning technique that uses deep neural networks (DNN) in its core, to an automated theorem proving (ATP) problem. To this end, we construct a statistical model which quantifies the likelihood that a proof is indeed a correct one of a given proposition. Based on this model, we give a proof-synthesis procedure that searches for a proof in the order of the likelihood. This procedure uses an estimator of the likelihood of an inference rule being applied at each step of a proof. As an implementation of the estimator, we propose a proposition-to-proof architecture, which is a DNN tailored to the automated proof synthesis problem. To empirically demonstrate its usefulness, we apply our model to synthesize proofs of the minimal propositional logic. We train the proposition-to-proof model using a training dataset of proposition–proof pairs. The evaluation against a benchmark set shows the very high accuracy and an improvement to the recent work of neural proof synthesis.
Profile-guided memory optimization for deep neural networks

Taro Sekiyama, Takashi Imamichi, Haruki Imai, and Rudy Raymond

ArXiv e-prints, vol. abs/1804.10001 , 2018

Abs arXiv

Recent years have seen deep neural networks (DNNs) becoming wider and deeper to achieve better performance in many applications of AI. Such DNNs however require huge amounts of memory to store weights and intermediate results (e.g., activations, feature maps, etc.) in propagation. This requirement makes it difficult to run the DNNs on devices with limited, hard-to-extend memory, degrades the running time performance, and restricts the design of network models. We address this challenge by developing a novel profile-guided memory optimization to efficiently and quickly allocate memory blocks during the propagation in DNNs. The optimization utilizes a simple and fast heuristic algorithm based on the two-dimensional rectangle packing problem. Experimenting with well-known neural network models, we confirm that our method not only reduces the memory consumption by up to 49.5% but also accelerates training and inference by up to a factor of four thanks to the rapidity of the memory allocation and the ability to use larger mini-batch sizes.
Reasoning about Polymorphic Manifest Contracts

Taro Sekiyama, and Atsushi Igarashi

ArXiv e-prints, vol. abs/1806.07041 , 2018

Abs arXiv

Manifest contract calculi, which integrate cast-based dynamic contract checking and refinement type systems, have been studied as foundations for hybrid contract checking. In this article, we study techniques to reasoning about a polymorphic manifest contract calculus, including a few program transformations related to static contract verification. We first define a polymorphic manifest contract calculus FH, which is much simpler than a previously studied one with delayed substitution, and a logical relation for it and prove that the logical relation is sound with respect to contextual equivalence. Next, we show that the upcast elimination property, which has been studied as correctness of subtyping-based static cast verification, holds for FH. More specifically, we give a subtyping relation (which is not part of the calculus) for FH types and prove that a term obtained by eliminating upcasts—casts from one type to a supertype of it—is logically related and so contextually equivalent to the original one. We also justify two other program transformations for casts: selfification and static cast decomposition, which help upcast elimination. A challenge is that, due to the subsumption-free approach to manifest contracts, these program transformations do not always preserve well-typedness of terms. To address it, the logical relation and contextual equivalence in this work are defined as semityped relations: only one side of the relations is required to be well typed and the other side may be ill typed.
プロファイルに基づくニューラルネットワークのためのメモリ最適化

太朗関山, 貴司今道, 晴基今井, and Rudy Raymond

In 第35回日本ソフトウェア科学大会, 2018

オンライン大会予稿集
Stateful Manifest Contracts

Taro Sekiyama, and Atsushi Igarashi

In "第17回" # "fitintro", 福岡, 福岡, 2018

既発表論文紹介
Towards Proof Synthesis Guided by Neural Machine Translation

Taro Sekiyama, Akifumi Imanishi, and Kohei Suenaga

, vol. , 2018
Memory Optimization Based on Profiles for Neural Networks

Taro Sekiyama, Takashi Imamichi, Haruki Imai, and Rudy Raymond

In Proceedings of the 35th JSSST Convention, 2018
Stateful Manifest Contracts

Taro Sekiyama, and Atsushi Igarashi

In The 17thForum on Information Technology (FIT), 福岡, 福岡, 2018

既発表論文紹介

2017

TOPLAS

Polymorphic Manifest Contracts, Revised and Resolved

Taro Sekiyama, Atsushi Igarashi, and Michael Greenberg

ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 39 (1) , 2017

Abs DOI PDF Supp

Manifest contracts track precise program properties by refining types with predicates—e.g., {x:Int|x > 0} denotes the positive integers. Contracts and polymorphism make a natural combination: programmers can give strong contracts to abstract types, precisely stating pre- and post-conditions while hiding implementation details—for example, an abstract type of stacks might specify that the pop operation has input type {x:A Stack|not (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.
POPL

Stateful Manifest Contracts

Taro Sekiyama, and Atsushi Igarashi

In Proceedings of the 44th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2017

Abs DOI PDF Supp Slides

This paper studies hybrid contract verification for an imperative higher-order language based on a so-called 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 flow-sensitivity, which should be taken into account in verifying imperative programs statically. We develop an imperative higher-order manifest contract system λ^H_ref for flow-sensitive hybrid contract verification. We introduce a computational variant of Nanevski et al’s Hoare types, which are flow-sensitive 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 flow-insensitive, state-independent contracts of pure computation. While it is desirable that any—possibly state-manipulating—predicate can be used in contracts, abuse of stateful operations will break the system. To control stateful operations in contracts, we introduce a region-based effect system, which allows contracts in refinement types and computational Hoare types to manipulate states, as long as they are observationally pure and read-only, 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 region-based local reasoning, inspired by the frame rule of Separation Logic.
ICFP

On Polymorphic Gradual Typing

Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi

Proceedings of the ACM on Programming Languages (PACML), vol. 1 (ICFP) , 2017

Abs DOI PDF Supp Video Code

We study an extension of gradual typing—a method to integrate dynamic typing and static typing smoothly in a single language—to parametric polymorphism and its theoretical properties, including conservativity of typing and semantics over both statically and dynamically typed languages, type safety, blame-subtyping theorem, and the gradual guarantee—the so-called 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 Jack-of-All-Trades property, conjectured as an important property of the polymorphic blame calculus by Ahmed et al.
ICML

Bidirectional learning for time-series models with hidden units

Takayuki Osogami, Hiroshi Kajino, and Taro Sekiyama

In Proceedings of the 34th International Conference on Machine Learning (ICML), 2017

Abs PDF Supp

Hidden units can play essential roles in modeling time-series having long-term dependency or on-linearity but make it difficult to learn associated parameters. Here we propose a way to learn such a time-series model by training a backward model for the time-reversed time-series, 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.
Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic

Taro Sekiyama, Akifumi Imanishi, and Kohei Suenaga

ArXiv e-prints, vol. abs/1706.06462 , 2017

Abs arXiv

Inspired by the recent evolution of deep neural networks (DNNs) in machine learning, we explore their application to PL-related topics. This paper is the first step towards this goal; we propose a proof-synthesis method for the negation-free propositional logic in which we use a DNN to obtain a guide of proof search. The idea is to view the proof-synthesis 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 λ-term 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.
ICIAP

Multi-stage Neural Networks with Single-Sided Classifiers for False Positive Reduction and Its Evaluation Using Lung X-Ray CT Images

Masaharu Sakamoto, Hiroki Nakano, Kun Zhao, and Taro Sekiyama

In Proceedings of the 19th International Conference on Image Analysis and Processing (ICIAP), 2017

Abs DOI arXiv

Lung nodule classification is a class imbalanced problem because nodules are found in much lower frequency than non-nodules. 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, multi-stage convolutional neural networks perform as single-sided classifiers to filter out obvious non-nodules. 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.
深層学習によるプログラム生成の高速化

諒文今西, 太朗関山, 崇行村主, and 幸平末永

In 第19回プログラミングおよびプログラミング言語ワークショップ (PPL), 山梨, 笛吹, 2017

ポスター
漸進的型付き多相ラムダ計算

雄五十嵐, 太朗関山, and 淳五十嵐

In 第19回プログラミングおよびプログラミング言語ワークショップ (PPL), 山梨, 笛吹, 2017

ポスター
ワークスペース自動割当による畳み込みニューラルネットワークの高速化

太朗関山, and 晴基今井

In 第34回日本ソフトウェア科学大会, 2017

オンライン大会予稿集

Abs PDF

畳み込みニューラルネットワーク(CNN)は中間データを保存するためのメモリ(ワークスペース)を割り当てることで高速化されることが知られている．本稿ではニューラルネットワーク(NN)を動的に構築・操作できる深層学習フレームワークにおけるワークスペース管理手法を提案， CNNを自動的に高速化する．NNの動的構築によりNNが最低限必要とするメモリ量を推定することが難しくなり，その結果ワークスペースに割けるメモリ量の推測が困難になる．我々はNNが必要とするメモリを空きメモリからだけではなくワークスペースからも割り当てることでワークスペース割当を自動化しつつNNの構築を妨げない範囲でCNNを高速化する．我々は提案手法をChainerに実装し，ワークスペースの自動割当によりVGGNetなどの主要なCNNにおける伝搬処理が最大1.60 倍高速化されたことを確認した．
大規模ニューラルネットワークモデルの Out-of-Core 学習の性能評価

晴基今井, 根岸康, 太朗関山, and 清久仁河内谷

In ハイパフォーマンスコンピューティング研究会, 2017
Stateful Manifest Contracts

Taro Sekiyama, and Atsushi Igarashi

In 第19回プログラミングおよびプログラミング言語ワークショップ (PPL), 山梨, 笛吹, 2017

既発表論文紹介
Acceleration of Program Synthesis by Deep Learning

Akifumi Imanishi, Taro Sekiyama, Takayuki Muranushi, and Kohei Suenaga

In The 19th JSSST Workshop on Programming and Programming Languages (PPL), 2017
A Gradually Typed Polymorhpic Lambda Calculus

Yu Igarashi, Taro Sekiyama, and Atsushi Igarashi

In The 19th JSSST Workshop on Programming and Programming Languages (PPL), 2017
Acceleration of Convolutional Neural Networks by Automated Workspace Allocation

Taro Sekiyama, and Haruki Imai

In Proceedings of the 34th JSSST Convention, 2017

PDF
Performance Evaluation of Out-of-Core Learning with Large Neural Network Models

Haruki Imai, Yasushi Negishi, Taro Sekiyama, and Kiyokuni Kawachiya

In Proceedings of the JSSST Workshop on High-Performance Computing, 2017
Stateful Manifest Contracts

Taro Sekiyama, and Atsushi Igarashi

In The 19th JSSST Workshop on Programming and Programming Languages (PPL), 2017

既発表論文紹介
Stateful Manifest Contracts

太朗関山

2017

第34回日本ソフトウェア科学大会トップカンファレンス特別講演

2016

PhD Thesis

An Integrated Theory of Type-Based Static and Dynamic Verification

Taro Sekiyama

Kyoto University, 2016

Abs PDF Slides

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 full-fledged 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 type-based 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.
STOP

Gradual Typing for Delimited Continuations

Yusuke Miyazaki, Taro Sekiyama, and Atsushi Igarashi

In The 5th Script To Program Evolution Workshop (STOP), 2016

Abs PDF

We report our ongoing work on gradual typing for a language with delimited-control operators, shift and reset, which are known to be very powerful constructs. We base our gradual type system on the simple type system with so-called answer-type modification proposed by Danvy and Filinski. We introduce the type dynamic (written *), define the type consistency relation, modify the typing rules by using the type consistency relation, and give translation to insert explicit casts. The way we modify the typing rules is very similar to the Gradualizer but it turns out that the Gradualizer is not directly applicable for generation of rules of cast insertion translation. We also discuss the properties of the obtained gradually typed language according to Siek et al.’s criteria for gradually typed languages.
限定継続演算子 shift/reset のための漸進的型付け

勇輔宮崎, 太朗関山, and 淳五十嵐

In 第18回プログラミングおよびプログラミング言語ワークショップ (PPL), 岡山, 玉野, 2016

ポスター
Gradual Typing for Delimited Control Operators shift/reset

Yusuke Miyazaki, Taro Sekiyama, and Atsushi Igarashi

In The 18th JSSST Workshop on Programming and Programming Languages (PPL), 2016

2015

POPL

Manifest Contracts for Datatypes

Taro Sekiyama, Yuki Nishida, and Atsushi Igarashi

In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2015

Abs DOI PDF Supp Code Slides

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 user-defined 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.
APLAS

Shifting the Blame - A Blame Calculus with Delimited Control

Taro Sekiyama, Soichiro Ueda, and Atsushi Igarashi

In Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS), 2015

Abs DOI PDF Slides

We study integration of static and dynamic typing in the presence of delimited-control operators. In a program where typed and untyped parts coexist, the run-time 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 cast-based 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.
書き換え可能参照付き顕在的契約計算

太朗関山

In 第17回プログラミングおよびプログラミング言語ワークショップ (PPL), 2015

ポスター
京都大学 Teen Racketeer 養成コース

淳五十嵐, 巧爾中澤, 誠二馬谷, 太朗関山, 裕一朗花田, 武大元, 洋平宮本, and 幸平末永

In 第17回プログラミングおよびプログラミング言語ワークショップ (PPL), 愛媛, 松山, 2015

ポスター
Manifest Contarcts with Mutable References

Taro Sekiyama

In The 17th JSSST Workshop on Programming and Programming Languages (PPL), 2015
京都大学 Teen Racketeer 養成コース

Atsushi Igarashi, Koji Nakazawa, Seiji Umatani, Taro Sekiyama, Yuichiro Hanada, Takeshi Omoto, Yohei Miyamoto, and Kohei Suenaga

In The 17th JSSST Workshop on Programming and Programming Languages (PPL), 2015

2014

顕在的契約計算のための代数的データ型

太朗関山, 雄気西田, and 淳五十嵐

In 第16回プログラミングおよびプログラミング言語ワークショップ (PPL), 2014

Abs PDF

顕在的契約計算は単純な型では捉えられないプログラムの性質—例えば 0での除算ができないといった制約—を表わしたソフトウェア契約を型システムに取り入れた型付計算体系である．契約は篩(ふるい)型 (refinement type)として静的型情報に現われるが，成り立つことが静的に保証できない契約はキャストにより実行時検査される．本研究では代数的データ型を導入した顕在的契約計算を与え，その性質について議論する．本研究で扱う代数的データ型は，構築子への契約の付与や項変数の抽象化により，リストの昇順性のようなデータ構造要素間の不変条件を型として表現できるだけでなく，構築子の対応関係を明示した代数的データ型間のキャストにより不変条件の成立の可否を実行時検査できる．また本論文ではデータ構造に関する実行時検査の遅延化や計算体系の実装についても論ずる．
Algebraic Datatypes for Manifest Contracts

Taro Sekiyama, Yuki Nishida, and Atsushi Igarashi

In Proceedings of the 16th JSSST Workshop on Programming and Programming Languages (PPL), 2014

PDF

2012

HOPE

Logical Relations for a Manifest Calculus, Fixed

Taro Sekiyama, and Atsushi Igarashi

In The 1st ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE), Copenhagen, Denmark, 2012

Abs Slides

A manifest contract calculus is a lambda-calculus 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 fixed-point operator, give logical relations for the extended calculus, and show their soundness with respect to what we call semi-typed contextual equivalence and that an upcast is logically related to an identity function.
顕在的契約計算におけるアップキャスト除去

太朗関山, and 淳五十嵐

In 第14回プログラミングおよびプログラミング言語ワークショップ (PPL), 2012

Abs PDF

顕在的契約計算体系は，実行時に検査されるソフトウェア契約の情報— 例えば，スタックの pop 操作は非空スタックを引数とする，といった，単純な型では捉えられない制約条件—が，篩(ふるい)型 (refinement type)として静的型情報に明示的に現れている型付計算体系である．顕在的契約計算体系での実行時検査は型変換(キャスト) により実現される．本研究では多相関数型と再帰関数を含む顕在的契約計算体系 F_H^fix において，部分型関係にある型の間のキャストであるアップキャストが除去可能であることを，F_H^fix の弱型付文脈等価性とそれに対し健全な論理関係を与え，アップキャストと恒等関数が論理関係にあることを証明することで示す．
Upcast Elimination in Manifest Contracts

Taro Sekiyama, and Atsushi Igarashi

In Proceedings of the 14th JSSST Workshop on Programming and Programming Languages (PPL), 2012

PDF

2010

コーディングパターンとキーワードを用いて生成したコードスニペットの推薦

太朗関山, 浩典伊達, 隆石尾, and 克郎井上

In 第72回情報処理学会全国大会, 東京, 2010

学生奨励賞受賞
Recommendation of Code Snippets Generated by Coding Patterns and Keywords

Taro Sekiyama, Date Hironori, Takashi Ishio, and Katsuro Inoue

In Proceedings of the 72th IPSJ National Convention, 2010