Dependent types from counterexamples

Research output: Chapter in Book/Report/Conference proceedingConference contribution

29 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationPOPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Pages119-130
Number of pages12
DOIs
Publication statusPublished - 2010
Externally publishedYes
Event37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'10 - Madrid, Spain
Duration: 2010 Jan 172010 Jan 23

Other

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

Fingerprint

Recursive functions
Model checking

Keywords

  • Counterexamples
  • Dependent types
  • Interpolation
  • Intersection types
  • Type inference

ASJC Scopus subject areas

  • Software

Cite this

Terauchi, T. (2010). Dependent types from counterexamples. In POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (pp. 119-130) https://doi.org/10.1145/1706299.1706315

Dependent types from counterexamples. / Terauchi, Tachio.

POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2010. p. 119-130.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Terauchi, T 2010, Dependent types from counterexamples. in POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 119-130, 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'10, Madrid, Spain, 10/1/17. https://doi.org/10.1145/1706299.1706315
Terauchi T. Dependent types from counterexamples. In POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2010. p. 119-130 https://doi.org/10.1145/1706299.1706315
Terauchi, Tachio. / Dependent types from counterexamples. POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2010. pp. 119-130
@inproceedings{398991ab2ab24bada4945b83eea6796a,
title = "Dependent types from counterexamples",
abstract = "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.",
keywords = "Counterexamples, Dependent types, Interpolation, Intersection types, Type inference",
author = "Tachio Terauchi",
year = "2010",
doi = "10.1145/1706299.1706315",
language = "English",
isbn = "9781605584799",
pages = "119--130",
booktitle = "POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",

}

TY - GEN

T1 - Dependent types from counterexamples

AU - Terauchi, Tachio

PY - 2010

Y1 - 2010

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

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

KW - Counterexamples

KW - Dependent types

KW - Interpolation

KW - Intersection types

KW - Type inference

UR - http://www.scopus.com/inward/record.url?scp=77950888674&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=77950888674&partnerID=8YFLogxK

U2 - 10.1145/1706299.1706315

DO - 10.1145/1706299.1706315

M3 - Conference contribution

AN - SCOPUS:77950888674

SN - 9781605584799

SP - 119

EP - 130

BT - POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

ER -