×

No value restriction is needed for algebraic effects and handlers. (English) Zbl 1418.68034

Summary: We present a straightforward, sound, Hindley-Milner polymorphic type system for algebraic effects and handlers in a call-by-value calculus, which, to our surprise, allows type variable generalisation of arbitrary computations, and not just values. We first recall that the soundness of unrestricted call-by-value Hindley-Milner polymorphism is known to fail in the presence of computational effects such as reference cells and continuations, and that many programming examples can be recast to use effect handlers instead of these effects. After presenting the calculus and its soundness proof, formalised in Twelf, we analyse the expressive power of effect handlers with respect to state effects. We conjecture handlers alone cannot express reference cells, but show they can simulate dynamically scoped state, establishing that dynamic binding also does not need a value restriction.

MSC:

68N18 Functional programming and lambda calculus
68Q55 Semantics in the theory of computing
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

Twelf; ML; Koka; Eff; Links

References:

[1] AhmanD. (2015) Refinement types for algebraic effects (2015). In: Abstracts of the 21st Meeting ‘Types for Proofs and Programs’ (TYPES), Institute of Cybernetics, Tallinn University of Technology, pp. 10-11.
[2] AhmanD., GhaniN. & PlotkinG. D. (2016) Dependent types and fibred computational effects. In Proceedings of the 19th International Conference, Foundations of Software Science and Computation Structures - FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, JacobsB. & LödingC. (eds), Lecture Notes in Computer Science, vol. 9634. Berlin: Springer, pp. 36-54. · Zbl 1475.68057
[3] AhmanD. & StatonS. (2013) Normalization by evaluation and algebraic effects.Electr. Notes Theor. Comput. Sci.298, 51-69.10.1016/j.entcs.2013.09.007 · Zbl 1334.68046 · doi:10.1016/j.entcs.2013.09.007
[4] AppelA. W. & MacQueenD. B. (1991) Standard ML of New Jersey. In PLILP, pp. 1-13.
[5] AsaiK. & KameyamaY. (2007) Polymorphic delimited continuations. In APLAS, Lecture Notes in Computer Science, vol. 4807. Springer, pp. 239-254. · Zbl 1137.68344
[6] BauerA. & PretnarM. (2014) An effect system for algebraic effects and handlers.Log. Methods Comput. Sci.10(4:9), pp. 1-29. · Zbl 1448.68203
[7] BauerA. & PretnarM. (2015) Programming with algebraic effects and handlers.J. Log. Algebr. Meth. Program.84(1), 108-123.10.1016/j.jlamp.2014.02.001 · Zbl 1304.68025 · doi:10.1016/j.jlamp.2014.02.001
[8] BentonN., KennedyA. & RussellG. (1998) Compiling standard ML to java bytecodes. In Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming (ICFP ’98), Baltimore, Maryland, USA, September 27-29, 1998, FelleisenM., HudakP. & QueinnecC. (eds), ACM, pp. 129-140. · Zbl 1428.68096
[9] BradyE. (2013) Programming and reasoning with algebraic effects and dependent types. In Proceedings of ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA, September 25-27, 2013, MorrisettG. & UustaluT. (eds), ACM, pp. 133-144. · Zbl 1323.68097
[10] BradyE. (2014) Resource-dependent algebraic effects. In Proceedings of the 15th International Symposium on Trends in Functional Programming, TFP 2014, Soesterberg, The Netherlands, May 26-28, 2014. Revised Selected Papers. HageJ., & McCarthyJ. (eds), Lecture Notes in Computer Science, pp. 18-33. Berlin: Springer.
[11] CardelliL. (1991) Typeful programming. In Formal Description of Programming Concepts, NeuholdE. J. & PaulM. (eds). Berlin: Springer-Verlag, pp. 431-507. · Zbl 0743.68028
[12] CardelliL. & MitchellJ. C. (1991) Operations on records.Math. Struct. Comput. Sci.1(1), 3-48.10.1017/S0960129500000049 · Zbl 0727.68020 · doi:10.1017/S0960129500000049
[13] CartwrightR. & FelleisenM. (1994) Extensible denotational language specifications. In Proceedings of International Conference TACS ’94 on Theoretical Aspects of Computer Software, Sendai, Japan, April 19-22, 1994, HagiyaM. & MitchellJ. C. (eds). Lecture Notes in Computer Science, vol. 789. Springer pp. 244-272. · Zbl 0942.68544
[14] CooperE., LindleyS., WadlerP. & YallopJ. (2006) Links: Web programming without tiers. In Proceedings of the 5th International Symposium on Formal Methods for Components and Objects, FMCO 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures, de BoerF. S., BonsangueM. M., GrafS. & de RoeverW. P. (eds), Lecture Notes in Computer Science, vol. 4709. Springer, pp. 266-296.
[15] DanvyO. (2006) An Analytical Approach to Programs as Data oObjects. DSc dissertation, Department of Computer Science, University of Aarhus.
[16] DanvyO. & FilinskiA. (1989) A Functional Abstraction of Typed Contexts. Technical Report 89/12. DIKU.
[17] DanvyO. & FilinskiA. (1990) Abstracting control. In LISP and Functional Programming. pp. 151-160.
[18] FelleisenM. (1988) The theory and practice of first-class prompts. In Conference Record of the 15th Annual ACM Symposium on Principles of Programming Languages, San Diego, California, USA, January 10-13, 1988, FerranteJ. & MagerP. (eds), ACM Press, pp. 180-190.
[19] FelleisenM. (1991) On the expressive power of programming languages.Sci. Comput. Program.17(1-3), 35-75.10.1016/0167-6423(91)90036-W · Zbl 0745.68033 · doi:10.1016/0167-6423(91)90036-W
[20] FelleisenM., WandM., FriedmanD. P. & DubaB. F. (1988) Abstract continuations: A mathematical semantics for handling full jumps. In LISP and Functional Programming, pp. 52-62.
[21] FilinskiA. (1994) Representing monads. In Conference Record of POPL’94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, USA, January 17-21, 1994, BoehmH.-J., LangB. & YellinD. M. (eds), ACM Press, pp. 446-457.
[22] FioreM. P. & StatonS. (2014) Substitution, jumps, and algebraic effects. In CSL-LICS. ACM, pp. 41:1-41:10.
[23] ForsterY., KammarO., LindleyS. & PretnarM. (2016) On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control. arXiv:1610.09161 [cs.LO].
[24] GarrigueJ. (2001) Simple type inference for structural polymorphism. In Proceedings of the 2nd Asian Workshop on Programming Languages and Systems, APLAS’01, Korea Advanced Institute of Science and Technology, Daejeon, Korea, December 17-18, 2001, pp. 329-343.
[25] GarrigueJ. (2004) Relaxing the value restriction. In FLOPS. Lecture Notes in Computer Science, vol. 2998. Berlin: Springer, pp. 196-213. · Zbl 1122.68398
[26] GarrigueJ. (2010) A certified implementation of ML with structural polymorphism. In Proceedings of the 8th Asian Symposium on Programming Languages and Systems, APLAS 2010, Shanghai, China, November 28-December 1, 2010, UedaK. (ed), Lecture Notes in Computer Science, vol. 6461. Springer, pp. 360-375
[27] GarrigueJ. (2015) A certified implementation of ML with structural polymorphism and recursive types.Math. Struct. Comput. Sci.25(4), 867-891.10.1017/S0960129513000066 · Zbl 1361.68038 · doi:10.1017/S0960129513000066
[28] GiffordD. K. & LucassenJ. M. (1986) Integrating functional and imperative programming. In LISP and Functional Programming, pp. 28-38.
[29] GirardJ.-Y. (1972) (June) Interprétation fonctionnelle et élimination des coupures de l’arith-métique d’ordre supérieur. Thèse de doctorat d’état, Université Paris VII.
[30] GordonA. D. (ed). (2017) Proceedings of the 44th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages Paris, France—January 18-20, 2017, ACMNew York, NY, USA, 978-1-4503-4660-3. · Zbl 1355.68012
[31] GordonM. J. C., MilnerR. & WadsworthC. P. (1979) Edinburgh LCF. Lecture Notes in Computer Science, vol. 78. Berlin: Springer. · Zbl 0421.68039
[32] GunterC. A., RémyD. & RieckeJ. G. (1995) A generalization of exceptions and control in ML-like languages. In FPCA. ACM, pp. 12-23
[33] HancockP. & SetzerA. (2000) Interactive programs in dependent type theory. In Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic, Fischbachau, Germany, August 21-26, 2000, CloteP. & SchwichtenbergH. (eds), Lecture Notes in Computer Science, vol. 1862. Springer, pp. 317-331 · Zbl 0973.68041
[34] HarperR. & LillibridgeM. (1993a) Explicit polymorphism and CPS conversion. In Conference Record of the 20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, USA, January 1993, DeusenM. S. Van & LangB. (eds), ACM Press, pp. 206-219.
[35] HarperR. & LillibridgeM. (1993b) Polymorphic type assignment and CPS conversion.Lisp Symbolic Comput.6(3-4), 361-380.10.1007/BF01019463 · doi:10.1007/BF01019463
[36] HarperR. & MitchellJ. C. (1993) On the type structure of standard ML.ACM Trans. Program. Lang. Syst.15(2), 211-252.10.1145/169701.169696 · doi:10.1145/169701.169696
[37] HarperR. & PierceB. C. (1991) A record calculus based on symmetric concatenation. In Conference Record of the 18th Annual ACM Symposium on Principles of Programming Languages, Orlando, Florida, USA, January 21-23, 1991, WiseD. S. (ed), ACM Press, pp. 131-142.
[38] HillerströmD. & LindleyS. (2016) Liberating effects with rows and handlers. In Proceedings of the 1st International Workshop on Type-Driven Development, September 2016, ChapmanJ. & SwierstraW. (eds), ACM, pp. 15-27.
[39] HylandM., PlotkinG. D. & PowerJ. (2006) Combining effects: Sum and tensor.Theor. Comput. Sci.357(1-3), 70-99.10.1016/j.tcs.2006.03.013 · Zbl 1096.68088 · doi:10.1016/j.tcs.2006.03.013
[40] JaberG. & TzevelekosN. (2016) Trace semantics for polymorphic references. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’16). ACM, New York, NY, USA, 585-594. DOI: https://doi.org/10.1145/2933575.2934509 · Zbl 1401.68033
[41] KameyamaY. & YonezawaT. (2008) Typed dynamic control operators for delimited continuations. In Proceedings of Functional and Logic Programming, 9th International Symposium, FLOPS 2008, Ise, Japan, April 14-16, 2008, GarrigueJ. & HermenegildoM. V. (eds), Lecture Notes in Computer Science, vol. 4989. Springer, pp. 239-254. · Zbl 1137.68346
[42] KammarO. (2014) An Algebraic Theory of Type-and-Effect Systems. Ph.D. Thesis, University of Edinburgh, UK.
[43] KammarO. & PlotkinG. D. (2012) Algebraic foundations for effect-dependent optimisations. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, FieldJ. & HicksM. (eds), ACM, pp. 349-360. · Zbl 1321.68200
[44] KammarO., LindleyS. & OuryN. (2013) Handlers in action. In ICFP, ACM, pp. 145-158. · Zbl 1323.68126
[45] KatsumataS. (2013) Relating computational effects by ⊤⊤-lifting.Inf. Comput.222, 228-246.10.1016/j.ic.2012.10.014 · Zbl 1267.68087 · doi:10.1016/j.ic.2012.10.014
[46] KatsumataS. (2014) Parametric effect monads and semantics of effect systems. In Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, JagannathanS. & SewellP. (eds), ACM, pp. 633-646. · Zbl 1284.68133
[47] KiselyovO. (2015) Generating Code with Polymorphic Let. Technical Report, Tohoku University, Japan. Extended abstract submitted to the ACM SIGPLAN Workshop on ML.
[48] KiselyovO. & IshiiH. (2015) Freer monads, more extensible effects. In Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, Vancouver, BC, Canada, September 3-4, 2015, LippmeierB. (ed), ACM, pp. 94-105.
[49] KiselyovO. & ShanC.-C. (2007) A substructural type system for delimited continuations. In Proceedings of the 8th International Conference on Typed Lambda Calculi and Applications, TLCA 2007, Paris, France, June 26-28, 2007, RoccaS. & RonchiD. (ed), Lecture Notes in Computer Science, vol. 4583. Springer, pp. 223-239. · Zbl 1215.68124
[50] KiselyovO., ShanC.-C. & SabryA. (2006) Delimited dynamic binding. In ICFP. ACM, pp. 26-37. · Zbl 1321.68128
[51] KiselyovO., SabryA. & SwordsC. (2013) Extensible effects: An alternative to monad transformers. In Haskell. ACM, pp. 59-70.
[52] LandinP. J. (1964) The mechanical evaluation of expressions.Comput. J.6(4), 308-320.10.1093/comjnl/6.4.308 · Zbl 0122.36106 · doi:10.1093/comjnl/6.4.308
[53] LeijenD. (2014) Koka: Programming with row polymorphic effect types. In MSFP. EPTCS, vol. 153, pp. 100-126. · Zbl 1464.68062
[54] LeijenD. (2017) Type directed compilation of row-typed algebraic effects. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), Gordon A. D. (ed), ACM, New York, NY, USA, pp. 486-499. · Zbl 1380.68097
[55] LepigreR. (2016) A classical realizability model for a semantical value restriction. In Proceedings of the 25th European Symposium on Programming, Programming Languages and Systems, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, ThiemannP. (ed), Lecture Notes in Computer Science, vol. 9632. Springer, pp. 476-502. · Zbl 1335.68059
[56] LeroyX. (1992) Typage Polymorphe D’un Langage Algorithmique. PhD Thesis (in French), Université Paris 7.
[57] LeroyX. (1993) Polymorphism by name for references and continuations. In POPL. ACM Press, pp. 220-231.
[58] LeroyX. & WeisP. (1991) Polymorphic type inference and assignment. In POPL. ACM Press, pp. 291-302.
[59] LevyP. B. (2004) Call-by-Push-Value: A Functional/Imperative Synthesis. Semantics Structures in Computation, vol. 2. Berlin: Springer.
[60] LevyP. B., PowerJ. & ThieleckeH. (2003) Modelling environments in call-by-value programming languages.Inf. Comput.185(2), 182-210.10.1016/S0890-5401(03)00088-9 · Zbl 1069.68073 · doi:10.1016/S0890-5401(03)00088-9
[61] LillibridgeM. (1999) Unchecked exceptions can be strictly more powerful than call/cc.Higher-Order Symbol. Comput.12(1), 75-104.10.1023/A:1010020917337 · Zbl 0935.68010 · doi:10.1023/A:1010020917337
[62] LindleyS. & CheneyJ. (2012) Row-based effect types for database integration. In TLDI. ACM, pp. 91-102.
[63] LindleyS., McBrideC. & McLaughlinC. (2017) Do be do be do. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), GordonA. D. (ed), ACM, New York, NY, USA, pp. 500-514. · Zbl 1380.68098
[64] LippmeierB. (2009) Witnessing purity, constancy and mutability. In Proceedings of the 7th Asian Symposium on Programming Languages and Systems, APLAS 2009, Seoul, Korea, December 14-16, 2009, HuZ. (ed), Lecture Notes in Computer Science, vol. 5904. Springer, pp. 95-110.
[65] LucassenJ. M. & GiffordD. K. (1988) Polymorphic effect systems. In POPL. ACM Press, pp. 47-57.
[66] MarinoD. & MillsteinT. D. (2009) A generic type-and-effect system. In Proceedings of TLDI’09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009, KennedyA. & AhmedA. (eds), ACM, pp. 39-50.
[67] MellièsP.-A. (2010) Segal condition meets computational effects. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom. IEEE Computer Society, pp. 150-159.
[68] MellièsPaul-André. (2014) Local states in string diagrams. In Proceedings of Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, DowekG. (ed), Lecture Notes in Computer Science, vol. 8560. Springer, pp. 334-348. · Zbl 1416.68110
[69] MilnerR. (1978) A theory of type polymorphism in programming.J. Comput. Syst. Sci.17(3), 348-375.10.1016/0022-0000(78)90014-4 · Zbl 0388.68003 · doi:10.1016/0022-0000(78)90014-4
[70] MoggiE. (1991) Notions of computation and monads.Inf. Comput.93(1), 55-92.10.1016/0890-5401(91)90052-4 · Zbl 0723.68073 · doi:10.1016/0890-5401(91)90052-4
[71] MoreauL. (1998) A syntactic theory of dynamic binding.Higher-order and Symbolic Computation11(3), 233-279.10.1023/A:1010087314987 · Zbl 0934.68038 · doi:10.1023/A:1010087314987
[72] Munch-MaccagnoniG. (2009) Focalisation and classical realisability. In Computer Science Logic ’09, GrädelE. & KahleR. (eds), Lecture Notes in Computer Science, vol. 5771. Heidelberg: Springer, pp. 409-423. · Zbl 1257.03055
[73] NielsonF. & NielsonH. R. (1999) Type and effect systems. In Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the Occasion of his Retirement from his Professorship at the University of Kiel), OlderogE.-R. & SteffenB. (eds), Lecture Notes in Computer Science, vol. 1710. Berlin: Springer, pp. 114-136.
[74] OhoriA. (1989) A simple semantics for ML polymorphism. In Proceedings of the 4th International Conference on Functional Programming Languages and Computer Architecture, FPCA 1989, London, UK, September 11-13, 1989, StoyJ. E. (ed), ACM, pp. 281-292.
[75] OhoriA. (1992) A compilation method for ML-style polymorphic record calculi. In Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ’92), January 19-22, 1992, SethiR. (ed), ACM, New York, NY, USA, pp. 154-165.
[76] OhoriA. (1995) A polymorphic record calculus and its compilation.ACM Trans. Program. Lang. Syst.17(6), 844-895.10.1145/218570.218572 · doi:10.1145/218570.218572
[77] PfenningF. & SchürmannC. (1999) System description: Twelf - A meta-logical framework for deductive systems. In CADE. Lecture Notes in Computer Science, vol. 1632. Springer, pp. 202-206.
[78] PierceB. C. (2002) Types and Programming Languages. Cambridge, MA, USA: MIT Press. · Zbl 0995.68018
[79] PittsA. M. (2011-2016) Types. Lecture notes, University of Cambridge Computer Laboratory.
[80] PlotkinG. D. (1977) LCF considered as a programming language.Theor. Comput. Sci.5(3), 223-255.10.1016/0304-3975(77)90044-5 · Zbl 0369.68006 · doi:10.1016/0304-3975(77)90044-5
[81] PlotkinG. D. & PowerJ. (2002) Notions of computation determine monads. In Proceedings of the 5th International Conference, Foundations of Software Science and Computation Structures, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, NielsenM. & EngbergU. (eds), Lecture Notes in Computer Science, vol. 2303. Springer, pp. 342-356. · Zbl 1077.68676
[82] PlotkinG. D. & PowerJ. (2003) Algebraic operations and generic effects.Appl. Categorical Struct.11(1), 69-94.10.1023/A:1023064908962 · Zbl 1023.18006 · doi:10.1023/A:1023064908962
[83] PlotkinG. D. & PretnarM. (2008) A logic for algebraic effects. In Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA. IEEE Computer Society, pp. 118-129
[84] PlotkinG. D. & PretnarM. (2013) Handling algebraic effects.Logical Methods in Comput. Sci.9(4). · Zbl 1314.68191
[85] PretnarM. (2010) Logic and Handling of Algebraic Effects. Ph.D. thesis, University of Edinburgh, UK.
[86] PretnarM. (2014) Inferring algebraic effects.Log. Methods Comput. Sci.10(3). · Zbl 1341.68024
[87] PretnarM. (2015) An introduction to algebraic effects and handlers. invited tutorial paper.Electr. Notes Theor. Comput. Sci.319, 19-35.10.1016/j.entcs.2015.12.003 · Zbl 1351.68079 · doi:10.1016/j.entcs.2015.12.003
[88] RémyD. (1990) Algèbres touffues. application au typage polymorphe des objets enregistrements dans les langages fonctionnels. Thèse de doctorat, Université de Paris 7.
[89] RémyD.1991 (May) Type Inference for Records in a Natural Extension of ML. Research Report 1431. Institut National de Recherche en Informatique et Automatisme, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France.
[90] RémyD. (2015) Type Systems. Lecture notes, Parisian Master of Research in Computer Science.
[91] ReynoldsJ. C. (1974) Towards a theory of type structure. In Programming Symposium, Proceedings Colloque Sur La Programmation. London, UK: Springer-Verlag, pp. 408-423. · Zbl 0309.68016
[92] ReynoldsJ. C. (1984) Polymorphism is not set-theoretic. In Proceedings of Semantics of Data Types, International Symposium, Sophia-Antipolis, France, June 27-29, 1984, KahnG., MacQueenD. B. & PlotkinG. D. (eds), Lecture Notes in Computer Science, vol. 173. Springer. pp. 145-156. · Zbl 0554.03012
[93] RompfT., MaierI. & OderskyM. (2009) Implementing first-class polymorphic delimited continuations by a type-directed selective cps-transform. In Proceeding of the 14th ACM SIGPLAN International Conference on Functional Programming, ICFP 2009, Edinburgh, Scotland, UK, August 31-September 2, 2009, HuttonG. & TolmachA. P. (eds), ACM, pp. 317-328. · Zbl 1302.68187
[94] SalehA. H. & SchrijversT. (2016) Efficient algebraic effect handlers for prolog. Corrabs/1608.00816. · Zbl 1379.68080
[95] ScottD. S. (1993) A type-theoretical alternative to ISWIM, CUCH, OWHY.Theor. Comput. Sci.121(1&2), 411-440.10.1016/0304-3975(93)90095-B · Zbl 0942.68522 · doi:10.1016/0304-3975(93)90095-B
[96] SethiR. (ed). (1992) Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. January 19-22, 1992. ACM, New York, NY, USA.
[97] ShanC.-C. (2007) A static simulation of dynamic delimited control.Higher-Order Symbol. Comput.20(4), 371-401.10.1007/s10990-007-9010-4 · Zbl 1128.68010 · doi:10.1007/s10990-007-9010-4
[98] StatonS. (2009) Two cotensors in one: Presentations of algebraic theories for local state and fresh names.Electr. Notes Theor. Comput. Sci.249, 471-490.10.1016/j.entcs.2009.07.103 · Zbl 1338.18034 · doi:10.1016/j.entcs.2009.07.103
[99] StatonS. (2010) Completeness for algebraic theories of local state. In Proceedings of 13th International Conference, Foundations of Software Science and Computational Structures, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010, OngC.-H. Luke (ed), Lecture Notes in Computer Science, vol. 6014. Springer, pp. 48-63. · Zbl 1284.68205
[100] StatonS. (2013a) An algebraic presentation of predicate logic - (extended abstract). In Proceedings of 16th International Conference, Foundations of Software Science and Computation Structures, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, PfenningF. (ed), Lecture Notes in Computer Science, vol. 7794, Springer, pp. 401-417. · Zbl 1260.68116
[101] StatonS. (2013b) Instances of computational effects: An algebraic perspective. In LICS, IEEE Computer Society., pp. 519. · Zbl 1368.68183
[102] StatonS. (2015) Algebraic effects, linearity, and quantum programming languages. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, RajamaniS. K. & WalkerD. (eds), ACM, pp. 395-406. · Zbl 1345.68137
[103] SwierstraW. (2008) Data types à la carte.J. Funct. Program.18(4), 423-436. · Zbl 1153.68015
[104] TofteM. (1990) Type inference for polymorphic references.Inf. Comput.89(1), 1-34.10.1016/0890-5401(90)90018-D · Zbl 0705.68028 · doi:10.1016/0890-5401(90)90018-D
[105] TolmachA. P. (1998) Optimizing ML using a hierarchy of monadic types. In Proceedings of the 2nd International Workshop on Types in Compilation, TIC ’98, Kyoto, Japan, March 25-27, 1998, LeroyX. & OhoriA. (eds), Lecture Notes in Computer Science, vol. 1473. Springer, pp. 97-115.
[106] WadlerP. (1992) The essence of functional programming. In Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ’92), January 19-22, 1992, SethiR. (ed), ACM, New York, NY, USA, pp. 1-14.
[107] WadlerP. & ThiemannP. (2003) The marriage of effects and monads.ACM Trans. Comput. Log.4(1), 1-32.10.1145/601775.601776 · Zbl 1365.68166 · doi:10.1145/601775.601776
[108] WandM. (1987) Complete type inference for simple objects. In Proceedings of the Symposium on Logic in Computer Science (LICS ’87), Ithaca, New York, USA, June 22-25, 1987. IEEE Computer Society, pp. 37-44.
[109] WellsJ. B. (1999) Typability and type checking in System F are equivalent and undecidable.Ann. Pure Appl. Logic98(1-3), 111-156.10.1016/S0168-0072(98)00047-5 · Zbl 0932.03017 · doi:10.1016/S0168-0072(98)00047-5
[110] WrightA. K. (1995) Simple imperative polymorphism.Lisp Symbol. Comput.8(4), 343-355.10.1007/BF01018828 · doi:10.1007/BF01018828
[111] WuN. & SchrijversT. (2015) Fusion for free—efficient algebraic effect handlers. In Proceedings of the 12th International Conference on Mathematics of Program Construction, MPC 2015, Königswinter, Germany, June 29-July 1, 2015, HinzeR. & VoigtländerJ. (eds), Lecture Notes in Computer Science, vol. 9129. Springer, pp. 302-322. · Zbl 1432.68077
[112] WuN., SchrijversT. & HinzeR. (2014) Effect handlers in scope. In Haskell. ACM, pp. 1-12.
[113] ZeilbergerN. (2009) Refinement types and computational duality. In Proceedings of the 3rd ACM Workshop on Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009, AltenkirchT. & MillsteinT. D. (eds), ACM, pp. 15-26.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.