Dependent type inference with interpolants

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Dependent type inference with interpolants

Full text

Pdf (471 KB)

Source

International Conference on Principles and Practice of Declarative Programming archive
Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming table of contents

Coimbra, Portugal

SESSION: Types table of contents

Pages 277-288

Year of Publication: 2009

ISBN:978-1-60558-568-0

Authors

Hiroshi Unno	Tohoku University, Sendai, Japan
Naoki Kobayashi	Tohoku University, Sendai, Japan

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
ACM: Association for Computing Machinery

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 11, Downloads (12 Months): 11, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1599410.1599445 What is a DOI?

ABSTRACT

We propose a novel type inference algorithm for a dependently-typed functional language. The novel features of our algorithm are: (i) it can iteratively refine dependent types with interpolants until the type inference succeeds or the program is found to be ill-typed, and (ii) in the latter case, it can generate a kind of counter-example as an explanation of why the program is ill-typed. We have implemented a prototype type inference system and tested it for several programs.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	T. Altenkirch, C. McBride, and J. McKinna. Why dependent types matter. Manuscript, available online, April 2005.
	2	L. Augustsson. Cayenne -- a language with dependent types. In ICFP '98, pages 239--250. ACM Press, 1998.
	3	T. Ball, R. Majumdar, T. Millstein, and S.K. Rajamani. Automatic predicate abstraction of C programs. In PLDI '01, pages 203--213. ACM Press, 2001.
	4	Y. Bertot and P. Casteran. Interactive Theorem Proving and Program Development. Springer-Verlag, 2004.
	5	D. Beyer, D. Zufferey, and R. Majumdar. CSIsat: Interpolation for LA+EUF (tool paper). In CAV '08, volume 5123 of Lecture Notes in Computer Science, pages 304--308, July 2008.
	6	R.S. Boyer and J.S. Moore. Proving theorems about LISP functions. Journal of the ACM, 22(1):129--144, 1975.
	7	A. Bundy. The automation of proof by mathematical induction. In Handbook of Automated Reasoning, volume I, chapter 13, pages 845--911. Elsevier Science, 2001.
	8	W.-N. Chin and S.-C. Khoo. Calculating sized types. In PEPM '00, pages 62--72. ACM Press, 1999.
	9	W.-N. Chin, S.-C. Khoo, and D.N. Xu. Extending sized type with collection analysis. In PEPM '03, pages 75--84. ACM Press, 2003.
	10	E.M. Clarke, O. Grumberg, and D.A. Peled. Model checking. MIT Press, Cambridge, MA, USA, 1999.
	11	P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL '77, pages 238--252. ACM Press, 1977.
	12	W. Craig. Linear reasoning. a new form of the Herbrand-Gentzen theorem. The Journal of Symbolic Logic, 22:250--268, September 1957.
	13	C. Flanagan. Hybrid type checking. In POPL '06, pages 245--256. ACM Press, 2006.
	14	S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In CAV '97, volume 1254 of Lecture Notes in Computer Science, pages 72--83. Springer-Verlag, June 1997.
	15	C. Haack and J.B. Wells. Type error slicing in implicitly typed higher-order languages. In ESOP '03, volume 2618 of Lecture Notes in Computer Science, pages 284--301. Springer-Verlag, April 2003.
	16	T.A. Henzinger, R. Jhala, R. Majumdar, and K.L. McMillan. Abstractions from proofs. In POPL '04, pages 232--244. ACM Press, 2004.
	17	T.A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL '02, pages 58--70. ACM Press, 2002.
	18	H. Hosoya and B.C. Pierce. How good is local type inference? Technical Report MS-CIS-99-17, University of Pennsylvania, June 1999.
	19	J. Hughes, L. Pareto, and A. Sabry. Proving the correctness of reactive systems using sized types. In POPL '96, pages 410--423. ACM Press, 1996.
	20	D. Kapur, R. Majumdar, and C.G. Zarba. Interpolation for data structures. In SIGSOFT '06/FSE-14, pages 105--116. ACM, 2006.
	21	K. Knowles and C. Flanagan. Type reconstruction for general refinement types. In ESOP '07, volume 4421 of Lecture Notes in Computer Science, pages 505--519. Springer-Verlag, March/April 2007.
	22	K.L. McMillan. An interpolating theorem prover. Theoretical Computer Science, 345(1):101--121, 2005.
	23	K.L. McMillan. Lazy abstraction with interpolants. In CAV '06, volume 4144 of Lecture Notes in Computer Science, pages 123--136. Springer-Verlag, August 2006.
	24	B.C. Pierce and D.N. Turner. Local type inference. In POPL '98, pages 252--265. ACM Press, 1998.
	25	P. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI '08. ACM Press, 2008.
	26	H. Unno and N. Kobayashi. On-demand refinement of dependent types. In FLOPS '08, volume 4989 of Lecture Notes in Computer Science, pages 81--96. Springer-Verlag, April 2008.
	27	H. Unno and N. Kobayashi. Dependent type inference with interpolants (Full version), June 2009. Available from http://www.kb.ecei.tohoku.ac.jp/~uhiro/.
	28	H. Xi and F. Pfenning. Eliminating array bound checking through dependent types. In PLDI '98, pages 249--257. ACM Press, 1998.
	29	H. Xi and F. Pfenning. Dependent types in practical programming. In POPL '99, pages 214--227. ACM Press, 1999.