Combining Testing and Proving in Dependent Type Theory

1. Augustsson, L.: Cayenne: a Language with Dependent Types. In: Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP 1998). ACM SIGPLAN Notices, vol. 34(1), pp. 239–250 (1998)

   Google Scholar 

2. Backhouse, R., Jansson, P., Jeuring, J., Meertens, L.: Generic Programming – An Introduction. In: Swierstra, S.D., Oliveira, J.N. (eds.) AFP 1998. LNCS, vol. 1608, pp. 28–115. Springer, Heidelberg (1999)

   Chapter  Google Scholar 

3. Bove, A.: General Recursion in Type Theory. PhD thesis. Chalmers University of Technology (2002)

   Google Scholar 

4. Carlsson, M., Hallgren, T.: Fudgets - Purely Functional Processes with applications to Graphical User Interfaces. PhD thesis. Chalmers University of Technology (1998)

   Google Scholar 

5. Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of the ACM Sigplan International Conference on Functional Programming (ICFP 2000), vol. 35.9, pp. 18–22. ACM Press, New York (2000)

   Google Scholar 

6. Claessen, K., Hughes, J.: QuickCheck: Automatic Specification-Based Testing: http: http://www.cs.chalmers.se/~rjmh/QuickCheck/

7. Coquand, C.: Agda, available from http://www.cs.chalmers.se/~catarina/agda

8. Coquand, T.: Pattern Matching with Dependent Types. In: Nordström, B., Petersson, K., Plotkin, G. (eds.) Proceedings of The 1992 Workshop on Types for Proofs and Programs, Båstad, pp. 71–84 (1992)

   Google Scholar 

9. Coquand, T.: Structured Type Theory. draft (1999), available from http://www.cs.chalmers.se/~coquand/type.html

10. Dybjer, P.: Inductive Families. Formal Aspects of Computing 6, 440–465 (1994)

    Article  MATH  Google Scholar 

11. Dybjer, P., Setzer, A.: A finite axiomatization of inductive-recursive definitions. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 129–146. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

12. Dybjer, P., Setzer, A.: Indexed Induction-Recursion. In: Kahle, R., Schroeder-Heister, P., Stärk, R.F. (eds.) PTCS 2001. LNCS, vol. 2183, pp. 93–113. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

13. Hallgren, T.: Alfa, available from http://www.cs.chalmers.se/~hallgren/Alfa

14. Hayashi, S., Nakano, H.: PX, a Computational Logic. The MIT Press, Cambridge (1988)

    Google Scholar 

15. Hayashi, S., Sumitomo, R., Shii, K.-i.: Towards Animation of Proofs - testing proofs by examples. Theoretical Computer Science 272, 177–195 (2002)

    Article  MATH  MathSciNet  Google Scholar 

16. Martin-Löf, P.: Constructive Mathematics and Computer Programming. In: Logic, Methodology and Philosophy of Science, VI, 1979, pp. 153–175. North-Holland, Amsterdam (1982)

    Chapter  Google Scholar 

17. Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis (1984)

    Google Scholar 

18. Okasaki, C.: An Overview of Edison. In: Haskell Workshop, September 2000, pp. 34–54 (2000)

    Google Scholar 

19. Parent, C.: A collection of examples using the Program tactic, available from http://pauillac.inria.fr/coq/contribs-eng.html

20. Programatica: Integrating Programming, Properties, and Validation, http://www.cse.ogi.edu/PacSoft/projects/programatica/

21. Rabhi, F.A., Lapalme, G.: Algorithms: a functional programming approach. Addison-Wesley Press, Reading (1999)

    Google Scholar 

22. Wahlstedt, D.: Detecting termination using size-change in parameter values. Master thesis. Chalmers University of Technology (2000)

    Google Scholar 

23. Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proceedings of the 26th ACM SIGPLAN-SIGACT on Principles of programming languages, pp. 214–227. ACM Press, New York (1999)

    Chapter  Google Scholar 

Download references