Advertisement

Partiality, State and Dependent Types

  • Kasper Svendsen
  • Lars Birkedal
  • Aleksandar Nanevski
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6690)

Abstract

Partial type theories allow reasoning about recursively- defined computations using fixed-point induction. However, fixed-point induction is only sound for admissible types and not all types are admissible in sufficiently expressive dependent type theories.

Previous solutions have either introduced explicit admissibility conditions on the use of fixed points, or limited the underlying type theory. In this paper we propose a third approach, which supports Hoare-style partial correctness reasoning, without admissibility conditions, but at a tradeoff that one cannot reason equationally about effectful computations. The resulting system is still quite expressive and useful in practice, which we confirm by an implementation as an extension of Coq.

Keywords

Type Theory Partial Type Dependent Type Inductive Type Separation Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    The Coq Proof Assistant, http://coq.inria.fr/
  2. 2.
    Coq Reference Manual, Version 8.3Google Scholar
  3. 3.
    Abbott, M., Altenkirch, T., Ghani, N.: Representing nested inductive types using W-types. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 59–71. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  4. 4.
    Amadio, R.M.: Recursion over Realizability Structures. Information and Computation 91, 55–85 (1991)CrossRefzbMATHGoogle Scholar
  5. 5.
    Birkedal, L., Støvring, K., Thamsborg, J.: Realisability semantics of parametric polymorphism, general references and recursive types. Math. Struct. Comp. Sci. 20(4), 655–703 (2010)CrossRefzbMATHGoogle Scholar
  6. 6.
    Bjorner, D., Jones, C.B. (eds.): The Vienna Development Method: The Meta-Language. LNCS, vol. 61. Springer, Heidelberg (1978)zbMATHGoogle Scholar
  7. 7.
    Bove, A.: Simple General Recursion in Type Theory. Nordic Journal of Computing 8 (2000)Google Scholar
  8. 8.
    Capretta, V.: General Recursion via Coinductive Types. Logical Methods in Computer Science 1(2), 1–28 (2005)CrossRefzbMATHGoogle Scholar
  9. 9.
    Constable, R.L., Smith, S.F.: Partial Objects in Constructive Type Theory. In: Proceedings of Second IEEE Symposium on Logic in Computer Science (1987)Google Scholar
  10. 10.
    Crary, K.: Admissibility of Fixpoint Induction over Partial Types. In: Automated Deduction - CADE-15 (1998)Google Scholar
  11. 11.
    Dybjer, P.: Representing inductively defined sets by wellorderings in Martin-Löf’s type theory. Theor. Comput. Sci. 176(1-2), 329–335 (1997)CrossRefzbMATHGoogle Scholar
  12. 12.
    Gonthier, G., Mahboubi, A.: A Small Scale Reflection Extension for the Coq system. Technical report, INRIA (2007)Google Scholar
  13. 13.
    Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1, 271–281 (1972)CrossRefzbMATHGoogle Scholar
  14. 14.
    Jacobs, B.: Categorical Logic and Type Theory. Elsevier Science, Amsterdam (1999)zbMATHGoogle Scholar
  15. 15.
    Meyer, B.: Object-oriented software construction. Prentice Hall, Englewood Cliffs (1997)zbMATHGoogle Scholar
  16. 16.
    Moerdijk, I., Palmgren, E.: Wellfounded trees in categories. Annals of Pure and Applied Logic 104(1-3), 189–218 (2000)CrossRefzbMATHGoogle Scholar
  17. 17.
    Nanevski, A., Morrisett, G., Birkedal, L.: Hoare Type Theory, Polymorphism and Separation. Journal of Functional Programming 18(5-6), 865–911 (2008)CrossRefzbMATHGoogle Scholar
  18. 18.
    Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: Dependent Types for Imperative Programs. In: Proceedings of ICFP 2008, pp. 229–240 (2008)Google Scholar
  19. 19.
    Nanevski, A., Vafeiadis, V., Berdine, J.: Structuring the Verification of Heap-Manipulating Programs. In: Proceedings of POPL 2010 (2010)Google Scholar
  20. 20.
    O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  21. 21.
    Petersen, R.L., Birkedal, L., Nanevski, A., Morrisett, G.: A realizability model for impredicative hoare type theory. In: Gairing, M. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 337–352. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  22. 22.
    Reus, B.: Synthetic Domain Theory in Type Theory: Another Logic of Computable Functions. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  23. 23.
    Svendsen, K., Birkedal, L., Nanevski, A.: Partiality, State and Dependent Types. Technical report, IT University of Copenhagen (2011), http://www.itu.dk/people/kasv/ihtt-adm-tr.pdf

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Kasper Svendsen
    • 1
  • Lars Birkedal
    • 1
  • Aleksandar Nanevski
    • 2
  1. 1.IT University of CopenhagenDenmark
  2. 2.IMDEA SoftwareSpain

Personalised recommendations