2024/05/10 更新

写真a

ガリグ ジヤツク
GARRIGUE Jacques
GARRIGUE, Jacques
所属
大学院多元数理科学研究科 多元数理科学専攻 数理解析 教授
大学院担当
大学院多元数理科学研究科
学部担当
理学部 数理学科
職名
教授

学位 1

  1. 理学博士 ( 1995年3月   東京大学 ) 

研究キーワード 1

  1. 関数型言語 型理論 ラムダ計算

研究分野 2

  1. その他 / その他  / ソフトウエア

  2. その他 / その他  / 情報学基礎

現在の研究課題とSDGs 3

  1. 進んだ型システムをもったプログラミング言語における型検証器の機械的な証明

  2. 確率的グラフィカルモデルの形式検証とその人工知能への応用

  3. 多機能関数型プログラミング言語の堅牢な型検査

経歴 4

  1. 名古屋大学   大学院多元数理科学研究科 数理解析   教授

    2018年8月 - 現在

  2. 名古屋大学   大学院多元数理科学研究科 数理解析   准教授

    2007年4月 - 2018年7月

  3. 名古屋大学   大学院多元数理科学研究科   助教授

    2004年10月 - 2007年3月

  4. 京都大学数理解析研究所 助手

    1995年4月 - 2004年9月

      詳細を見る

    国名:日本国

学歴 2

  1. パリ高等師範学校   数学情報科学科

    1990年9月 - 1998年3月

      詳細を見る

    国名: 日本国

  2. 東京大学   理学系研究科   情報科学専攻

    1992年10月 - 1995年3月

      詳細を見る

    国名: 日本国

所属学協会 3

  1. 日本ソフトウェア科学会

  2. 情報処理学会

  3. ACM

委員歴 2

  1. 情報処理学会プログラミング研究会   幹事  

    2016年4月 - 2020年3月   

      詳細を見る

    団体区分:学協会

  2. 情報処理学会プログラミング研究会編集委員会   編集委員  

    2007年4月 - 2011年3月   

受賞 1

  1. 高橋奨励賞

    2010年6月   日本ソフトウェア科学会  

     詳細を見る

    受賞国:日本国

 

論文 36

  1. Typed compositional quantum computation with lenses

    Jacques Garrigue, Takafumi Saikawa

    arXiv     2024年3月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(その他学術会議資料等)  

    DOI: https://doi.org/10.48550/arXiv.2311.14347

  2. A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    arXiv     2023年12月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(その他学術会議資料等)  

    DOI: https://doi.org/10.48550/arXiv.2312.06103

  3. An intuitionistic set-theoretical model of fully dependent CC omega 査読有り

    Sato Masahiro, Garrigue Jacques

    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE     2023年4月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.1017/S0960129523000087

    Web of Science

  4. A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism 査読有り 国際共著

    Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa

    Journal of Functional Programming   31 巻   2021年7月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.1017/S0956796821000137

    その他リンク: https://www.math.nagoya-u.ac.jp/~garrigue/papers/

  5. Reasoning with Conditional Probabilities and Joint Distributions in Coq 査読有り

    AFFELDT Reynald, GARRIGUE Jacques, SAIKAWA Takafumi

    Computer Software   37 巻 ( 3 ) 頁: 79 - 95   2020年7月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)   出版者・発行元:Iwanami Shoten  

    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.

    DOI: https://doi.org/10.11309/jssst.37.3_79

  6. Formal adventures in convex and conical spaces 査読有り

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    Conference on Intelligent Computer Mathematics   12236 LNAI 巻   頁: 23 - 38   2020年6月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

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

    Scopus

    その他リンク: https://arxiv.org/abs/2004.12713

  7. A Library for Formalization of Linear Error-Correcting Codes

    Affeldt Reynald, Garrigue Jacques, Saikawa Takafumi

    JOURNAL OF AUTOMATED REASONING   64 巻 ( 6 ) 頁: 1123 - 1164   2020年1月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)   出版者・発行元:Journal of Automated Reasoning  

    DOI: 10.1007/s10817-019-09538-8

    Web of Science

    Scopus

  8. Proving tree algorithms for succinct data structures 査読有り

    Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka

    International Conference on Interactive Theorem Proving (ITP 2019)   10 巻   頁: 5:1--5:19   2019年9月

     詳細を見る

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

    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

  9. Lightweight linearly-typed programming with lenses and monads 査読有り

    Imai Keigo, Garrigue Jacques

    Journal of Information Processing   27 巻 ( 0 ) 頁: 431-444 - 444   2019年5月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)   出版者・発行元: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

  10. Examples of Formal Proofs about Data Compression 査読有り

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    International Symposium on Information Theory and Its Applications     2018年10月

     詳細を見る

    記述言語:英語  

    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

  11. Safe Low-level Code Generation in Coq Using Monomorphization and Monadification 査読有り

    Akira Tanaka, Reynald Affeldt, Jacques Garrigue

    Journal of Information Processing   26 巻   頁: 54-72   2018年1月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    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

  12. Safe low-level code generation in Coq using monomorphization and monadification 査読有り

    Tanaka A.

    Journal of Information Processing   26 巻 ( 0 ) 頁: 54 - 72   2018年1月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)   出版者・発行元: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

  13. GADTs and Exhaustiveness: Looking for the Impossible 招待有り 査読有り

    Jacques Garrigue, Jacques Le Normand

    Electronic Proceedings in Theoretical Computer Science   ( 241 ) 頁: 23-35   2017年2月

     詳細を見る

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


    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

  14. Des unites dans le typeur 査読有り

    Jacques Garrigue, Dara Ly

    Journées Francaises des Langages Applicatifs     頁: 1-6   2017年1月

     詳細を見る

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

    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.

  15. GADTs and Exhaustiveness: Looking for the Impossible 招待有り 査読有り

    Garrigue Jacques, Le Normand Jacques

    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE   241 巻 ( 241 ) 頁: 23 - 35   2017年

     詳細を見る

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

    DOI: 10.4204/EPTCS.241.2

    Web of Science

    Scopus

  16. Units in the type checker

    Garrigue J., Ly D.

    JFLA 2017 - Journees Francophones des Langages Applicatifs     頁: 85 - 90   2017年

     詳細を見る

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

    Scopus

  17. Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    International Symposium on Information Theory and Its Applications     頁: 537-541   2016年10月

     詳細を見る

    記述言語:英語  

  18. Formal Verification of the rank Algorithm for Succinct Data Structures 査読有り

    Akira Tanaka, Reynald Affeldt, Jacques Garrigue

    Formal Methods and Software Engineering, Springer-Verlag LNCS   10009 巻   頁: 243-260   2016年10月

     詳細を見る

    記述言語:英語  

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

  19. Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory 査読有り

    Reynald Affeldt, Jacques Garrigue

    6th Conference on Interactive Theorem Proving (ITP 2015), Springer LNCS   9236 巻   頁: 17-33   2015年8月

     詳細を見る

    記述言語:英語  

    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

  20. A Certified Implementation of ML with Structural Polymorphism and Recursive Types 査読有り

    Jacques Garrigue

    Mathematical Structures in Computer Science   25 巻 ( 4 ) 頁: 867-891   2015年4月

     詳細を見る

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

    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

  21. Formalization of linear error codes using SSreflect

    Reynald Affeldt, Jacques Garrigue

    Math for industry   61 巻   頁: 76-78   2015年3月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    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.

  22. 分割できながら等価:型レベル・エイリアス

    日本ソフトウェア科学会全国大会     頁: PPL4-2   2014年9月

     詳細を見る

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

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

  23. Ambivalent types for principal type inference with GADTs 査読有り

    Jacques Garrigue, Didier Remy

    11th Asian Symposium on Programming Languages and Systems     頁: 300-315   2013年12月

     詳細を見る

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

    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.

  24. Path resolution for recursive nested modules 査読有り

    Jacques Garrigue, 中田景子

    Higher-Order and Symbolic Computation     2012年5月

     詳細を見る

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

    DOI: 10.1007/s10990-012-9083-6

  25. A Syntactic Type System for Recursive Modules 査読有り

    Hyonseung Im, Keiko Nakata, Jacques Garrigue and Sungwoo Park

    ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications     2011年10月

     詳細を見る

    記述言語:英語  

    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

  26. A Certified Implementation of ML with Structural Polymorphism 査読有り

    Jacques Garrigue

    Proceedings of the 8th Asian Symposium on Programming Language and Systems.   LNCS 巻 ( 6461 ) 頁: 360-375   2010年11月

     詳細を見る

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

    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.

  27. *構造的多相性をもった言語の検証つきインタープリタ

    日本ソフトウェアか学会第26回大会講演論文集   26 巻   2009年9月

     詳細を見る

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

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

  28. Path resolution for recursive nested modules is undecidable 査読有り

    Keiko Nakata, Jacques Garrigue

    9th International Workshop on Termination     頁: 43-47   2007年6月

     詳細を見る

    記述言語:英語  

    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.

  29. *Private rows: abstracting the unnamed 査読有り

    Jacques Garrigue

    4th Asian Symposium on Programming Languages and Systems   LNCS 巻 ( 4279 )   2006年11月

     詳細を見る

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

  30. *Recursive Modules for Programming 査読有り

    Keiko Nakata, Jacques Garrigue

    International Conference on Functional Programming   11 巻   2006年9月

     詳細を見る

    記述言語:英語  

  31. Recursive Object-Oriented Modules 査読有り

    Keiko Nakata, Akira Ito, Jacques Garrigue

    Workshop on Foundations of Object-Oriented Languages   11 巻   2005年1月

     詳細を見る

    記述言語:英語  

  32. *Relaxing the value restriction 査読有り

    Jacques Garrigue

    International Symposium on Functional and Logic Programming   LNCS 巻 ( 2998 )   2004年4月

     詳細を見る

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

  33. Typing deep pattern-matching in presence of polymorphic variants

    Jacques Garrigue

      7 巻   2004年3月

     詳細を見る

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

  34. Simple Type Inference for Structural Polymorphism 査読有り

    Jacques Garrigue

    9th Workshop on Foundations of Object-Oriented Languages   9 巻   2002年1月

     詳細を見る

    記述言語:英語  

  35. Code reuse through polymorphic variants 査読有り

    Jacques Garrigue

      25 巻   頁: 93ー100   2000年

     詳細を見る

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

  36. Extending ML with semi-explicit higher order polymorphism 査読有り

    Jacques Garrigue, Didier Remy

    Information and Computation   155 巻   頁: 134-171   1999年

     詳細を見る

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

▼全件表示

書籍等出版物 3

  1. Programming Languages and Systems, 12th Asian Symposium (APLAS 2014)

    Jacques Garrigue, editor( 担当: 単著)

    Springer  2014年11月  ( ISBN:9783319127354

     詳細を見る

    記述言語:英語

  2. Functional and Logic Programming, 9th International Symposium (FLOPS 2008)

    Jacques Garrigue and Manuel Hermenegildo, editors( 担当: 共著)

    Springer LNCS  2008年3月  ( ISBN:978-3-540-78968-0

     詳細を見る

    記述言語:英語

  3. コンピュータサイエンス入門―アルゴリズムとプログラミング言語

    大堀 淳, ジャック ガリグ, 西村 進( 担当: 共著)

    岩波書店  1999年 

     詳細を見る

    記述言語:日本語

講演・口頭発表等 38

  1. Environment-friendly monadic equational reasoning for OCaml 国際会議

    Jacques Garrigue, Reynald Affeldt, Takafumi Saikawa

    APLAS NIER  2023年11月26日  Asian Association for Foundation of Software

     詳細を見る

    開催年月日: 2023年11月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Taipei   国名:台湾  

  2. Environment-friendly monadic equational reasoning for OCaml

    Jacques Garrigue

    The 19th Theorem Proving and Provers meeting (TPP 2023)  2023年10月30日 

     詳細を見る

    開催年月日: 2023年10月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Tokyo Institute of Technology   国名:日本国  

  3. A type-theoretic account of quantum computation 国際会議

    Jacques Garrigue, Takafumi Saikawa

    Workshop on Type-Driven Development  2023年9月4日  ACM

     詳細を見る

    開催年月日: 2023年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Seattle, WA   国名:アメリカ合衆国  

    その他リンク: https://www.math.nagoya-u.ac.jp/~garrigue/papers/index.html

  4. Environment-friendly monadic equational reasoning for OCaml 国際会議

    Takafumi Saikawa, Reynald Affeldt, Jacques Garrigue

    Coq Workshop  2023年7月31日 

     詳細を見る

    開催年月日: 2023年7月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Bialystok   国名:ポーランド共和国  

  5. OCaml プログラムの Coq への変換とプログラムの正しさの証明

    毎田詠人, 中村薫, 才川隆文, Jacques Garrigue

    第25回プログラミングおよびプログラミング言語ワークショップ  2023年3月6日  日本ソフトウェア科学会プログラミング論研究会

     詳細を見る

    開催年月日: 2023年3月

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

    開催地:名古屋大学   国名:日本国  

  6. Interpreting OCaml GADTs into Coq 国際会議

    Jacques Garrigue, Takafumi Saikawa

    ML Family Workshop 2022  2022年9月15日  ACM SIGPLAN

     詳細を見る

    開催年月日: 2022年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Ljubljana   国名:スロベニア共和国  

  7. Formalizing quantum circuits with MathComp/Ssreflect 国際会議

    Jacques Garrigue, Takafumi Saikawa

    The Third International Workshop on Programming Languages for Quantum Computing  2022年9月15日  ACM SIGPLAN

     詳細を見る

    開催年月日: 2022年9月

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

    開催地:Ljubljana   国名:スロベニア共和国  

  8. OCaml から Coq へのコンパイラ及び翻訳されたプログラムの証明

    中村薫, Jacques Garrigue, 毎田詠人, 才川隆文

    日本ソフトウェア科学会第40回大会  2022年8月31日  日本ソフトウェア科学会

     詳細を見る

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

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

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

  9. Validating OCaml soundness by translation into Coq 国際会議

    Saikawa Takafumi, Jacques Garrigue

    28th International Conference on Types for Proofs and Programs  2022年6月24日 

     詳細を見る

    開催年月日: 2022年6月

    記述言語:英語   会議種別:口頭発表(一般)  

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

  10. A Gallina generating backend to check OCaml’s type inference correctness

    Jacques Garrigue, Takafumi Saikawa

    PPL 2022  2022年3月6日 

     詳細を見る

    開催年月日: 2022年3月

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

    国名:日本国  

  11. Formalizing quantum circuits with MathComp/Ssreflect

    Takafumi Saikawa, Jacques Garrigue

    PPL 2022  2022年3月7日 

     詳細を見る

    開催年月日: 2022年3月

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

    国名:日本国  

  12. Proving the correctness of OCaml typing by translation into Coq

    Jacques Garrigue

    Theorem Proving and Provers 2021  2021年11月22日 

     詳細を見る

    開催年月日: 2021年11月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

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

  13. Formalizing quantum circuits with MathComp/Ssreflect

    Takafumi Saikawa

    Theorem Proving and Provers 2021  2021年11月21日 

     詳細を見る

    開催年月日: 2021年11月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

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

  14. Formalizing OCaml GADT typing in Coq 国際会議

    Jacques Garrigue, Xuanrui Qi

    ML Workshop 2021  2021年8月26日  ACM SIGPLAN

     詳細を見る

    開催年月日: 2021年8月

    記述言語:英語   会議種別:口頭発表(一般)  

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

  15. Towards a Coq specification for Generalized Algebraic Datatypes in OCaml 国際会議

    Jacques Garrigue, Xuanrui Qi

    International Workshop on Coq for Programming Languages (CoqPL 2021)  2021年1月19日  ACM SIGPLAN

     詳細を見る

    開催年月日: 2021年1月

    記述言語:英語   会議種別:口頭発表(一般)  

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

  16. Tracking injectivity and nominality beyond abstraction 国際会議

    Jacques Garrigue

    ML Family Workshop  2020年8月27日  ACM SIGPLAN

     詳細を見る

    開催年月日: 2020年8月

    記述言語:英語   会議種別:口頭発表(一般)  

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

  17. Reasoning with Conditional Probabilities and Joint Distributions in Coq

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    JSSST Workshop on Programming and Programming Languages 

     詳細を見る

    開催年月日: 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.

  18. Correctness of the LOUDS encoding of tree structures

    Jacques Garrigue

    Theorem Proving and Provers meeting 

     詳細を見る

    開催年月日: 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.

  19. レンズとモナドを用いた軽量な線形型付きプログラミング

    今井 敬吾, Jacques Garrigue

    情報処理学会プログラミング研究発表会 

     詳細を見る

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

    記述言語:日本語   会議種別:口頭発表(一般)  

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

  20. Lightweight linearly-typed programming with lenses and monads

    Keigo Imai and Jacques Garrigue

    OCaml Users in Paris 

     詳細を見る

    開催年月日: 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.

  21. Proving tree algorithms for succinct data structures

    Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka

    JSSST National Meeting 

     詳細を見る

    開催年月日: 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.

  22. Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes

    Affeldt R.

    Proceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016 

     詳細を見る

    開催年月日: 2017年2月

    記述言語:英語   会議種別:口頭発表(一般)  

    Scopus

  23. GADTs and exhaustiveness: looking for the impossible 国際会議

    Jacques Garrigue, Jacques Le Normand

    Workshop on ML 

     詳細を見る

    開催年月日: 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.

  24. Type-level module aliases: independent and equal 国際会議

    Jacques Garrigue

    Jacques Garrigue 

     詳細を見る

    開催年月日: 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.

  25. Formalization of Error-correcting Codes using SSReflect 国際会議

    Reynald Affeldt, Jacques Garrigue

    Coq Workshop 

     詳細を見る

    開催年月日: 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.

  26. Runtime types in OCaml 国際会議

    Gregoire Henry, Jacques Garrigue

    OCaml 2013 

     詳細を見る

    開催年月日: 2013年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:アメリカ合衆国  

  27. On variance, injectivity, and abstraction 国際会議

    Jacques Garrigue

    OCaml 2013 

     詳細を見る

    開催年月日: 2013年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:アメリカ合衆国  

  28. Tracing ambiguity in GADT type inference 国際会議

    Jacques Garrigue, Didier Remy

    ACM-SIGPLAN Workshop on ML 

     詳細を見る

    開催年月日: 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.

  29. Path resolution for nested recursive modules

    Jacques Garrigue, Keiko Nakata

    Dependable components seminar 

     詳細を見る

    開催年月日: 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.

  30. Adding GADTs to OCaml: a direct approach 国際会議

    Jacques Garrigue, Jacques Le Normand

    ACM SIGPLAN Workshop on ML 

     詳細を見る

    開催年月日: 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.

  31. Adding GADTs to OCaml: the direct approach

    Jacques Garrigue, Jacques Le Normand

    Gallium-Moscova seminar 

     詳細を見る

    開催年月日: 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.

  32. First-class modules and composable signatures in Objective Caml3.12 国際会議

    The 2010 ACM SIGPLAN Workshop on ML 

     詳細を見る

    開催年月日: 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-

  33. A certified interpreter for a subset of OCaml

    Theorem Proving and Provers 2009 

     詳細を見る

    開催年月日: 2009年11月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  34. Objective Camlがなぜバグを書かせないのか 招待有り

    数学ソフトウェアとフリードキュメント/09 

     詳細を見る

    開催年月日: 2009年9月

    記述言語:日本語   会議種別:口頭発表(招待・特別)  

    国名:日本国  

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

  35. A Certified Interpreter for ML with Structural Polymorphism 国際会議

    4th Informal ACM SIGPLAN Workshop on Mechanizing MetatheoryEdinburgh, Scotland 

     詳細を見る

    開催年月日: 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.

  36. Soundness and principality of type inference for structural polymorphism

    Theorem Proving and Provers (TPP) Meeting 

     詳細を見る

    開催年月日: 2008年11月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  37. Proving OCaml's type system?

    Gallium-Moscova seminar 

     詳細を見る

    開催年月日: 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.

  38. Engineering does help: a parameterized proof of soundness for structural polymorphism with recursive types.

    TPP meeting 

     詳細を見る

    開催年月日: 2007年11月

    記述言語:日本語   会議種別:口頭発表(一般)  

    国名:日本国  

▼全件表示

科研費 5

  1. 物理的・確率的システムの検証を支える形式的基盤の構築

    研究課題/研究課題番号:22H00520  2022年4月 - 2026年3月

    科学研究費助成事業  基盤研究(A)

    Affeldt Reynald, J Garrigue, 勝股 審也, 溝口 佳寛, 中野 圭介, 才川 隆文

      詳細を見る

    担当区分:研究分担者 

    今日, コンピュータプログラムは, デジタル情報の操作やそのネットワークに加えて, 外界との相互作用を行うため, プログラムの検証には, 形式論理と離散数学だけでなく, 実解析や確率論や幾何学などの数学が必要となり, プログラムの様々な副作用の厳密な検証が困難になっている. その複雑さを抑えるためには, プログラムの意味論の基礎的な研究と, 高度な数学に一貫性のある形式表現を与える統合的な研究の双方が必要である. 本研究では, 定理証明支援系Coq上, 実解析, 連続確率, 剛体幾何を形式化し, モナドと等式推論に基づいて, 形式的基盤の構築とその評価を行う.

  2. 論理体系への翻訳によるプログラミング言語の型健全性の保証

    研究課題/研究課題番号:22K11902  2022年4月 - 2025年3月

    科学研究費助成事業  基盤研究(C)

    J Garrigue, 才川 隆文, Affeldt Reynald

      詳細を見る

    担当区分:研究代表者 

    配分額:4160000円 ( 直接経費:3200000円 、 間接経費:960000円 )

    正しく型付けされたプログラムが実行時にエラーを起さないという型健全性はプログラミング言語の重要な性質であり,その恩恵を受けるために型検査も健全でなければならない.しかし,それを形式的に証明することが煩雑な上に,次々に追加される機能への対応が困難である.
    この研究では,型健全性や型検査の健全性をプログラミング言語に対する直接的な証明ではなく,既に論理的健全性が確立されている論理体系への翻訳によって得ようとする.
    機能を追加するときに翻訳を拡張すれば十分で,翻訳先の定理証明支援系における自動的な型検査が証明になる.OCamlからCoqへの埋め込みを具体例としてこの方法を実現する.

  3. 確率的グラフィカルモデルの形式検証とその人工知能への応用

    研究課題/研究課題番号:18H03204  2018年4月 - 2021年3月

    科学研究費助成事業  基盤研究(B)

    Affeldt Reynald, 勝股 審也, 中野 圭介, J Garrigue

      詳細を見る

    担当区分:研究分担者  資金種別:競争的資金

    配分額:2321000円 ( 直接経費:1625000円 、 間接経費:696000円 )

    本研究では、確率とグラフを形式的に扱うように理論とツールを開発し、その応用実験も行った。定理証明支援系Coqを用いて、確率論及びより一般的なルベーグ積分の形式化を行った。木構造とグラフ構造に関する理論を開発し、そのデータ構造に基づくアルゴリズムの形式検証に応用した。以上の形式化を用いて、情報理論と人工知能の基礎の形式化を取り組んだ。確率的プログラムの形式検証のため、理論を開発し、定理証明支援系Coqを用いて確率を含むエフェクトを有するプログラムの形式検証基盤を開発した。本研究の成果の普及活動として、オープンソースソフトウェアを公開した。
    形式検証は一般的には基礎的な研究と見なされる。伝統的な数学分野の定理に対する形式検証実験のほうが注目を集めているからである。一方、IT製品の安全性評価に重要な、産業応用にも不可欠な技術である。例えば自動車のように、人命にかかわるシステムに人工知能を搭載するためには、その品質保証の技術が欠かせない。しかし、研究者の注目が薄い分野となっている。本研究では、確率的プログラミングでは初めて、正しさが証明されたソフトウェア実装とその形式化に必要な数学ライブラリが得られる。よって、人工知能の安全性・機械学習の形式検証・信頼性を保証するための基盤技術になりうる。

  4. 多機能型システムを持ったプログラミング言語のための型付き中間言語の設計

    研究課題/研究課題番号:16K00095  2016年4月 - 2019年3月

    科学研究費補助金  基盤研究(C)

    J Garrigue

      詳細を見る

    担当区分:研究代表者  資金種別:競争的資金

    配分額:3250000円 ( 直接経費:2500000円 、 間接経費:750000円 )

    関数型プログラミング言語OCamlの型検証器の堅牢性を高めるために様々な研究に取り組んだ。型検証器の理論的な基盤の整理と型検証器の見通しの改善を目指し、まずGADT(一般化代数的データ型)のパターンマッチングの網羅性という問題に理論的に答えを与え、OCamlに反映させた。他の開発者とともに、型検証器のモジュール性を高めた。型付中間言語が安全性に効果的になるための条件も検討した。また、プログラムの形式的検証の様々な研究を通じて、今後の中間言語の形式化を準備した。
    社会のあらゆる所でソフトウェアは我々の生活をサポートしている。娯楽や書類の作成から、飛行機の飛行制御システムや医療機器まで、応用は幅広いが、その全ての場面で安全性が求められる。型システムがプログラムの安全性の確保に効果的であり、型の表現力が高いほどの効果が現れる。しかし、型システムが複雑になると、型の整合性の確認を行う型検証器とその後の処理の正しさの担保が難しくなる。この研究はプログラミング言語処理系の型の正しさを保証することでソフトウェアの安全性の向上を目指す。

  5. ビッグデータ処理の形式検証に向けて

    研究課題/研究課題番号:15K12013  2015年4月 - 2018年3月

    Affeldt Reynald

      詳細を見る

    担当区分:研究分担者 

    インターネットに接続される機器の増加に伴い、蓄積されるデータが爆発的に増大している。これらの大規模なデータを解析し、活用しようという動きが、いわゆる「ビッグデータ」のもとで進んでいる。しかし、ビッグデータ処理に用いられるプログラムの信頼性について、十分に厳密な検討や検証がなされているとは言いがたい。本研究では、「簡潔データ構造」に着目し、そのアルゴリズム及び実装の安全な開発方法を提案し、評価を行った。具体的には、定理証明支援系Coqを用いて、簡潔データ構造の基本的なアルゴリズムを形式化し、その性質を検証してから、実用的なコードを出力できるようにした。

 

担当経験のある科目 (本学) 5

  1. 数学展望Ⅱ

    2020

  2. 数理科学展望III

    2012

  3. 数理解析・計算機数学III

    2012

  4. 現代数学への流れ

    2011

  5. 数理解析・計算機数学Ⅲ

    2011

担当経験のある科目 (本学以外) 3

  1. 関数型プログラミング入門

    2013年4月 - 2014年3月 筑波大学)

  2. 宣言型プログラム論

    2007年4月 - 2008年3月 筑波大学)

  3. 宣言型プログラム論

    2006年4月 - 2007年3月 筑波大学)

 

社会貢献活動 2

  1. NHK文化教室 数学の花畑

    2011年4月

     詳細を見る

    数学連続講義の1回

  2. NHK文化教室 数学の風に吹かれて

    2011年1月

     詳細を見る

    数学連続講義の1回

学術貢献活動 1

  1. International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2021) 国際学術貢献

    役割:パネル司会・セッションチェア等, 査読

    European Joint Conferences on Theory and Practice of Software  2021年3月

     詳細を見る

    種別:学会・研究会等