20 citations · 57 across the 16 of their papers we have counts for
16 papers
Unifying Function- and Argument-First Bidirectional Type Systems
Takuma Yoshioka, Taro Sekiyama, Atsushi Igarashi
Bidirectional typing mixes type synthesis and type checking into a single process. Existing bidirectional type systems can be classified into two styles based on whether, given a f…
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers
Fuga Kawamata, Hiroshi Unno, Taro Sekiyama +1
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 practica…
Temporal Verification with Answer-Effect Modification
Taro Sekiyama, Hiroshi Unno
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…
Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning
Minchao Wu, Takeshi Tsukada, Hiroshi Unno +2
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. Desp…
Toward Neural-Network-Guided Program Synthesis and Verification
Naoki Kobayashi, Taro Sekiyama, Issei Sato +1
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 c…
Signature Restriction for Polymorphic Algebraic Effects
Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi
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 g…
Gradual Typing for Extensibility by Rows
Taro Sekiyama, Atsushi Igarashi
This work studies gradual typing for row types and row polymorphism. Key ingredients in this work are the dynamic row type, which represents a statically unknown part of a row, and…
Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces
Takamasa Okudono, Masaki Waga, Taro Sekiyama +1
We present a method to extract a weighted finite automaton (WFA) from a recurrent neural network (RNN). Our algorithm is based on the WFA learning algorithm by Balle and Mohri, whi…
Dynamic Type Inference for Gradual Hindley--Milner Typing
Yusuke Miyazaki, Taro Sekiyama, Atsushi Igarashi
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 algorith…
Handling polymorphic algebraic effects
Taro Sekiyama, Atsushi Igarashi
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…
Reasoning about Polymorphic Manifest Contracts
Taro Sekiyama, Atsushi Igarashi
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…
Automated proof synthesis for propositional logic with deep neural networks
Taro Sekiyama, Kohei Suenaga
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. T…
Profile-guided memory optimization for deep neural networks
Taro Sekiyama, Takashi Imamichi, Haruki Imai +1
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 mem…
Lung Nodule Classification by the Combination of Fusion Classifier and Cascaded Convolutional Neural Networks
Masaharu Sakamoto, Hiroki Nakano, Kun Zhao +1
Lung nodule classification is a class imbalanced problem, as nodules are found with much lower frequency than non-nodules. In the class imbalanced problem, conventional classifiers…
Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic
Taro Sekiyama, Akifumi Imanishi, Kohei Suenaga
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 go…
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 +1
Lung nodule classification is a class imbalanced problem because nodules are found with much lower frequency than non-nodules. In the class imbalanced problem, conventional classif…