• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

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

Research Project

Project/Area Number 16K00095
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Research Field Software
Research InstitutionNagoya University

Principal Investigator

Garrigue Jacques  名古屋大学, 多元数理科学研究科, 教授 (80273530)

Research Collaborator Tanaka Kazunari  
Project Period (FY) 2016-04-01 – 2019-03-31
Project Status Completed (Fiscal Year 2018)
Budget Amount *help
¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000)
Fiscal Year 2018: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2017: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2016: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Keywords型システム / 中間言語 / 型検証 / プログラム検証 / 型健全性 / プログラミング言語処理系
Outline of Final Research Achievements

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.

Academic Significance and Societal Importance of the Research Achievements

社会のあらゆる所でソフトウェアは我々の生活をサポートしている。娯楽や書類の作成から、飛行機の飛行制御システムや医療機器まで、応用は幅広いが、その全ての場面で安全性が求められる。型システムがプログラムの安全性の確保に効果的であり、型の表現力が高いほどの効果が現れる。しかし、型システムが複雑になると、型の整合性の確認を行う型検証器とその後の処理の正しさの担保が難しくなる。この研究はプログラミング言語処理系の型の正しさを保証することでソフトウェアの安全性の向上を目指す。

Report

(4 results)
  • 2018 Annual Research Report   Final Research Report ( PDF )
  • 2017 Research-status Report
  • 2016 Research-status Report
  • Research Products

    (7 results)

All 2019 2018 2017 2016

All Journal Article (3 results) (of which Int'l Joint Research: 1 results,  Peer Reviewed: 3 results,  Open Access: 3 results,  Acknowledgement Compliant: 1 results) Presentation (4 results) (of which Int'l Joint Research: 1 results)

  • [Journal Article] Lightweight linearly-typed programming with lenses and monads2019

    • Author(s)
      Keigo Imai; Jacques Garrigue
    • Journal Title

      Journal of Information Processing

      Volume: 印刷中

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Examples of formal proofs about data compression2018

    • Author(s)
      Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa
    • Journal Title

      International Symposium on Information Theory and Its Applications, Singapore, October 28--31, 2018, IEICE/IEEE Xplore

      Volume: 1 Pages: 665-669

    • DOI

      10.23919/isita.2018.8664276

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] GADTs and Exhaustiveness: Looking for the Impossible2017

    • Author(s)
      Jacques Garrigue, Jacques Le Normand
    • Journal Title

      Electronic Proceedings in Theoretical Computer Science

      Volume: 241 Pages: 23-35

    • DOI

      10.4204/eptcs.241.2

    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
  • [Presentation] Reasoning with Conditional Probabilities and Joint Distributions in Coq2019

    • Author(s)
      Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
    • Organizer
      プログラミングおよびプログラミング言語ワークショップ
    • Related Report
      2018 Annual Research Report
  • [Presentation] Proving tree algorithms for succinct data structures2018

    • Author(s)
      Jacques Garrigue, Reynald Affeldt, Xuanrui Qi, and Kazunari Tanaka
    • Organizer
      日本ソフトウェア科学会
    • Related Report
      2018 Annual Research Report
  • [Presentation] レンズとモナドを用いた軽量な線形型付きプログラミング2018

    • Author(s)
      今井 敬吾, Jacques Garrigue
    • Organizer
      情報処理学会プログラミング研究発表会
    • Related Report
      2018 Annual Research Report
  • [Presentation] Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes2016

    • Author(s)
      Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
    • Organizer
      ISITA 2016
    • Place of Presentation
      Monterey, California
    • Year and Date
      2016-11-01
    • Related Report
      2016 Research-status Report
    • Int'l Joint Research

URL: 

Published: 2016-04-21   Modified: 2020-03-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi