1. Abel, A., Coquand, T., Dybjer, P.: On the algebraic foundation of proof assistants for intuitionistic type theory. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol. 4989, pp. 3–13. Springer, Heidelberg (2008)

   Chapter  Google Scholar 

2. Abel, A., Coquand, T., Dybjer, P.: Verifying a semantic beta-eta-conversion test for Martin-Löf type theory. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol. 5133, pp. 29–56. Springer, Heidelberg (2008)

   Chapter  Google Scholar 

3. Agda wiki (2008),appserv.cs.chalmers.se/users/ulfn/wiki/agda.php

4. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Develpment. Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)

   Book MATH  Google Scholar 

5. Bove, A., Capretta, V.: Modelling general recursion in type theory. Mathematical Structures in Computer Science 15, 671–708 (2005)

   Article MathSciNet MATH  Google Scholar 

6. Constable, R.L., et al.: Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Englewood Cliffs (1986)

   Google Scholar 

7. Coquand, T.: An algorithm for testing conversion in type theory. In: Logical Frameworks, pp. 255–279. Cambridge University Press, Cambridge (1991)

   Chapter  Google Scholar 

8. Coquand, T., Kinoshita, Y., Nordström, B., Takeyama, M.: A simple type-theoretic language: Mini-tt. In: Levy, J.-J., Bertot, Y., Huet, G., Plotkin, G. (eds.) From Semantics to Computer Science: Essays in Honor of Gilles Kahn, pp. 139–164. Cambridge University Press, Cambridge (2008)

   Google Scholar 

9. Dybjer, P.: Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics. In: Logical Frameworks, pp. 280–306. Cambridge University Press, Cambridge (1991)

   Chapter  Google Scholar 

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

    Article MATH  Google Scholar 

11. Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic 65(2) (June 2000)

    Google Scholar 

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

13. Dybjer, P., Setzer, A.: Indexed induction-recursion. Journal of Logic and Algebraic Programming 66(1), 1–49 (2006)

    Article MathSciNet MATH  Google Scholar 

14. Girard, J.Y.: Une extension de l’interprétation de Gödel à l’analyse, et son application à l’elimination des coupures dans l’analyse et la théorie des types. In: Fenstad, J.E. (ed.) Proceedings of the Second Scandinavian Logic Symposium, pp. 63–92. North-Holland Publishing Company, Amsterdam (1971)

    Chapter  Google Scholar 

15. Gödel, K.: Über eine bisher noch nicht benutze erweitrung des finiten standpunktes. Dialectica 12 (1958)

    Google Scholar 

16. Hinze, R.: A new approach to generic functional programming. In: Proceedings of the 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts (January 2000)

    Google Scholar 

17. Jansson, P., Jeuring, J.: PolyP — a polytypic programming language extension. In: POPL 1997, pp. 470–482. ACM Press, New York (1997)

    Google Scholar 

18. Martin-Löf, P.: Hauptsatz for the Intuitionistic Theory of Iterated Inductive Definitions. In: Fenstad, J.E. (ed.) Proceedings of the Second Scandinavian Logic Symposium, pp. 179–216. North-Holland Publishing Company, Amsterdam (1971)

    Chapter  Google Scholar 

19. Martin-Löf, P.: An Intuitionistic Theory of Types: Predicative Part. In: Rose, H.E., Shepherdson, J.C. (eds.) Logic Colloquium 1973, pp. 73–118. North-Holland Publishing Company, Amsterdam (1975)

    Google Scholar 

20. 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)

    Google Scholar 

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

    Google Scholar 

22. McBride, C.: Epigram: Practical programming with dependent types. In: Vene, V., Uustalu, T. (eds.) AFP 2004. LNCS, vol. 3622, pp. 130–170. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

23. Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML. MIT Press, Cambridge (1997)

    Google Scholar 

24. Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin-Löf’s Type Theory. An Introduction. Oxford University Press, Oxford (1990)

    MATH  Google Scholar 

25. Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden (September 2007)

    Google Scholar 

26. Peyton Jones, S. (ed.): Haskell 98 Language and Libraries The Revised Report. Cambridge University Press, Cambridge (2003)

    MATH  Google Scholar 

27. Peyton Jones, S., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. In: ICFP 2006: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, pp. 50–61. ACM Press, New York (2006)

    Chapter  Google Scholar 

28. Pfenning, F., Xi, H.: Dependent Types in practical programming. In: Proc. 26th ACM Symp. on Principles of Prog. Lang., pp. 214–227 (1999)

    Google Scholar 

29. Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci. 5(3), 225–255 (1977)

    Article MathSciNet  Google Scholar 

30. Scott, D.: Constructive validity. In: Symposium on Automatic Demonstration. Lecture Notes in Mathematics, vol. 125, pp. 237–275. Springer, Berlin (1970)

    Chapter  Google Scholar 

31. Taha, W., Sheard, T.: Metaml and multi-stage programming with explicit annotations. Theor. Comput. Sci. 248(1-2), 211–242 (2000)

    Article MATH  Google Scholar 

32. The Coq development team. The Coq proof assistant (2008),coq.inria.fr/

33. Thompson, S.: Type Theory and Functional Programming. Addison-Wesley, Reading (1991)

    MATH  Google Scholar 

34. Wahlstedt, D.: Dependent Type Theory with Parameterized First-Order Data Types and Well-Founded Recursion. PhD thesis, Chalmers University of Technology (2007) ISBN 978-91-7291-979-2

    Google Scholar 

Download references