Advertisement

Type and Effect Systems

  • Flemming Nielson
  • Hanne Riis Nielson
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1710)

Abstract

The design and implementation of a correct system can benefit from employing static techniques for ensuring that the dynamic behaviour satisfies the specification. Many programming languages incorporate types for ensuring that certain operations are only applied to data of the appropriate form. A natural extension of type checking techniques is to enrich the types with annotations and effects that further describe intensional aspects of the dynamic behaviour.

Keywords

Polymorphic type systems effect annotations subeffecting and subtyping semantic correctness type inference algorithms syntactic soundness and completeness Analyses for control flow binding times side effects region structure communication structure 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    T. Amtoft, F. Nielson, and H. R. Nielson. Type and Effect Systems: Behaviours for Concurrency. Imperial College Press, 1999.Google Scholar
  2. 2.
    T. Amtoft, F. Nielson, and H.R. Nielson. Type and behaviour reconstruction for higher-order concurrent programs. Journal of Functional Programming, 7(3):321–347, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    T. Amtoft, F. Nielson, H.R. Nielson, and J. Ammann. Polymorphic subtyping for effect analysis: The dynamic semantics. In Analysis and Verification of Multiple-Agent Languages, volume 1192 of Lecture Notes in Computer Science, pages 172–206. Springer, 1997.Google Scholar
  4. 4.
    P. N. Benton. Strictness logic and polymorphic invariance. In Proc. Second International Symposium on Logical Foundations of Computer Science, volume 620 of Lecture Notes in Computer Science, pages 33–44. Springer, 1992.Google Scholar
  5. 5.
    P. N. Benton. Strictness properties of lazy algebraic datatypes. In Proc. WSA ‘93, volume 724 of Lecture Notes in Computer Science, pages 206–217. Springer, 1993.Google Scholar
  6. 6.
    L. Damas and R. Milner. Principal type-schemes for functional programs. In Proc. POPL ‘82, pages 207–212. ACM Press, 1982.Google Scholar
  7. 7.
    K.-F. Faxén. Optimizing lazy functional programs using flow inference. In Proc. SAS ‘95, volume 983 of Lecture Notes in Computer Science, pages 136–153. Springer, 1995.Google Scholar
  8. 8.
    K.-F. Faxén. Polyvariance, polymorphism, and flow analysis. In Proc. Analysis and Verification of Multiple-Agent Languages, volume 1192 of Lecture Notes in Computer Science, pages 260–278. Springer, 1997.Google Scholar
  9. 9.
    Y.-C. Fuh and P. Mishra. Polymorphic subtype inference: Closing the theory-practice gap. In Proc. TAPSOFT ‘89, volume 352 of Lecture Notes in Computer Science, pages 167–183. Springer, 1989.Google Scholar
  10. 10.
    Y.-C. Fuh and P. Mishra. Type inference with subtypes. Theoretical Computer Science, 73:155–175, 1990.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    N. Heintze. Control-flow analysis and type systems. In Proc. SAS ‘95, volume 983 of Lecture Notes in Computer Science, pages 189–206. Springer, 1995.Google Scholar
  12. 12.
    Nevin Heintze and Jon G. Riecke. The SLam calculus: Programming with Secrecy and Integrity. In Proc. POPL ‘98, pages 365–377. ACM Press, 1998.Google Scholar
  13. 13.
    F. Henglein and C. Mossin. Polymorphic binding-time analysis. In Proc. ESOP ‘94, volume 788 of Lecture Notes in Computer Science, pages 287–301. Springer, 1994.Google Scholar
  14. 14.
    T. P. Jensen. Strictness analysis in logical form. In Proc. FPCA ‘91, volume 523 of Lecture Notes in Computer Science, pages 352–366. Springer, 1991.Google Scholar
  15. 15.
    T. P. Jensen. Disjunctive strictness analysis. In Proc. LICS ‘92, pages 174–185, 1992.Google Scholar
  16. 16.
    M. P. Jones. A theory of qualified types. In Proc. ESOP ‘92, volume 582 of Lecture Notes in Computer Science, pages 287–306. Springer, 1992.Google Scholar
  17. 17.
    N. D. Jones and F. Nielson. Abstract Interpretation: a Semantics-Based Tool for Program Analysis. In Handbook of Logic in Computer Science volume 4. Oxford University Press, 1995.Google Scholar
  18. 18.
    P. Jouvelot. Semantic Parallelization: a practical exercise in abstract interpretation. In Proc. POPL ‘87, pages 39–48, 1987.Google Scholar
  19. 19.
    P. Jouvelot and D. K. Gifford. Reasoning about continuations with control effects. In Proc. PLDI ‘89, ACM SIGPLAN Notices, pages 218–226. ACM Press, 1989.Google Scholar
  20. 20.
    P. Jouvelot and D. K. Gifford. Algebraic reconstruction of types and effects. In Proc. POPL ‘91, pages 303–310. ACM Press, 1990.Google Scholar
  21. 21.
    J. M. Lucassen and D. K. Gifford. Polymorphic effect analysis. In Proc. POPL ‘88, pages 47–57. ACM Press, 1988.Google Scholar
  22. 22.
    R. Milner. A theory of type polymorphism in programming. Journal of Computer Systems, 17:348–375, 1978.zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    J. Mitchell. Type inference with simple subtypes. Journal of Functional Programming, 1(3):245–285, 1991.zbMATHMathSciNetCrossRefGoogle Scholar
  24. 24.
    F. Nielson. A formal type system for comparing partial evaluators. In D. Bjørner, A. P. Ershov, and N. D. Jones, editors, Proc. Partial Evaluation and Mixed Computation, pages 349–384. North Holland, 1988.Google Scholar
  25. 25.
    F. Nielson. The typed λ-calculus with firsrst-class processes. In Proc. PARLE‘89, volume 366 of Lecture Notes in Computer Science, pages 355–373. Springer, 1989.Google Scholar
  26. 26.
    F. Nielson and H. R. Nielson. Two-Level Functional Languages, volume 34 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.Google Scholar
  27. 27.
    F. Nielson and H. R. Nielson. From CML to process algebras. In Proc. CONCUR‘93, volume 715 of Lecture Notes in Computer Science, pages 493–508. Springer, 1993.Google Scholar
  28. 28.
    F. Nielson and H. R. Nielson. Layered predicates. In Proc. REX‘92 workshop on Semantics-foundations and applications, volume 666 of Lecture Notes in Computer Science, pages 425–456. Springer, 1993.Google Scholar
  29. 29.
    F. Nielson and H. R. Nielson. From CML to its process algebra. Theoretical Computer Science, 155:179–219, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  30. 30.
    F. Nielson, H. R. Nielson, and C. L. Hankin. Principles of Program Analysis. Springer, 1999.Google Scholar
  31. 31.
    F. Nielson, H.R. Nielson, and T. Amtoft. Polymorphic subtyping for effect analysis: The algorithm. In Analysis and Verification of Multiple-Agent Languages, volume 1192 of Lecture Notes in Computer Science, pages 207–243. Springer, 1997.Google Scholar
  32. 32.
    H. R. Nielson, T. Amtoft, and F. Nielson. Behaviour analysis and safety conditions: a case study in CML. In Proc. FASE ‘98, number 1382 in Lecture Notes in Computer Science, pages 255–269. Springer, 1998.Google Scholar
  33. 33.
    H. R. Nielson and F. Nielson. Higher-Order Concurrent Programs with Finite Communication Topology. In Proc. POPL ‘94. Springer, 1994.Google Scholar
  34. 34.
    H. R. Nielson and F. Nielson. Communication analysis for Concurrent ML. In F. Nielson, editor, ML with Concurrency, Monographs in Computer Science, pages 185–235. Springer, 1997.Google Scholar
  35. 35.
    H.R. Nielson, F. Nielson, and T. Amtoft. Polymorphic subtyping for effect analysis: The static semantics. In Analysis and Verification of Multiple-Agent Languages, volume 1192 of Lecture Notes in Computer Science, pages 141–171. Springer, 1997.Google Scholar
  36. 36.
    G. D. Plotkin. A structural approach to operational semantics. Technical Report FN-19, DAIMI, Aarhus University, Denmark, 1981.Google Scholar
  37. 37.
    G. S. Smith. Polymorphic inference with overloading and subtyping. In Proc. TAP-SOFT ‘93, volume 668 of Lecture Notes in Computer Science, pages 671–685. Springer, 1993.Google Scholar
  38. 38.
    G. S. Smith. Polymorphic type schemes for functional programs with overloading and subtyping. Science of Computer Programming, 23:197–226, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  39. 39.
    J.-P. Talpin and P. Jouvelot. The type and effect discipline. In Proc. LICS ‘92, pages 162–173, 1992.Google Scholar
  40. 40.
    J.-P. Talpin and P. Jouvelot. The type and effect discipline. Information and Computation, 111(2):245–296, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  41. 41.
    Y.-M. Tang. Control-Flow Analysis by Effect Systems and Abstract Interpretation. PhD thesis, Ecole des Mines de Paris, 1994.Google Scholar
  42. 42.
    M. Tofte. Type inference for polymorphic references. Information and Computation, 89:1–34, 1990.zbMATHCrossRefMathSciNetGoogle Scholar
  43. 43.
    M. T ofte and L. Birkedal. A region inference algorithm. ACM TOPLAS, 20(3):1–44, 1998.Google Scholar
  44. 44.
    M. Tofte and J.-P. Talpin. Implementing the call-by-value lambda-calculus using a stack of regions. In Proc. POPL ‘94, pages 188–201. ACM Press, 1994.Google Scholar
  45. 45.
    M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132:109–176, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  46. 46.
    M. Wand. Specifying the correctness of binding-time analysis. In Proc. POPL ‘93, pages 137–143, 1993.Google Scholar
  47. 47.
    R. Wilhelm. Global flow analysis and optimization in the MUG2 compiler generating system. In S. S. Muchnick and N. D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 5. Prentice Hall International, 1981.Google Scholar
  48. 48.
    A. K. Wright. Typing references by effect inference. In Proc. ESOP ‘92, volume 582 of Lecture Notes in Computer Science, pages 473–491. Springer, 1992.Google Scholar
  49. 49.
    A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115:38–94, 1994.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Flemming Nielson
    • 1
  • Hanne Riis Nielson
    • 1
  1. 1.Department of Computer ScienceAarhus UniversityDenmark

Personalised recommendations