Language：English   Publishing type：Research paper (international conference proceedings)  

DOI： 10.1007/978-3-030-53518-6_2

Scopus

Other Link： https://arxiv.org/abs/2004.12713

Language：English   Publishing type：Research paper (scientific journal)  

DOI： 10.1007/s10817-019-09538-8

Web of Science

Scopus

Authorship：Lead author   Language：English   Publishing type：Research paper (scientific journal)  

Succinct data structures give space-efficient representations of large amounts of data without sacrificing performance. They rely on cleverly designed data representations and algorithms. We present here the formalization in Coq/SSReflect of two different tree-based succinct representations and their accompanying algorithms. One is the Level-Order Unary Degree Sequence, which encodes the structure of a tree in breadth-first order as a sequence of bits, where access operations can be defined in terms of Rank and Select, which work in constant time for static bit sequences. The other represents dynamic bit sequences as binary balanced trees, where Rank and Select present a low logarithmic overhead compared to their static versions, and with efficient insertion and deletion. The two can be stacked to provide a dynamic representation of dictionaries for instance. While both representations are well-known, we believe this to be their first formalization and a needed step towards provably-safe implementations of big data.

DOI： 10.4230/LIPIcs.ITP.2019.5

arXiv

Language：English   Publishing type：Research paper (scientific journal)  

This paper shows an encoding of linear types in OCaml and its applications. The encoding enables to write correct OCaml programs based on safe resource access guided by linear types. Linear types ensure that every variable is used exactly once, and, thus, they can be used to check the behavioural aspects of programs such as resource access and communication protocols in a static way. However, linear types require significant effort to be integrated into existing programming languages. Our encoding allows the vanilla OCaml typechecker to enforce linearity by using lenses and a parameterised monad. Parameterised monads are monads with a pre- and a post-condition, and we use them to track the creation and consumption of resources at the type level. Lenses, which point at parts of a data type, are used to refer to a resource in pre- and post-conditions. To handle comfortably structured data such as linearly typed lists, we further propose an extension to pattern matching based on the syntax-extension mechanism of OCaml. We show an application to static checking of communication protocols in OCaml.

DOI： 10.2197/ipsjjip.27.431

Scopus

Language：English  

Because of the increasing complexity of mathematical proofs, there is a growing interest in formalization using proof-assistants. In this paper, we explain new formal proofs of standard lemmas in data compression (Jensen's and Kraft's inequalities) as well as concrete applications (to the analysis of compression methods and Shannon-Fano codes). We explain in particular how one turns the paper proof into formal terms and the relation between the informal proof and the formal one. These formalizations come as an extension to an existing formal library for information theory and error-correcting codes.

DOI： 10.23919/ISITA.2018.8664276

Language：English   Publishing type：Research paper (scientific journal)  

Our goal is the production of formally-verified pieces of low-level code. Low-level code is typically written in C, so as to enable efficient manipulation of data at the bit-level and easy access to built-in features of CPUs. Proof-assistants arguably provide the most rigorous approach to formal verification of computer programs. Unfortunately, they only allow for extraction of runnable code in high-level languages such as ML. Of course it is possible to embed C snippets into ML programs, but this results in a complicated extraction process and the performance of the output program becomes difficult to anticipate. In this paper, we propose a new code generation scheme for the Coq proof-assistant that directly generates provably-safe C code. It is implemented in the form of plugins. The generation of C source code is done by a plugin performing beforehand monomorphization of Coq programs. The correctness of monomorphization can be proved within Coq. Code generation allows for user-guided changes of data structures. It is therefore possible to do formal verification using proof-friendly data structures, while enjoying optimized C representations in the output code. In order to ensure the safety of this transformation, we propose a new customizable monadification algorithm in the form of another plugin. Using monadification, one can ensure by the insertion of the right monads the preservation of critical invariants, such as the absence of overflows or complexity properties. We provide several examples to illustrate our approach, including a realistic use-case: the rank algorithm from succinct data structures.

DOI： https://doi.org/10.2197/ipsjjip.26.54

Language：English   Publishing type：Research paper (scientific journal)   Publisher：Information Processing Society of Japan  

Our goal is the production of formally-verified pieces of low-level code. Low-level code is typically written in C, so as to enable efficient manipulation of data at the bit-level and easy access to built-in features of CPUs. Proof-assistants arguably provide the most rigorous approach to formal verification of computer programs. Unfortunately, they only allow for extraction of runnable code in high-level languages such as ML. Of course it is possible to embed C snippets into ML programs, but this results in a complicated extraction process and the performance of the output program becomes difficult to anticipate. In this paper, we propose a new code generation scheme for the Coq proof-assistant that directly generates provably-safe C code. It is implemented in the form of plugins. The generation of C source code is done by a plugin performing beforehand monomorphization of Coq programs. The correctness of monomorphization can be proved within Coq. Code generation allows for user-guided changes of data structures. It is therefore possible to do formal verification using proof-friendly data structures, while enjoying optimized C representations in the output code. In order to ensure the safety of this transformation, we propose a new customizable monadification algorithm in the form of another plugin. Using monadification, one can ensure by the insertion of the right monads the preservation of critical invariants, such as the absence of overflows or complexity properties. We provide several examples to illustrate our approach, including a realistic use-case: the rank algorithm from succinct data structures.

DOI： 10.2197/ipsjjip.26.54

Scopus

Authorship：Lead author   Language：English   Publishing type：Research paper (scientific journal)  

Sound exhaustiveness checking of pattern-matching is an essential feature of functional programming languages, and OCaml supports it for GADTs. However this check is incomplete, in that it may fail to detect that a pattern can match no concrete value. In this paper we show that this problem is actually undecidable, but that we can strengthen the exhaustiveness and redundancy checks so that they cover more practical cases. The new algorithm relies on a clever modification of type inference for patterns.

DOI： http://dx.doi.org/10.4204/EPTCS.241.2

Authorship：Lead author   Language：English  

We describe here an extension of the OCaml type checker to represent units of measure. Such an addition allow a more precise typing of numerical values in applications such as scientific calculations. Our implementation use Kennedy's algorithm for unification, but subsumption requires a new algorithm, which we present here.

Publishing type：Research paper (international conference proceedings)   Publisher：Open Publishing Association  

Sound exhaustiveness checking of pattern-matching is an essential feature of functional programming languages, and OCaml supports it for GADTs. However this check is incomplete, in that it may fail to detect that a pattern can match no concrete value. In this paper we show that this problem is actually undecidable, but that we can strengthen the exhaustiveness and redundancy checks so that they cover more practical cases. The new algorithm relies on a clever modification of type inference for patterns.

DOI： 10.4204/EPTCS.241.2

Web of Science

Scopus

Language：Japanese   Publishing type：Research paper (scientific journal)   Publisher：JFLA 2017 - Journees Francophones des Langages Applicatifs  

Scopus

Language：English  

Language：English  

DOI： 10.1007/978-3-319-47846-3_16

Language：English  

By adding redundancy to transmitted data, error-correcting codes (ECCs) make it possible to communicate reliably over noisy channels. Minimizing redundancy and (de)coding time has driven much research, culminating with Low-Density Parity-Check (LDPC) codes. At first sight, ECCs may be considered as a trustful piece of computer systems because classical results are well-understood. But ECCs are also performance-critical so that new hardware calls for new implementations whose testing is always an issue. Moreover, research about ECCs is still flourishing with papers of ever-growing complexity. In order to provide means for implementers to perform verification and for researchers to firmly assess recent advances, we have been developing a formalization of ECCs using the SSReflect extension of the Coq proof-assistant. We report on the formalization of linear ECCs, duly illustrated with a theory about the celebrated Hamming codes and the verification of the sum-product algorithm for decoding LDPC codes.

DOI： 10.1007/978-3-319-22102-1_2

Authorship：Lead author   Language：English   Publishing type：Research paper (scientific journal)  

The type system of Objective Caml has many unique features, which make ensuring the correctness of its implementation difficult. One of these features is structurally polymorphic types, such as polymorphic object and variant types, which have the extra specificity of allowing recursion. We implemented in Coq a certified interpreter for Core ML extended with structural polymorphism and recursion. Along with type soundness of evaluation, soundness and principality of type inference are also proved.

DOI： 10.1017/S0960129513000066

Language：English   Publishing type：Research paper (scientific journal)  

By adding redundant information to transmitted data,
error-correcting codes (ECCs) make it possible to communicate
reliably over noisy channels. Minimizing redundancy and decoding
time has driven much research, culminating with Low-Density
Parity-Check (LDPC) codes. Hard-disk storage, wifi communications,
mobile phones, etc.: most modern devices now rely on ECCs and in
particular LDPC codes. Yet, correctness guarantees are only provided
by research papers of ever-growing complexity. One solution to
improve this situation is to enable certified implementations by
providing a formalization of ECCs. We think that a first difficulty
to achieve this goal has been partially lifted by the SSReflect
library, that provides a substantial formalization of linear
algebra. Using this library, we have been tackling the formalization
of linear ECCs. In this talk, we would like to introduce a Coq
library that makes it possible to formally state and verify basic
properties of linear ECCs. This library is already rich enough to
formalize most properties of Hamming codes and we are now in a
position to formalize the more difficult LDPC codes.

Authorship：Lead author   Language：Japanese  

OCamlのモジュールシステムは強力だが、名前空間の形成に使うと様々な問題点がある。まず、入れ子モジュールで階層化しようとすると、ファイル分割ができなくなるという問題。また、それを諦めて同じモジュールを複数の名前空間にコピーすると、一部の等価性が失われたり、型情報が異常に大きくなったりする。OCaml 4.02に導入された型レベル・エイリアスはモジュールへのリンクを型情報に記録することでそれらの問題の解決に貢献している。

Authorship：Lead author   Language：English  

GADTs, short for Generalized Algebraic DataTypes, which allow constructors of algebraic datatypes to be non-surjective, have many useful applications. However, pattern matching on GADTs introduces local type equality assumptions, which are a source of ambiguities that may destroy principal types--and must be resolved by type annotations.

We introduce ambivalent types to tighten the definition of ambiguities
and better confine them, so that type inference has principal types, remains monotonic, and requires fewer type annotations.

Authorship：Lead author   Language：English   Publishing type：Research paper (scientific journal)  

The ML module system facilitates the modular development of large programs,
through decomposition, abstraction and reuse. To increase its flexibility,
a lot of work has been devoted to extending it
with recursion, which is currently prohibited.
The introduction of recursion adds expressivity to the
module system. However it also creates
problems that a non-recursive module system does not have.

In this paper, we address one such problem, namely resolution of
path references. Paths are how one refers to nested modules in ML.
Without recursion, well-typedness guarantees termination of path resolution,
in other words, we can statically determine the module
that a path refers to. This does not always hold with recursive
module extensions, since the module system then can encode a
lambda-calculus with recursion, whose termination is undecidable
regardless of well-typedness. We formalize this problem
of path resolution by means of a rewrite system on paths and prove
that the problem is undecidable even without higher-order
functors, via an encoding of the Turing machine into a calculus with
just recursive modules, first-order functors, and nesting.
Motivated by this result, we introduce a further restriction on first-order functors,
limiting polymorphism on functor parameters by requiring
signatures for functor parameters to be non-recursive,
and show that this restriction is decidable and admits terminating path
resolution.

DOI： 10.1007/s10990-012-9083-6

Language：English  

A practical type system for ML-style recursive modules should address at least two technical challenges.
First, it needs to solve the double vision problem, which refers to an inconsistency between external and internal views of recursive modules.
Second, it needs to overcome the tension between practical decidability and expressivity which arises from the potential presence of cyclic type definitions caused by recursion between modules.
Although type systems in previous proposals solve the double vision problem and are also decidable, they fail to typecheck common patterns of recursive modules, such as functor fixpoints, that are essential to the expressivity of the module system and the modular development of recursive modules.

This paper proposes a novel type system for recursive modules that solves the double vision problem and typechecks common patterns of recursive modules including functor fixpoints.
First, we design a type system with a type equivalence based on weak bisimilarity, which does not lend itself to practical implementation in general, but accommodates a broad range of cyclic type definitions.
Then, we identify a practically implementable fragment using a type equivalence based on type normalization, which is expressive enough to typecheck typical uses of recursive modules.
Our approach is purely syntactic and the definition of the type system is ready for use in an actual implementation.

DOI： 10.1145/2076021.2048141

Authorship：Lead author   Language：English  

The type system of Objective Caml has many unique features, which make
ensuring the correctness of its implementation difficult.
One of these features is structurally polymorphic types, such as
polymorphic object and variant types, which have the extra specificity
of allowing recursion. We implemented in Coq a certified interpreter
for Core ML extended with structural polymorphism and recursion.
Along with type soundness of evaluation, soundness and
principality of type inference are also proved.

Authorship：Lead author   Language：Japanese  

Objective Camlの型システムは他言語と異なる機能を多くもっている．オブジェクト型や多相ヴァリアント型は構造的多相型によって実現されているが，その複雑さが実装の正しさの保証を難しくする．本研究では再帰型を含んだ構造的多相性を追加した Core ML に対して完全に証明されたインタープリタを Coq で実装した．中でも，再帰型の存在が証明を難しくしている．評価の安全性以外に，型推論の健全性と完全性も証明し，全てのアルゴリズムがプログラムとして抽出でき，実際に実行できる．

Language：English  

The ML module system supports the modular development of large
programs, through decomposition, abstraction and reuse.
To increase its flexibility, much work has been devoted to extending
it with recursion.
To keep type normalization terminating in such an extension, thus to
keep type checking decidable, path references must be resolved in a
terminating way.
Here paths are a mechanism to refer to components of modules.
In this paper, we show that the termination of path resolution is
undecidable for a ML-like module system with recursive modules and
first-order applicative functors, by encoding any Turing machine.
This demonstrates the need for some restriction.

Authorship：Lead author   Language：English  

Language：English  

Language：English  

Authorship：Lead author   Language：English  

Authorship：Lead author   Language：English  

Language：English  

Authorship：Lead author   Language：English  

Authorship：Lead author   Language：English   Publishing type：Research paper (scientific journal)  

Event date： 2022.9

Language：English   Presentation type：Oral presentation (general)  

Venue：Ljubljana   Country：Slovenia  

Event date： 2022.9

Language：English   Presentation type：Poster presentation  

Venue：Ljubljana   Country：Slovenia  

Event date： 2022.8 - 2022.9

Language：Japanese   Presentation type：Poster presentation  

Venue：Nagoya   Country：Japan  

Event date： 2022.6

Language：English   Presentation type：Oral presentation (general)  

Venue：Nantes   Country：France  

Event date： 2022.3

Language：English   Presentation type：Poster presentation  

Country：Japan  

Event date： 2022.3

Language：English   Presentation type：Poster presentation  

Country：Japan  

Event date： 2021.11

Language：English   Presentation type：Oral presentation (general)  

Country：Japan  

Other Link： https://t6s.github.io/tpp2021/

Event date： 2021.11

Language：English   Presentation type：Oral presentation (general)  

Country：Japan  

Other Link： https://t6s.github.io/tpp2021/

Event date： 2021.8

Language：English   Presentation type：Oral presentation (general)  

Venue：Online   Country：United States  

Event date： 2021.1

Language：English   Presentation type：Oral presentation (general)  

Venue：Online   Country：United States  

Event date： 2020.8

Language：English   Presentation type：Oral presentation (general)  

Venue：Online   Country：Korea, Republic of  

Event date： 2019.3

Language：English   Presentation type：Oral presentation (general)  

Venue：Hanamaki   Country：Japan  

Probabilities occur in many applications of computer science, such as communication theory and artificial intelligence. These are critical applications that require some form of verification to guarantee the quality of their implementations.
Unfortunately, probabilities are also the typical example of a mathematical theory whose abuses of notations make pencil-and-paper proofs difficult to formalize.
In this paper, we experiment a new formalization of conditional probabilities that we validate with two applications. First, we formalize the foundational definitions and theorems of information theory, extending previous work with new lemmas. Second, we formalize the notion of conditional independence and its properties, paving the road for a formalization of graphical probabilistic models.

Event date： 2018.11

Language：Japanese   Presentation type：Oral presentation (general)  

Venue：Tohoku University   Country：Japan  

Succinct data structures give space efficient representations of large amounts of data without sacrificing performance. In order to do that they rely on cleverly designed data representations and algorithms. We present here the formalization in Coq/SSReflect of the Level-Order Unary Degree Sequences (aka LOUDS), which encode the structure of a tree in breadth first order as a sequence of bits, where access operations can be defined in terms of Rank and Select, which work in constant time for static bit sequences.

Event date： 2018.10 - 2018.11

Language：Japanese   Presentation type：Oral presentation (general)  

Venue：日本IBM 箱崎事業所 (東京)   Country：Japan  

Event date： 2018.10

Language：French   Presentation type：Oral presentation (general)  

Venue：Paris 6 University / IRILL   Country：France  

This presentation shows an encoding and its applications of linear
types in OCaml. The encoding enables to write correct OCaml programs
based on safe resource access guided by linear types. Linear types
ensure that every variable is used exactly once, thus they are used to
check behavioural aspects of programs like resource accesses and
communication protocols in a static way. However, linear types
require significant effort to be integrated with the existing
programming languages. The encoding allows OCaml typecheckers to do
linear type checking by utilising lenses and a parameterised monad
without changing the compilers. Parameterised monads are monads with
a pre- and a post-condition, and we use them to track the creation
and consumption of resources in type-level. Lenses, which point at
parts of a data type, are used to refer to a resource in pre- and
post-conditions. To handle structured data like linearly-typed lists,
we further propose an extension to the pattern-matching construct
based on the syntax-extension mechanism in OCaml. We show an
application of statically checked communication protocol in OCaml.

Event date： 2018.8

Language：Japanese   Presentation type：Oral presentation (general)  

Venue：Osaka University   Country：Japan  

Succinct data structures give space efficient representations of large
amounts of data without sacrificing performance. In order to do that
they rely on cleverly designed data representations and algorithms.
We present here the formalization in Coq/SSReflect of two different
succinct tree algorithms. One is the Level-Order Unary Degree Sequence
(aka LOUDS), which encodes the structure of a tree in breadth first
order as a sequence of bits, where access operations can be defined in
terms of Rank and Select, which work in constant time for static bit
sequences. The other represents dynamic bit sequences as binary
red-black trees, where Rank and Select present a low logarithmic
overhead compared to their static versions, and with efficient Insert
and Delete. The two can be stacked to provide a dynamic representation
of dictionaries for instance. While both representations are
well-known, we believe this to be their first formalization and
a needed step towards provably-safe implementations of big data.

Event date： 2017.2

Language：English   Presentation type：Oral presentation (general)  

Scopus

Event date： 2015.9

Language：English   Presentation type：Oral presentation (general)  

Country：Japan  

Sound exhaustiveness checking of pattern-matching is an essential feature of GADTs, and OCaml has supported it from day one, by showing that the remaining cases could never be typed. Not only does it allow the programmer to be confident in the soundness of his code, but it also it permits optimizations which make GADTs more efficient. However, while this approach is sound and can prune some simple uses of GADTs, some other uses caused superfluous warnings. In this talk we describe the original approach and how we ensure its soundness, and show that one can do better by turning the type-checking of extra cases into a backtracking proof search algorithm. We also show that the exhaustiveness problem is undecidable for GADTs, so that this proof search must be kept partial.

Event date： 2014.9

Language：English   Presentation type：Oral presentation (general)  

Country：Sweden  

We promote the use of type-level module aliases, a trivial extension of the ML module system, which helps avoiding code dependencies, and provides an alternative to strengthening for type equalities.

Event date： 2014.7

Language：English   Presentation type：Oral presentation (general)  

Country：Austria  

By adding redundant information to transmitted data, error-correcting codes (ECCs) make it possible to communicate reliably over noisy channels. Minimizing redundancy and coding/decoding time has driven much research, culminating with Low-Density Parity-Check (LDPC) codes. Hard-disk storage, wifi communications, mobile phones, etc.: most modern devices now rely on ECCs and in particular LDPC codes. Yet, correctness guarantees are only provided by research papers of ever-growing complexity. One solution to improve this situation is to provide a formalization of ECCs. We think that a first difficulty to achieve this goal has been lifted by the SSReflect library, that provides a substantial formalization of linear algebra. Using this library, we have been tackling the formalization of linear ECCs. Our formalization of linear ECCs is already rich enough to formalize most properties of Hamming codes and we are now in a position to formalize the more difficult LDPC codes.

Event date： 2013.9

Language：English   Presentation type：Oral presentation (general)  

Country：United States  

Event date： 2013.9

Language：English   Presentation type：Oral presentation (general)  

Country：United States  

Event date： 2012.9

Language：English   Presentation type：Oral presentation (general)  

Country：Denmark  

GADTs, short for Generalized Algebraic DataTypes, extend usual algebraic datatypes with a form of dependent typing that has many useful applications, but raises serious issues for type inference.
Pattern matching on GADTs introduces type equalities with limited scopes, which are a source of ambiguities that may destroy principal types - and must be resolved by type annotations.
By tracing ambiguities in types, we may tighten the definition of ambiguities and confine them, so as to request fewer type annotations.
Now in use in OCaml~4.00, this solution also lifts some restrictions on object and polymorphic variant types that appeared in a previous implementation of GADTs in OCaml.

Event date： 2012.8

Language：English   Presentation type：Oral presentation (general)  

Country：Japan  

Recursive modules are a useful extension to the ML module system, but they create a tension between expressivity and decidability.
We define a path resolution calculus, intended to describe the resolution of recursive references in an applicative recursive module system, and show that having both nesting and first-order functors is sufficient to get undecidability. We then introduce a further restriction, requiring the signatures of functor parameters to be non-recursive, and show that this restriction is decidable and admits terminating path resolution.

Event date： 2011.9

Language：English   Presentation type：Symposium, workshop panel (public)  

Country：Japan  

Generalized Algebraic Datatypes, or GADTs, extend algebraic datatypes
by allowing an explicit relation between type parameters and case analysis.
They have useful applications, among others for encoding invariants of
data structures, or providing tag-less data representations.

We have implemented them in OCaml, by directly modifying the type
inference engine. We discuss the technical choices involved, and
the properties expected to hold. In particular, we have worked on two
aspects of inference: principality, which holds only by requiring some
derivations to be minimal, and exhaustiveness of pattern-matching,
which requires a new notion of incompatibility.

Event date： 2011.6

Language：English   Presentation type：Oral presentation (general)  

Country：France  

Generalized Algebraic Datatypes, or GADTs, extend algebraic datatypes
by allowing an explicit relation between type parameters and case analysis.
They have useful applications, among others for encoding invariants of
data structures, or providing tag-less data representations.

We have implemented them in OCaml, by directly modifying the type
inference engine. We discuss the technical choices involved, and
the properties expected to hold. In particular, we have worked on two
aspects of inference: principality, which holds only by requiring some
derivations to be minimal, and exhaustiveness of pattern-matching,
which requires a new notion of incompatibility.

Event date： 2010.9

Language：English   Presentation type：Oral presentation (general)  

Notwithstanding its name, Objective Caml has a
full-fledged SML-style module system.
Its applicative functors allow for flexible parameterization
of components, and many libraries, including the preprocessor Camlp4,
use them for their structure. More recent extensions include the
addition of recursive modules, and private row
types, which allow even more involved structuring.

While this module language is overall successful, as demonstrated by
its active use, it has also some well-

Event date： 2009.11

Language：English   Presentation type：Oral presentation (general)  

Country：Japan  

Event date： 2009.9

Language：Japanese   Presentation type：Oral presentation (invited, special)  

Country：Japan  

ective Camlは関数型プログラミング言語の一つだが，コンパイラおよび処理系が高速で，利用者が多くなって来た．その最大の利点は，先進的な型システムによって，型を明示的に書かなくても，型推論の段階でほとんどのバグが見付かるということである．コンパイラがバグを全て見付けるということ自体は理論的に不可能なのに，その効果がどこから来ているかを説明し，プログラムの安全な書き方に導いていく

Event date： 2009.9

Language：English   Presentation type：Oral presentation (general)  

The many unique features of OCaml's type system make ensuring the correctness of its implementation difficult. Among those, structurally polymorphic types, such as polymorphic object and variant types, have the extra specificity of allowing recursion. I implemented in Coq a certified interpreter for Core ML extended with structural polymorphism and recursion. Along with type soundness of
evaluation, soundness and principality of typ inference were proved.

Event date： 2008.11

Language：English   Presentation type：Oral presentation (general)  

Country：Japan  

Event date： 2008.6

Presentation type：Oral presentation (invited, special)  

Objective Caml's type system is a complex beast. At its core are structurally polymorphic types, with objects and variants, with also labels and first class polymorphism. On top of that it has subtyping and a typed module system. We report on experiments in proving properties of the underlying specifications using Coq, namely soundness of objects and variants, and some properties of a fragment
of subtyping.

Event date： 2007.11

Language：Japanese   Presentation type：Oral presentation (general)  

Country：Japan