Automation for Dependently Typed Functional Programming

• Autorzy: Wilson S. , Fleuriot J. , Smaill A.
• Języki publikacji: EN

Abstrakty

EN

Writing dependently typed functional programs that capture non-trivial program properties is difficult in current systems due to lack of proof automation. We identify proof patterns that occur when programming with dependent types and detail how automating such patterns allow us to work more comfortably with types that capture, for example, membership, ordering and nonlinear arithmetic properties. We describe the role of the rippling heuristic, both for inductive and non-inductive proofs, and generalisation in providing such automation. We then discuss an implementation of our ideas in Coq with practical examples of dependently typed programs, that capture useful program properties, which can be verified automatically. We demonstrate that our proof automation is generic in that it can provide support for working with theorems involving user-defined functions and inductive data types.

Słowa kluczowe

EN

dependent types; rippling; generalisation; automated theorem proving; Coq

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2010
• Tom: Vol. 102, nr 2
• Strony: 209--228
• Opis fizyczny: Bibliogr. 30 poz., tab.

Twórcy

autor

Wilson S.

autor

Fleuriot J.

autor

Smaill A.

• School of Informatics, The University of Edinburgh, Informatics Forum, 10 Crichton Street, Edinburgh EH8 9AB, United Kingdom,

Bibliografia

• [1] Adams, A. A., Dennis, L. A.: Rippling in PVS, Proc. of 1st Int. Workshop on Design and Application of Strategies/Tactics in Higher Order Logics, STRATA 2003 (M. Archer, B. Di Vito, C. Mu˜noz, Eds.), Technical report CP-2003-212448, NASA, 2003, 84-90.
• [2] Aderhold, M.: Improvements in formula generalization., Proc. of 21st Int. Conf. on Automated Deduction, CADE-21 (Bremen, July 2007) (F. Pfenning, Ed.), Lect. Notes in Artif. Intell., 4603, Springer-Verlag, 2007, 231-246.
• [3] Aubin, R.: Mechanizing Structural Induction, PhD thesis, University of Edinburgh, 1976.
• [4] Augustsson, L.: Cayenne-a language with dependent types, Proc. of 3rd ACM SIGPLAN Int. Conf. On Functional Programming, ICFP '98 (Baltimore, MD, Sept. 1998), ACM Press, 1998, 239-250.
• [5] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science, Springer-Verlag, 2004.
• [6] Boyer, R. S., Moore, J. S.: A Computational Logic, Academic Press, 1979.
• [7] Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-Level Guidance for Mathematical Reasoning, Cambridge University Press, 2005.
• [8] Bundy, A., van Harmelen, F., Horn, C., Smaill, A.: The Oyster-Clam system, Proc. of 10th Int. Conf. On Automated Deduction, CADE-10 (Kaiserslautern, July 1990) (M. Stickel, Ed.), Lect. Notes in Artif. Intell., 449, Springer-Verlag, 1990, 647-648.
• [9] Burton, F. W.: An efficient functional implementation of FIFO queues, Information Processing Letters, 14(5), 1982, 205-206.
• [10] Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs, Proc. Of 5th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP '00, Montréal, Sept. 2000), ACM Press, 2000, 268-279.
• [11] Constable, R. L., Allen, S. F., Bromley, H. M., Cleaveland, W. R., Cremer, J. F., Harper, R. W., Howe, D. J., Knoblock, T. B., Mendler, N. P., Panangaden, P., Sasaki, J. T., Smith, S. F.: Implementing Mathematics with the Nuprl Development System, Prentice-Hall, 1986.
• [12] Coquand, C.: The AGDA proof system homepage, 1998, http://www.cs.chalmers.se/~catarina/agda/.
• [13] Cui, S., Donnelly, K., Xi, H.: ATS: a language that combines programming with theorem proving, Proc. Of 5th Int. Workshop on Frontiers of Combining Systems, FroCoS 2005 (Vienna, Sept. 2005) (B. Gramlich, Ed.), Lect. Notes in Artif. Intell., 3717, Springer-Verlag, 2005, 310-320.
• [14] Delahaye, D.: A tactic language for the system Coq, Proc. of 7th Int. Conf. on Logic for Programming and Automated Reasoning, LPAR 2000 (Reunion Island, Nov. 2000) (M. Parigot, A. Voronkov, Eds.), Lect. Notes in Artif. Intell., 1955, Springer-Verlag, 2000, 85-95.
• [15] Dennis, L. A., Green, I., Smaill, A.: Embeddings as a higher-order representation of annotations for rippling, Technical report NOTTCS-WP-2005-1, School of CS and IT, University of Nottingham, 2005.
• [16] Dixon, L.: A Proof Planning Framework for Isabelle, PhD thesis, University of Edinburgh, 2005.
• [17] Gronski, J., Knowles, K., Tomb, A., Freund, S. N., Flanagan, C.: Sage: hybrid checking for flexible specifications, Proc. of 7th ACM SIGPLAN Scheme and Functional Programming Workshop, Scheme 2006 (Portland, OR, Sept. 2006) (R. Findler, Ed.), Technical report TR2006-06, Dept. of Computer Science, University of Chicago, 2006, 93-104.
• [18] Ireland, A., Bundy, A.: Productive use of failure in inductive proof, Journal of Automated Reasoning, 16(1-2), 1996, 79-111.
• [19] Kammüller, F.: Modular reasoning in Isabelle, Proc. of 17th Int. Conf. on Automated Deduction, CADE-17 (Pittsburgh, PA, June 2000) (D. A. McAllester, Ed.), Lect. Notes in Artif. Intell., 1831, Springer-Verlag, 2000, 99-114.
• [20] Martin-Löf, P.: A theory of types, Manuscript, 1971.
• [21] The Coq development team: The Coq Proof Assistant Reference Manual, version 8.1. LogiCal Project, 2006
• [22] McBride, C., McKinna, J.: The view from the left, Journal of Functional Programing, 14(1), 2004, 69-111.
• [23] Nipkow, T., Paulson, L. C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, Lect. Notes in Comput. Sci., 2283, Springer-Verlag, 2002.
• [24] Owre, S., Shankar, N., Rushby, J. M., Stringer-Calvert, D. W.: PVS System Guide, Computer Science Laboratory, SRI International, Menlo Park, CA, 1999.
• [25] Pientka, B., Kreitz, C.: Instantiation of existentially quantified variables in inductive specification proofs, Proc. of Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC' 98 (Plattsburgh, NY, Sept. 1998) (J. Calmet, J. A. Plaza, Eds.), Lect. Notes in Comput. Sci., 1476, Springer-Verlag, 1998, 247-258.
• [26] Smaill, A., Green, I.: Higher-order annotated terms for proof search, Proc. of 9th Int. Conf. on Theorem Proving in Higher Order Logics, TPHOLs '96 (Turku, Aug. 1996) (J. von Wright, J. Grundy, J. Harrison, Eds.), Lect. Notes in Comput. Sci., 1125, Springer-Verlag, 1996, 399-413.
• [27] Sozeau, M.: Program-ing finger trees in Coq, Proc. of 12th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP '07 (Freiburg, Oct. 2007), ACM Press, 2007, 13-24.
• [28] Sozeau, M.: Subset coercions in Coq, Revised Selected Papers from Int. Workshop on Types for Proofs and Program TYPES 2006 (Nottingham, Apr. 2006) (T. Altenkirch, C. McBride, Eds.), Lect. Notes in Comput. Sci., 4502, Springer-Verlag, 2007, 237-252.
• [29] Werner, B.: Méta-théorie du Calcul des Constructions Inductives, PhD Thesis, Université Paris 7, 1994.
• [30] Xi, H., Pfenning, F.: Dependent types in practical programming, Proc. of 26th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL '99 (San Antonio, TX, Jan. 1999), ACM Press, 1999, 214-227.