Updated on 2022/03/25

写真a

 
GARRIGUE, Jacques
 
Organization
Graduate School of Mathematics Computational Mathematics Professor
Graduate School
Graduate School of Mathematics
Undergraduate School
School of Science Department of Mathematics
Title
Professor

Degree 1

  1. Doctor of Science ( 1995.3   The University of Tokyo ) 

Research Interests 1

  1. Functional programming languagesType theoryLambda-calculus

Research Areas 2

  1. Others / Others  / Software

  2. Others / Others  / Fundamental Informatics

Current Research Project and SDGs 3

  1. Mechanical proof of an advanced type system

  2. Formal verification of probabilistic graphical models

  3. Robust type checker for functional programming with a rich type system

Research History 4

  1. Nagoya University   Graduate School of Mathematics Computational Mathematics   Professor

    2018.8

  2. Nagoya University   Graduate School of Mathematics Computational Mathematics   Associate professor

    2007.4 - 2018.7

  3. Nagoya University   Graduate School of Mathematics   Assistant Professor

    2004.10 - 2007.3

  4. Reasearch Associate, Kyoto University RIMS

    1995.4 - 2004.9

      More details

    Country:Japan

Education 2

  1. Ecole Normale Superieure de Paris   Departement de Mathematiques et Informatique

    1990.9 - 1998.3

      More details

    Country: Japan

  2. The University of Tokyo   Graduate School, Division of Science   Department of Information Sciences

    1992.10 - 1995.3

      More details

    Country: Japan

Professional Memberships 3

  1. Japan Society for Software Science and Technology

  2. IPSJ

  3. ACM

Committee Memberships 2

  1. IPSJ SIG-PRO   Steering committee member  

    2016.4 - 2020.3   

      More details

    Committee type:Academic society

  2. Editorial committee of IPSJ SIGPRO   Editor  

    2007.4 - 2011.3   

Awards 1

  1. Takahashi Encouragement Prize

    2010.6   Japanese Society for Software Science and Technology  

     More details

    Country:Japan

 

Papers 33

  1. A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism Reviewed International coauthorship

    Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa

    Journal of Functional Programming   Vol. 31   2021.7

     More details

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

    DOI: 10.1017/S0956796821000137

    Other Link: https://www.math.nagoya-u.ac.jp/~garrigue/papers/

  2. Reasoning with Conditional Probabilities and Joint Distributions in Coq Reviewed

    AFFELDT Reynald, GARRIGUE Jacques, SAIKAWA Takafumi

    Computer Software   Vol. 37 ( 3 ) page: 79 - 95   2020.7

     More details

    Language:English   Publishing type:Research paper (scientific journal)   Publisher: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

  3. Formal adventures in convex and conical spaces Reviewed

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    Conference on Intelligent Computer Mathematics   Vol. 12236 LNAI   page: 23 - 38   2020.6

     More details

    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

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

    Affeldt R

    Journal of Automated Reasoning   Vol. 64 ( 6 ) page: 1123 - 1164   2020.1

     More details

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

    DOI: 10.1007/s10817-019-09538-8

    Web of Science

    Scopus

  5. Proving tree algorithms for succinct data structures Reviewed

    Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka

    International Conference on Interactive Theorem Proving (ITP 2019)   Vol. 10   page: 5:1--5:19   2019.9

     More details

    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

  6. Lightweight linearly-typed programming with lenses and monads Reviewed

    Imai Keigo, Garrigue Jacques

    Journal of Information Processing   Vol. 27 ( 0 ) page: 431-444 - 444   2019.5

     More details

    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

  7. Examples of Formal Proofs about Data Compression Reviewed

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    International Symposium on Information Theory and Its Applications     2018.10

     More details

    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

  8. Safe Low-level Code Generation in Coq Using Monomorphization and Monadification Reviewed

    Akira Tanaka, Reynald Affeldt, Jacques Garrigue

    Journal of Information Processing   Vol. 26   page: 54-72   2018.1

     More details

    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

  9. Safe low-level code generation in Coq using monomorphization and monadification Reviewed

    Akira Tanaka, Reynald Affeldt, Jacques Garrigue

    Journal of Information Processing   Vol. 26 ( 0 ) page: 54 - 72   2018.1

     More details

    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

  10. GADTs and Exhaustiveness: Looking for the Impossible Invited Reviewed

    Jacques Garrigue, Jacques Le Normand

    Electronic Proceedings in Theoretical Computer Science   ( 241 ) page: 23-35   2017.2

     More details

    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

  11. Des unites dans le typeur Reviewed

    Jacques Garrigue, Dara Ly

    Journées Francaises des Langages Applicatifs     page: 1-6   2017.1

     More details

    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.

  12. GADTs and exhaustiveness: Looking for the impossible Invited Reviewed

    Jacques Garrigue, Jacques Le Normand

    Electronic Proceedings in Theoretical Computer Science, EPTCS   Vol. 241 ( 241 ) page: 23 - 35   2017

     More details

    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

  13. Units in the type checker

    Garrigue J., Ly D.

    JFLA 2017 - Journees Francophones des Langages Applicatifs     page: 85 - 90   2017

     More details

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

    Scopus

  14. 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     page: 537-541   2016.10

     More details

    Language:English  

  15. Formal Verification of the rank Algorithm for Succinct Data Structures Reviewed

    Akira Tanaka, Reynald Affeldt, Jacques Garrigue

    Formal Methods and Software Engineering, Springer-Verlag LNCS   Vol. 10009   page: 243-260   2016.10

     More details

    Language:English  

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

  16. Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory Reviewed

    Reynald Affeldt, Jacques Garrigue

    6th Conference on Interactive Theorem Proving (ITP 2015), Springer LNCS   Vol. 9236   page: 17-33   2015.8

     More details

    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

  17. A Certified Implementation of ML with Structural Polymorphism and Recursive Types Reviewed

    Jacques Garrigue

    Mathematical Structures in Computer Science   Vol. 25 ( 4 ) page: 867-891   2015.4

     More details

    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

  18. Formalization of linear error codes using SSreflect

    Reynald Affeldt, Jacques Garrigue

    Math for industry   Vol. 61   page: 76-78   2015.3

     More details

    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.

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

    日本ソフトウェア科学会全国大会     page: PPL4-2   2014.9

     More details

    Authorship:Lead author   Language:Japanese  

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

  20. Ambivalent types for principal type inference with GADTs Reviewed

    Jacques Garrigue, Didier Remy

    11th Asian Symposium on Programming Languages and Systems     page: 300-315   2013.12

     More details

    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.

  21. Path resolution for recursive nested modules Reviewed

    Jacques Garrigue, Keiko Nakata

    Higher-Order and Symbolic Computation     2012.5

     More details

    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

  22. A Syntactic Type System for Recursive Modules Reviewed

    Hyonseung Im, Keiko Nakata, Jacques Garrigue and Sungwoo Park

    ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications     2011.10

     More details

    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

  23. A Certified Implementation of ML with Structural Polymorphism Reviewed

    Jacques Garrigue

    Proceedings of the 8th Asian Symposium on Programming Language and Systems.   Vol. LNCS ( 6461 ) page: 360-375   2010.11

     More details

    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.

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

    日本ソフトウェアか学会第26回大会講演論文集   Vol. 26   2009.9

     More details

    Authorship:Lead author   Language:Japanese  

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

  25. Path resolution for recursive nested modules is undecidable Reviewed

    Keiko Nakata, Jacques Garrigue

    9th International Workshop on Termination     page: 43-47   2007.6

     More details

    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.

  26. *Private rows: abstracting the unnamed Reviewed

    Jacques Garrigue

    4th Asian Symposium on Programming Languages and Systems   Vol. LNCS ( 4279 )   2006.11

     More details

    Authorship:Lead author   Language:English  

  27. *Recursive Modules for Programming Reviewed

    Keiko Nakata, Jacques Garrigue

    International Conference on Functional Programming   Vol. 11   2006.9

     More details

    Language:English  

  28. Recursive Object-Oriented Modules Reviewed

    Keiko Nakata, Akira Ito, Jacques Garrigue

    Workshop on Foundations of Object-Oriented Languages   Vol. 11   2005.1

     More details

    Language:English  

  29. *Relaxing the value restriction Reviewed

    Jacques Garrigue

    International Symposium on Functional and Logic Programming   Vol. LNCS ( 2998 )   2004.4

     More details

    Authorship:Lead author   Language:English  

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

    Jacques Garrigue

      Vol. 7   2004.3

     More details

    Authorship:Lead author   Language:English  

  31. Simple Type Inference for Structural Polymorphism Reviewed

    Jacques Garrigue

    9th Workshop on Foundations of Object-Oriented Languages   Vol. 9   2002.1

     More details

    Language:English  

  32. Code reuse through polymorphic variants Reviewed

    Jacques Garrigue

      Vol. 25   page: 93ー100   2000

     More details

    Authorship:Lead author   Language:English  

  33. Extending ML with semi-explicit higher order polymorphism Reviewed

    Jacques Garrigue, Didier Remy

    Information and Computation   Vol. 155   page: 134-171   1999

     More details

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

▼display all

Books 3

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

    Jacques Garrigue, editor( Role: Sole author)

    Springer  2014.11  ( ISBN:9783319127354

     More details

    Language:English

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

    Jacques Garrigue and Manuel Hermenegildo, editors( Role: Joint author)

    Springer LNCS  2008.3  ( ISBN:978-3-540-78968-0

     More details

    Language:English

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

    大堀 淳, ジャック ガリグ, 西村 進( Role: Joint author)

    岩波書店  1999 

     More details

    Language:Japanese

Presentations 29

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

    Jacques Garrigue, Takafumi Saikawa

    PPL 2022  2022.3.6 

     More details

    Event date: 2022.3

    Language:English   Presentation type:Poster presentation  

    Country:Japan  

  2. Formalizing quantum circuits with MathComp/Ssreflect

    Takafumi Saikawa, Jacques Garrigue

    PPL 2022  2022.3.7 

     More details

    Event date: 2022.3

    Language:English   Presentation type:Poster presentation  

    Country:Japan  

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

    Jacques Garrigue

    Theorem Proving and Provers 2021  2021.11.22 

     More details

    Event date: 2021.11

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

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

  4. Formalizing quantum circuits with MathComp/Ssreflect

    Takafumi Saikawa

    Theorem Proving and Provers 2021  2021.11.21 

     More details

    Event date: 2021.11

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

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

  5. Formalizing OCaml GADT typing in Coq International conference

    Jacques Garrigue, Xuanrui Qi

    ML Workshop 2021  2021.8.26  ACM SIGPLAN

     More details

    Event date: 2021.8

    Language:English   Presentation type:Oral presentation (general)  

    Venue:Online   Country:United States  

  6. Towards a Coq specification for Generalized Algebraic Datatypes in OCaml International conference

    Jacques Garrigue, Xuanrui Qi

    International Workshop on Coq for Programming Languages (CoqPL 2021)  2021.1.19  ACM SIGPLAN

     More details

    Event date: 2021.1

    Language:English   Presentation type:Oral presentation (general)  

    Venue:Online   Country:United States  

  7. Tracking injectivity and nominality beyond abstraction International conference

    Jacques Garrigue

    ML Family Workshop  2020.8.27  ACM SIGPLAN

     More details

    Event date: 2020.8

    Language:English   Presentation type:Oral presentation (general)  

    Venue:Online   Country:Korea, Republic of  

  8. Reasoning with Conditional Probabilities and Joint Distributions in Coq

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    JSSST Workshop on Programming and Programming Languages 

     More details

    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.

  9. Correctness of the LOUDS encoding of tree structures

    Jacques Garrigue

    Theorem Proving and Provers meeting 

     More details

    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.

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

    今井 敬吾, Jacques Garrigue

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

     More details

    Event date: 2018.10 - 2018.11

    Language:Japanese   Presentation type:Oral presentation (general)  

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

  11. Lightweight linearly-typed programming with lenses and monads

    Keigo Imai and Jacques Garrigue

    OCaml Users in Paris 

     More details

    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.

  12. Proving tree algorithms for succinct data structures

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

    JSSST National Meeting 

     More details

    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.

  13. 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 

     More details

    Event date: 2017.2

    Language:English   Presentation type:Oral presentation (general)  

    Scopus

  14. GADTs and exhaustiveness: looking for the impossible International conference

    Jacques Garrigue, Jacques Le Normand

    Workshop on ML 

     More details

    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.

  15. Type-level module aliases: independent and equal International conference

    Jacques Garrigue

    Jacques Garrigue 

     More details

    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.

  16. Formalization of Error-correcting Codes using SSReflect International conference

    Reynald Affeldt, Jacques Garrigue

    Coq Workshop 

     More details

    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.

  17. Runtime types in OCaml International conference

    Gregoire Henry, Jacques Garrigue

    OCaml 2013 

     More details

    Event date: 2013.9

    Language:English   Presentation type:Oral presentation (general)  

    Country:United States  

  18. On variance, injectivity, and abstraction International conference

    Jacques Garrigue

    OCaml 2013 

     More details

    Event date: 2013.9

    Language:English   Presentation type:Oral presentation (general)  

    Country:United States  

  19. Tracing ambiguity in GADT type inference International conference

    Jacques Garrigue, Didier Remy

    ACM-SIGPLAN Workshop on ML 

     More details

    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.

  20. Path resolution for nested recursive modules

    Jacques Garrigue, Keiko Nakata

    Dependable components seminar 

     More details

    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.

  21. Adding GADTs to OCaml: a direct approach International conference

    Jacques Garrigue, Jacques Le Normand

    ACM SIGPLAN Workshop on ML 

     More details

    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.

  22. Adding GADTs to OCaml: the direct approach

    Jacques Garrigue, Jacques Le Normand

    Gallium-Moscova seminar 

     More details

    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.

  23. First-class modules and composable signatures in Objective Caml3.12 International conference

    The 2010 ACM SIGPLAN Workshop on ML 

     More details

    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-

  24. A certified interpreter for a subset of OCaml

    Theorem Proving and Provers 2009 

     More details

    Event date: 2009.11

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

  25. Objective Camlがなぜバグを書かせないのか Invited

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

     More details

    Event date: 2009.9

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

    Country:Japan  

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

  26. A Certified Interpreter for ML with Structural Polymorphism International conference

    4th Informal ACM SIGPLAN Workshop on Mechanizing MetatheoryEdinburgh, Scotland 

     More details

    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.

  27. Soundness and principality of type inference for structural polymorphism

    Theorem Proving and Provers (TPP) Meeting 

     More details

    Event date: 2008.11

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

  28. Proving OCaml's type system?

    Gallium-Moscova seminar 

     More details

    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.

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

    TPP meeting 

     More details

    Event date: 2007.11

    Language:Japanese   Presentation type:Oral presentation (general)  

    Country:Japan  

▼display all

KAKENHI (Grants-in-Aid for Scientific Research) 3

  1. Formal verification of probabilistic graphical models and its application to artificial intelligence

    Grant number:18H03204  2018.4 - 2021.3

    基盤B

    Reynald Affeldt

      More details

    Authorship:Coinvestigator(s)  Grant type:Competitive

    Grant amount:\2321000 ( Direct Cost: \1625000 、 Indirect Cost:\696000 )

  2. Design of a typed intermediate language for a richly typed programming language

    Grant number:16K00095  2016.4 - 2019.3

    Grant-in-Aid for Scientific Research  Grant-in-Aid for Scientific Research(C)

    Garrigue Jacques

      More details

    Authorship:Principal investigator  Grant type:Competitive

    Grant amount:\3250000 ( Direct Cost: \2500000 、 Indirect Cost:\750000 )

    I did several researches to strengthen the robustness of the OCaml type checker. Aiming at improving the theoretical foundation and structure of the type checker, I first solved the question of the interaction between GADTs (generalized algebraic datatypes) and the exhaustiveness check of pattern matching, both theoretically and practically. I worked with other developers at making the type checker more modular. I studid the conditions for improving the safety of the language through a typed intermediate language. I also worked on several topics of program verification, which should help with the formalization of this typed intermediate language.

  3. Towards formal verification of big data processing

    Grant number:15K12013  2015.4 - 2018.3

    AFFELDT Reynald

      More details

    Authorship:Coinvestigator(s) 

    Data accumulate as the result of the increasing number of devices connected to the Internet. These so-called big data are the object of various analyses whose reliability is important. In this project, we focus on succinct data structures as an example of big data. We propose and evaluate an approach for their safe implementation. Concretely, we formalize and verify standard algorithms for succinct data structures using the Coq proof-assistant, and extend the latter so as to be able to extract safe programs that are usable in practice.

 

Teaching Experience (On-campus) 5

  1. Perspectives in Mathematics II

    2020

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

    2012

  3. Perspectives in Mathematical Sciences III

    2012

  4. Introduction to Concepts of Modern Mathematics

    2011

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

    2011

Teaching Experience (Off-campus) 3

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

    2013.4 - 2014.3 University of Tsukuba)

  2. 宣言型プログラム論

    2007.4 - 2008.3 University of Tsukuba)

  3. 宣言型プログラム論

    2006.4 - 2007.3 University of Tsukuba)

 

Social Contribution 2

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

    2011.4

     More details

    数学連続講義の1回

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

    2011.1

     More details

    数学連続講義の1回

Academic Activities 1

  1. International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2021) International contribution

    Role(s):Panel moderator, session chair, etc., Peer review

    European Joint Conferences on Theory and Practice of Software  2021.3

     More details

    Type:Academic society, research group, etc.