link.springer.com

Monads and Effects

  • ️Tue Jan 01 2002

Research partially supported by MURST and ESPRIT WG APPSEM.

References

  1. A. W. Appel. Compiling with Continuations. Cambridge University Press, 1992.

    Google Scholar 

  2. P. N. Benton, G. M. Bierman, and V. C. V. de Paiva. Computational types from a logical perspective. Journal of Functional Programming, 8(2):177–193, March 1998. Preliminary version appeared as Technical Report 365, University of Cambridge Computer Laboratory, May 1995.

    Google Scholar 

  3. P. N. Benton. Strictness Analysis of Lazy Functional Programs. PhD thesis, Computer Laboratory, University of Cambridge, December 1992.

    Google Scholar 

  4. A. Banerjee, N. Heintze, and J. G. Reicke. Region analysis and the polymorphic lambda calculus. In Fourteenth IEEE Symposium on Logic and Computer Science, 1999.

    Google Scholar 

  5. G. Barthe, J. Hatcliff, and P. Thiemann. Monadic type systems: Pure type systems for impure settings. In Proceedings of the Second HOOTS Workshop, Stanford University, Palo Alto, CA. December, 1997, Electronic Notes in Theoretical Computer Science. Elsevier, February 1998.

    Google Scholar 

  6. N. Benton and A. Kennedy. Monads, effects and transformations. In Third International Workshop on Higher Order Operational Techniques in Semantics (HOOTS), Paris, volume 26 of Electronic Notes in Theoretical Computer Science. Elsevier, September 1999.

    Google Scholar 

  7. N. Benton and A. Kennedy. Exceptional syntax. Journal of Functional Programming, 11(4):395–410, July 2001.

    Google Scholar 

  8. N. Benton, A. Kennedy, and G. Russell. Compiling Standard ML to Java bytecodes. In 3rd ACM SIGPLAN Conference on Functional Programming, September 1998.

    Google Scholar 

  9. G. L. Burn and D. Le Metayer. Proving the correctness of compiler optimisations based on a global program analysis. Technical Report Doc 92/20, Department of Computing, Imperial College, London, 1992.

    Google Scholar 

  10. P. Buneman, S. Naqvi, V. Tannen, and L. Wong. Principles of programming with complex objects and collection types. Theoretical Computer Science, 149(1), 1995.

    Google Scholar 

  11. F. Borceux. Handbook of Categorial Algebra. Cambridge University Press, 1994.

    Google Scholar 

  12. Erik Barendsen and Sjaak Smetsers. Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science, pages 579–612, 1996.

    Google Scholar 

  13. W. Burge. Recursive Programming Techniques. Addison-Wesley Publishing Company, Reading, Mass., 1975.

    MATH  Google Scholar 

  14. M. Barr and C. Wells. Toposes, Triples and Theories. Springer, 1985.

    Google Scholar 

  15. R. Cartwright and M. Felleisen. Extensible denotational language specifications. In Theoretical Aspects of Computer Software, volume 789 of LNCS. Springer, 1994.

    Google Scholar 

  16. C. Calcagno, S. Helsen, and P. Thiemann. Syntactic type soundness results for the region calculus. Information and Computation, to appear 200x.

    Google Scholar 

  17. P. Cenciarelli and E. Moggi. A syntactic approach to modularity in denotational semantics. In CTCS 1993, 1993. CWI Tech. Report.

    Google Scholar 

  18. H. B. Curry. The elimination theorem when modality is present. Journal of Symbolic Logic, 17(4):249–265, January 1957.

    Google Scholar 

  19. O. Danvy and A. Filinski. Representing control: A study of the CPS transformation. Mathematical Structures in Computer Science, 2, 1992.

    Google Scholar 

  20. O. Danvy and J. Hatcliff. CPS transformation after strictness analysis. ACM Letters on Programming Languages and Systems, 1(3), 1993.

    Google Scholar 

  21. S. dal Zilio and A. Gordon. Region analysis and a π-calculus with groups. In 25th International Symposium on Mathematical Foundations of Computer Science, August 2000.

    Google Scholar 

  22. A. Filinski. Representing layered monads. In POPL’99. ACM Press, 1999.

    Google Scholar 

  23. M. Fairtlough and M. Mendler. An intuitionistic modal logic with applications to the formal verification of hardware. In Proceedings of Computer Science Logic 1994, volume 933 of Lecture Notes in Computer Science. Springer-Verlag, 1995.

    Chapter  Google Scholar 

  24. C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The essence of compiling with continuations. In Proceedings of the 1993 Conference on Programming Language Design and Implementation. ACM, 1993.

    Google Scholar 

  25. D. K. Gifford, P. Jouvelot, J. M. Lucassen, and M. A. Sheldon. FX-87 reference manual. Technical Report MIT/LCS/TR-407, MIT Laboratory for Computer Science, 1987.

    Google Scholar 

  26. D.K. Gifford and J.M. Lucassen. Integrating functional and imperative programming. In ACM Conference on Lisp and Functional Programming. ACM Press, 1986.

    Google Scholar 

  27. J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Number 7 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

    Google Scholar 

  28. M.J.C. Gordon. Denotational Description of Programming Languages. Springer, 1979.

    Google Scholar 

  29. J. Gustavsson and D. Sands. A foundation for space-safe transformations of call-by-need programs. In A. D. Gordon and A. M. Pitts, editors, The Third International Workshop on Higher Order Operational Techniques in Semantics, volume 26 of Electronic Notes in Theoretical Computer Science. Elsevier, 1999.

    Google Scholar 

  30. J. Hatcliff and O. Danvy. A generic account of continuation-passing styles. In Proceedings of the 21st Annual Symposium on Principles of Programming Languages. ACM, January 1994.

    Google Scholar 

  31. Graham Hutton and Erik Meijer. Monadic parsing in Haskell. Journal of Functional Programming, 8(4):437–444, July 1998.

    Google Scholar 

  32. D. J. Howe. Proving congruence of bisimulation in functional programming languages. Information and Computation, 124(2):103–112, February 1996.

    Google Scholar 

  33. P. Hudak. Modular domain specific languages and tools. In Fifth International Conference on Software Reuse, pages 134–142, Victoria, Canada, June 1998.

    Google Scholar 

  34. John Hughes. Restricted Datatypes in Haskell. In Third Haskell Workshop. Utrecht University technical report, 1999.

    Google Scholar 

  35. Bart Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, 1999.

    Google Scholar 

  36. Simon Peyton Jones, John Hughes, (editors), Lennart Augustsson, Dave Barton, Brian Boutel, Warren Burton, Joseph Fasel, Kevin Hammond, Ralf Hinze, Paul Hudak, Thomas Johnsson, Mark Jones, John Launchbury, Erik Meijer, John Peterson, Alastair Reid, Colin Runciman, and Philip Wadler. Report on the Programming Language Haskell 98, a Non-strict, Purely Functional Language. Available from http://haskell.org, February 1999.

  37. Simon Peyton Jones. Explicit quantification in Haskell. http://research.microsoft.com/users/simonpj/Haskell/quantification.html.

  38. Mark P Jones, Alastair Reid, the Yale Haskell Group, the Oregon Graduate Institute of Science, and Technology. The Hugs 98 user manual. Available from http://haskell.org/hugs, 1994-1999.

  39. Simon Peyton Jones and Philip Wadler. Imperative functional programming. In 20’th Symposium on Principles of Programming Languages, Charlotte, North Carolina, January 1993. ACM Press.

    Google Scholar 

  40. D. Kranz, R. Kelsey, J. Rees, P. Hudak, J. Philbin, and N. Adams. Orbit: An optimizing compiler for Scheme. In Proceedings of the ACM SIGPLAN Symposium on Compiler Construction, SIGPLAN Notices, pages 219–233, 1986.

    Google Scholar 

  41. D. King and J. Launchbury. Structuring depth-first search algorithms in Haskell. In Conf. Record 22nd Symp. on Principles of Programming Languages, pages 344–354, San Francisco, California, 1995. ACM.

    Google Scholar 

  42. P.B. Levy. Call-by-push-value: a subsuming paradigm (extended abstract). In Typed Lambda-Calculi and Applications, volume 1581 of LNCS. Springer, 1999.

    Chapter  Google Scholar 

  43. S. Liang and P. Hudak. Modular denotational semantics for compiler construction. In ESOP’96, volume 1058 of LNCS. Springer, 1996.

    Google Scholar 

  44. S. Liang, P. Hudak, and M. Jones. Monad transformers and modular interpreters. In POPL’95. ACM Press, 1995.

    Google Scholar 

  45. J. Launchbury and S. Peyton Jones. Lazy functional state threads. In Proceedings of the 1994 SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 1994.

    Google Scholar 

  46. J. Launchbury and A. Sabry. Monadic state: Axiomatisation and type safety. In Proceedings of the International Conference on Functional Programming. ACM, 1997.

    Google Scholar 

  47. X. Leroy and P. Weis. Polymorphic type inference and assignment. In Proceedings of the 1991 ACM Conference on Principles of Programming Languages. ACM, 1991.

    Google Scholar 

  48. E. Manes. Algebraic Theories. Graduate Texts in Mathematics. Springer, 1976.

    Google Scholar 

  49. E Manes. Implementing collection classes with monads. Mathematical Structures in Computer Science, 8(3), 1998.

    Google Scholar 

  50. Y. Minamide. A functional represention of data structures with a hole. In Proceedings of the 25rd Symposium on Principles of Programming Languages, 1998.

    Google Scholar 

  51. Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In Conference Record of the 23rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St. Petersburg, Florida. ACM, January 1996.

    Google Scholar 

  52. E. Moggi. Computational lambda-calculus and monads. In Proceedings of the 4th Annual Symposium on Logic in Computer Science, Asiloomar, CA, pages 14–23, 1989.

    Google Scholar 

  53. E. Moggi. Notions of computation and monads. Information and Computation, 93(1), 1991.

    Google Scholar 

  54. E. Moggi. A semantics for evaluation logic. Fundamenta Informaticae, 22(1/2), 1995.

    Google Scholar 

  55. E. Moggi. Metalanguages and applications. In Semantics and Logics of Computation, volume 14 of Publications of the Newton Institute. Cambridge University Press, 1997.

    Google Scholar 

  56. P. Mosses. Denotational semantics. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 11. MIT press, 1990.

    Google Scholar 

  57. P. Mosses. Action Semantics. Number 26 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.

    Google Scholar 

  58. E. Moggi and F. Palumbo. Monadic encapsulation of effects: A revised approach. In Proceedings of the Third International Workshop on Higher-Order Operational Techniques in Semantics, Electronic Notes in Theoretical Computer Science. Elsevier, September 1999.

    Google Scholar 

  59. E. Moggi and A. Sabry. Monadic encapsulation of effects: A revised approach (extended version). Journal of Functional Programming, 11(6), November 2001.

    Google Scholar 

  60. I. Mason and C. Talcott. Equivalences in functional languages with effects. Journal of Functional Programming, 1:287–327, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  61. G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):528–569, May 1999.

    Google Scholar 

  62. F. Nielson and H. R. Nielson. Higher-order concurrent programs with finite communication topology. In Proceedings of the 21st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1994.

    Google Scholar 

  63. H. R. Nielson, F. Nielson, and T. Amtoft. Polymorphic subtyping for effect analysis: The static semantics. In Mads Dam, editor, Proceedings of the Fifth LOMAPS Workshop, number 1192 in Lecture Notes in Computer Science. Springer-Verlag, 1997.

    Google Scholar 

  64. F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.

    Google Scholar 

  65. F. Pfenning and R. Davies. A judgemental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4), August 2001.

    Google Scholar 

  66. S. L. Peyton Jones. Compiling Haskell by program transformation: A report from the trenches. In Proceedings of the European Symposium on Programming, Linköping, Sweden, number 1058 in Lecture Notes in Computer Science. Springer-Verlag, January 1996.

    Google Scholar 

  67. Simon Peyton Jones. Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. In R Steinbrueggen, editor, Engineering theories of software construction, Marktoberdorf Summer School 2000, NATO ASI Series. IOS Press, 2001.

    Google Scholar 

  68. A. M. Pitts. Operationally-based theories of program equivalence. In P. Dybjer and A. M. Pitts, editors, Semantics and Logics of Computation, Publications of the Newton Institute, pages 241–298. Cambridge University Press, 1997.

    Google Scholar 

  69. A. M. Pitts. Operational semantics and program equivalence. revised version of lectures at the international summer school on applied semantics. This volume, September 2000.

    Google Scholar 

  70. A.M. Pitts. Categorical logic. In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 5. Oxford University Press, 2000.

    Google Scholar 

  71. G. D. Plotkin. Call-by-name, call-by-value and the lambda calculus. Theoretical Computer Science, pages 125–159, 1975.

    Google Scholar 

  72. G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223–255, 1977.

    Article  MathSciNet  Google Scholar 

  73. S. L. Peyton Jones, J. Launchbury, M. B. Shields, and A. P. Tolmach. Bridging the gulf: A common intermediate language for ML and Haskell. In Proceedings of POPL’98. ACM, 1998.

    Google Scholar 

  74. S. L. Peyton Jones, J. Launchbury, M. B. Shields, and A. P. Tolmach. Corrigendum to bridging the gulf: A common intermediate language for ML and Haskell. Available from http://www.cse.ogi.edu/mbs/pub, 1998.

  75. D.S. Scott. A type-theoretic alternative to CUCH, ISWIM, OWHY. Theoretical Computer Science, 121, 1993.

    Google Scholar 

  76. A. Sabry and M. Felleisen. Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation, 6(3/4):289–360, 1993.

    Article  Google Scholar 

  77. Z. Shao. An overview of the FLINT/ML compiler. In Proceedings of the 1997 ACM Workshop on Types in Compilation, Amsterdam. ACM, June 1997.

    Google Scholar 

  78. M. Semmelroth and A. Sabry. Monadic encapsulation in ML. In Proceedings of the International Conference on Functional Programming. ACM, 1999.

    Google Scholar 

  79. I. D. B. Stark. Names and Higher Order Functions. PhD thesis, Computer Laboratory, University of Cambridge, 1994.

    Google Scholar 

  80. I. Stark. Categorical models for local names. Lisp and Symbolic Computation, 9(1), February 1996.

    Google Scholar 

  81. Amr Sabry and Philip Wadler. A reflection on call-by-value. ACM Transactions on Programming Languages and Systems, 19(6):916–941, November 1997.

    Google Scholar 

  82. J.-P. Talpin and P. Jouvelot. The type and effect discipline. Information and Computation, 111(2), June 1994. Revised from LICS 1992.

    Google Scholar 

  83. M. Tofte. Operational Semantics and Polymorphic Type Inference. PhD thesis, Department of Computer Science, University of Edinburgh, 1987.

    Google Scholar 

  84. A. Tolmach. Optimizing ML using a hierarchy of monadic types. In Proceedings of the Workshop on Types in Compilation, Kyoto, March 1998.

    Google Scholar 

  85. M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2), February 1997.

    Google Scholar 

  86. P. Wadler. Comprehending monads. Mathematical Structures in Computer Science, 2, 1992.

    Google Scholar 

  87. P. Wadler. The essence of functional programming. In Proceedings 1992 Symposium on Principles of Programming Languages, pages 1–14, Albuquerque, New Mexico, 1992.

    Google Scholar 

  88. P. Wadler. Monads for functional programming. In J. Jeuring and E. Meijer, editors, Advanced Functional Programming, number 925 in LNCS, pages 24–52. Springer Verlag, May 1995.

    Google Scholar 

  89. P. Wadler. The marriage of effects and monads. In International Conference on Functional Programming. ACM Press, 1998.

    Google Scholar 

  90. A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 15 November 1994.

    Google Scholar 

  91. A. Wright. Simple imperative polymorphism. LISP and Symbolic Computation, 8:343–355, 1995.

    Article  Google Scholar 

  92. P. Wadler and P. Thiemann. The marriage of effects and monads. To appear in ACM Transactions on Computational Logic, 1999.

    Google Scholar 

Download references