担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（学術雑誌）  

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

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：Journal of Information Processing  

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

記述言語：英語  

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

記述言語：英語   掲載種別：研究論文（学術雑誌）  

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

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：Journal of Information Processing  

<p>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.</p>

DOI： 10.2197/ipsjjip.26.54

Scopus

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（学術雑誌）  

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

担当区分：筆頭著者   記述言語：英語  

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.

掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Electronic Proceedings in Theoretical Computer Science, EPTCS  

DOI： 10.4204/EPTCS.241.2

Web of Science

Scopus

記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：JFLA 2017 - Journees Francophones des Langages Applicatifs  

Scopus

記述言語：英語  

記述言語：英語  

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

記述言語：英語  

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

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（学術雑誌）  

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

記述言語：英語   掲載種別：研究論文（学術雑誌）  

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.

担当区分：筆頭著者   記述言語：日本語  

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

担当区分：筆頭著者   記述言語：英語  

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.

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（学術雑誌）  

DOI： 10.1007/s10990-012-9083-6

記述言語：英語  

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

担当区分：筆頭著者   記述言語：英語  

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.

担当区分：筆頭著者   記述言語：日本語  

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

記述言語：英語  

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.

担当区分：筆頭著者   記述言語：英語  

記述言語：英語  

記述言語：英語  

担当区分：筆頭著者   記述言語：英語  

担当区分：筆頭著者   記述言語：英語  

記述言語：英語  

担当区分：筆頭著者   記述言語：英語  

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（学術雑誌）  

開催年月日： 2022年8月 - 2022年9月

記述言語：日本語   会議種別：ポスター発表  

開催地：名古屋   国名：日本国  

開催年月日： 2022年6月

記述言語：英語   会議種別：口頭発表（一般）  

開催地：Nantes   国名：フランス共和国  

開催年月日： 2022年3月

記述言語：英語   会議種別：ポスター発表  

国名：日本国  

開催年月日： 2022年3月

記述言語：英語   会議種別：ポスター発表  

国名：日本国  

開催年月日： 2021年11月

記述言語：英語   会議種別：口頭発表（一般）  

国名：日本国  

その他リンク： https://t6s.github.io/tpp2021/

開催年月日： 2021年11月

記述言語：英語   会議種別：口頭発表（一般）  

国名：日本国  

その他リンク： https://t6s.github.io/tpp2021/

開催年月日： 2021年8月

記述言語：英語   会議種別：口頭発表（一般）  

開催地：Online   国名：アメリカ合衆国  

開催年月日： 2021年1月

記述言語：英語   会議種別：口頭発表（一般）  

開催地：Online   国名：アメリカ合衆国  

開催年月日： 2020年8月

記述言語：英語   会議種別：口頭発表（一般）  

開催地：Online   国名：大韓民国  

開催年月日： 2019年3月

記述言語：英語   会議種別：口頭発表（一般）  

開催地：Hanamaki   国名：日本国  

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.

開催年月日： 2018年11月

記述言語：日本語   会議種別：口頭発表（一般）  

開催地：Tohoku University   国名：日本国  

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.

開催年月日： 2018年10月 - 2018年11月

記述言語：日本語   会議種別：口頭発表（一般）  

開催地：日本IBM 箱崎事業所 (東京)   国名：日本国  

開催年月日： 2018年10月

記述言語：フランス語   会議種別：口頭発表（一般）  

開催地：Paris 6 University / IRILL   国名：フランス共和国  

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.

開催年月日： 2018年8月

記述言語：日本語   会議種別：口頭発表（一般）  

開催地：Osaka University   国名：日本国  

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.

開催年月日： 2017年2月

記述言語：英語   会議種別：口頭発表（一般）  

Scopus

開催年月日： 2015年9月

記述言語：英語   会議種別：口頭発表（一般）  

国名：日本国  

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.

開催年月日： 2014年9月

記述言語：英語   会議種別：口頭発表（一般）  

国名：スウェーデン王国  

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.

開催年月日： 2014年7月

記述言語：英語   会議種別：口頭発表（一般）  

国名：オーストリア共和国  

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.

開催年月日： 2013年9月

記述言語：英語   会議種別：口頭発表（一般）  

国名：アメリカ合衆国  

開催年月日： 2013年9月

記述言語：英語   会議種別：口頭発表（一般）  

国名：アメリカ合衆国  

開催年月日： 2012年9月

記述言語：英語   会議種別：口頭発表（一般）  

国名：デンマーク王国  

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.

開催年月日： 2012年8月

記述言語：英語   会議種別：口頭発表（一般）  

国名：日本国  

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.

開催年月日： 2011年9月

記述言語：英語   会議種別：シンポジウム・ワークショップ パネル（公募）  

国名：日本国  

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.

開催年月日： 2011年6月

記述言語：英語   会議種別：口頭発表（一般）  

国名：フランス共和国  

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.

開催年月日： 2010年9月

記述言語：英語   会議種別：口頭発表（一般）  

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-

開催年月日： 2009年11月

記述言語：英語   会議種別：口頭発表（一般）  

国名：日本国  

開催年月日： 2009年9月

記述言語：日本語   会議種別：口頭発表（招待・特別）  

国名：日本国  

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

開催年月日： 2009年9月

記述言語：英語   会議種別：口頭発表（一般）  

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.

開催年月日： 2008年11月

記述言語：英語   会議種別：口頭発表（一般）  

国名：日本国  

開催年月日： 2008年6月

会議種別：口頭発表（招待・特別）  

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.

開催年月日： 2007年11月

記述言語：日本語   会議種別：口頭発表（一般）  

国名：日本国