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

2013 Fiscal Year Annual Research Report

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

Research Project

Project/Area Number 22700028
Research InstitutionNagoya University

Principal Investigator

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

Project Period (FY) 2010-04-01 – 2014-03-31
Keywords型推論 / アルゴリズムの証明 / モジュール / 交際情報交換
Research Abstract

この一年では、新たな型定義の形式化とその整合性のチェックを手がけた。しかし、定義される型が正則であることをチェックするアルゴリズムができたものの、その証明はまだ未完成である。この部分は今後もタリン工科大学の中田景子さんと協力して行う予定である。
それ以外に、OCamlの現在の実装に関する改善や拡張も続けている。前年度に導入したGADT(一般化代数的データ型)の実装の強化や理論的な裏付けを行った。特に、フランスのINRIAのDidier Remyと一緒に考えた型推論の主要性を損なわないGADTの型システムを完全に形式化・証明し、2013年のAPLASで発表した。十分に形式化されたので、今後はCoqでの実装への導入も考えたい。
もう一つの拡張はモジュールエイリアスの導入である。今まだは、OCamlで新しいモジュールを古いモジュールの別名として定義しても、型システムではモジュールの関係が分からなかった。そのせいで、型の等価性が不完全になったりした。また、効率の面でも、インターフェイスが無駄に大きくなったり、コンパイル時間にも影響していた。モジュールエイリアスの導入によって、そういう問題が解決できた。ちなみに、モジュールエイリアスの理論は中田景子さんと一緒に再帰モジュールのために作ったものであり、この先行研究がなければ理論的な難しさから実現しなかっただろう。こちらについては、部分的なCoqでの証明があるので、検証されたインタープリターでも導入を考える。

Current Status of Research Progress
Reason

25年度が最終年度であるため、記入しない。

Strategy for Future Research Activity

25年度が最終年度であるため、記入しない。

  • Research Products

    (5 results)

All 2014 2013 Other

All Journal Article (2 results) (of which Peer Reviewed: 2 results) Presentation (2 results) Remarks (1 results)

  • [Journal Article] A Certified Implementation of ML with Structural Polymorphism and Recursive Types2014

    • Author(s)
      Jacques Garrigue
    • Journal Title

      Mathematical Structures in Computer Science

      Volume: to appear Pages: to appear

    • Peer Reviewed
  • [Journal Article] Ambivalent types for principal type inference with GADTs2013

    • Author(s)
      Jacques Garrigue, Didier Remy
    • Journal Title

      APLAS 2013, Springer Verlag LNCS

      Volume: 2301 Pages: 257-272

    • DOI

      10.1007/978-3-319-03542-0_19

    • Peer Reviewed
  • [Presentation] On variance, injectivity, and abstraction2013

    • Author(s)
      Jacques Garrigue
    • Organizer
      OCaml Workshop
    • Place of Presentation
      Boston, USA
    • Year and Date
      20130924-20130924
  • [Presentation] Runtime types in OCaml2013

    • Author(s)
      Jacques Garrigue and Gregoire Henry
    • Organizer
      OCaml Workshop
    • Place of Presentation
      Boston, USA
    • Year and Date
      20130924-20130924
  • [Remarks] A Certified Implementation of ML

    • URL

      http://www.math.nagoya-u.ac.jp/~garrigue/papers/aplas2010.html

URL: 

Published: 2015-05-28  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi