Dependent types from counterexamples

Tachio Terauchi*

*この研究の対応する著者

研究成果

35 被引用数 (Scopus)

抄録

Motivated by recent research in abstract model checking, we present a new approach to inferring dependent types. Unlike many of the existing approaches, our approach does not rely on programmers to supply the candidate (or the correct) types for the recursive functions and instead does counterexample- guided refinement to automatically generate the set of candidate dependent types. The main idea is to extend the classical fixed-point type inference routine to return a counterexample if the program is found untypable with the current set of candidate types. Then, an interpolating theorem prover is used to validate the counterexample as a real type error or generate additional candidate dependent types to refute the spurious counterexample. The process is repeated until either a real type error is found or sufficient candidates are generated to prove the program typable. Our system makes non-trivial use of "linear" intersection types in the refinement phase. The paper presents the type inference system and reports on the experience with a prototype implementation that infers dependent types for a subset of the Ocaml language. The implementation infers dependent types containing predicates from the quantifier-free theory of linear arithmetic and equality with uninterpreted function symbols.

本文言語English
ホスト出版物のタイトルPOPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
ページ119-130
ページ数12
DOI
出版ステータスPublished - 2010 4 20
外部発表はい
イベント37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'10 - Madrid, Spain
継続期間: 2010 1 172010 1 23

出版物シリーズ

名前Conference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN(印刷版)0730-8566

Other

Other37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'10
国/地域Spain
CityMadrid
Period10/1/1710/1/23

ASJC Scopus subject areas

  • ソフトウェア

フィンガープリント

「Dependent types from counterexamples」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル