Document Open Access Logo

The Dynamic Practice and Static Theory of Gradual Typing

Author Michael Greenberg

PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2019.6.pdf
  • Filesize: 0.89 MB
  • 20 pages

Document Identifiers

Author Details

Michael Greenberg
  • Pomona College, Claremont, CA, USA

Acknowledgements

I thank Sam Tobin-Hochstadt and David Van Horn for their hearty if dubious encouragment. Conversations with Sam, Ron Garcia, Matthias Felleisen, Robby Findler, and Spencer Florence improved the argumentation. Stephanie Weirich helped me with Haskell programming; Richard Eisenberg wrote the program in Figure 3. Ross Tate, Neel Krishnaswami, Ron, and Éric Tanter provided helpful references I had overlooked. Ben Greenman provided helpful feedback. The anonymous SNAPL reviewers provided insightful comments as well as the CDuce code in Section 3.4.3. Finally, I thank Stephen Chong and Harvard Computer Science for hosting me while on sabbatical.

Cite AsGet BibTex

Michael Greenberg. The Dynamic Practice and Static Theory of Gradual Typing. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.SNAPL.2019.6

Abstract

We can tease apart the research on gradual types into two `lineages': a pragmatic, implementation-oriented dynamic-first lineage and a formal, type-theoretic, static-first lineage. The dynamic-first lineage’s focus is on taming particular idioms - `pre-existing conditions' in untyped programming languages. The static-first lineage’s focus is on interoperation and individual type system features, rather than the collection of features found in any particular language. Both appear in programming languages research under the name "gradual typing", and they are in active conversation with each other. What are these two lineages? What challenges and opportunities await the static-first lineage? What progress has been made so far?

Subject Classification

ACM Subject Classification
  • Social and professional topics → History of programming languages
  • Software and its engineering → Language features
Keywords
  • dynamic typing
  • gradual typing
  • static typing
  • implementation
  • theory
  • challenge problems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic Typing in a Statically-typed Language. In Principles of Programming Languages (POPL), pages 213-227, New York, NY, USA, 1989. ACM. URL: http://dx.doi.org/10.1145/75277.75296.
  2. Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. Blame for all. In Principles of Programming Languages (POPL), pages 201-214, 2011. URL: http://dx.doi.org/10.1145/1926385.1926409.
  3. Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. Theorems for free for free: parametricity, with and without types. PACMPL, 1(ICFP):39:1-39:28, 2017. URL: http://dx.doi.org/10.1145/3110283.
  4. Beatrice Åkerblom, Jonathan Stendahl, Mattias Tumlin, and Tobias Wrigstad. Tracing Dynamic Features in Python Programs. In Working Conference on Mining Software Repositories (MSR), pages 292-295, New York, NY, USA, 2014. ACM. URL: http://dx.doi.org/10.1145/2597073.2597103.
  5. Esteban Allende, Oscar Callaú, Johan Fabry, Éric Tanter, and Marcus Denker. Gradual Typing for Smalltalk. Sci. Comput. Program., 96(P1):52-69, December 2014. URL: http://dx.doi.org/10.1016/j.scico.2013.06.006.
  6. Esteban Allende, Johan Fabry, Ronald Garcia, and Éric Tanter. Confined gradual typing. In Object Oriented Programming Systems Languages and Applications (OOPSLA), pages 251-270, 2014. URL: http://dx.doi.org/10.1145/2660193.2660222.
  7. Esteban Allende, Johan Fabry, and Éric Tanter. Cast Insertion Strategies for Gradually-typed Objects. In Dynamic Languages Symposium (DLS), pages 27-36, New York, NY, USA, 2013. ACM. URL: http://dx.doi.org/10.1145/2508168.2508171.
  8. David An, Avik Chaudhuri, Jeffrey Foster, and Michael Hicks. Dynamic Inference of Static Types for Ruby. In Principles of Programming Languages (POPL), pages 459-472. ACM, 2011. Google Scholar
  9. Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. A Theory of Gradual Effect Systems. In International Conference on Functional Programming (ICFP), pages 283-295, New York, NY, USA, 2014. ACM. URL: http://dx.doi.org/10.1145/2628136.2628149.
  10. Nick Benton. Embedded Interpreters. J. Funct. Program., 15(4):503-542, July 2005. URL: http://dx.doi.org/10.1017/S0956796804005398.
  11. Nick Benton. Undoing Dynamic Typing (Declarative Pearl). In Jacques Garrigue and Manuel V. Hermenegildo, editors, Functional and Logic Programming, pages 224-238, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. Google Scholar
  12. Véronique Benzaken, Giuseppe Castagna, and Alain Frisch. CDuce: an XML-centric general-purpose language. In International Conference on Functional Programming (ICFP), pages 51-63. ACM, 2003. URL: http://dx.doi.org/10.1145/944705.944711.
  13. Bard Bloom, John Field, Nathaniel Nystrom, Johan Östlund, Gregor Richards, Rok Strnisa, Jan Vitek, and Tobias Wrigstad. Thorn: robust, concurrent, extensible scripting on the JVM. In Object Oriented Programming Systems Languages and Applications (OOPSLA), pages 117-136, 2009. URL: http://dx.doi.org/10.1145/1640089.1640098.
  14. William J. Bowman and Amal Ahmed. Typed Closure Conversion for the Calculus of Constructions. In Programming Language Design and Implementation (PLDI), pages 797-811, New York, NY, USA, 2018. ACM. URL: http://dx.doi.org/10.1145/3192366.3192372.
  15. William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed. Type-preserving CPS Translation of Σ and Π Types is Not Not Possible. Proc. ACM Program. Lang., 2(POPL):22:1-22:33, December 2017. URL: http://dx.doi.org/10.1145/3158110.
  16. John Boyland. The Problem of Structural Type Tests in a Gradual-Typed Language. In FOOL, 2014. Google Scholar
  17. Gilad Bracha. Pluggable type systems, October 2004. URL: http://bracha.org/pluggableTypesPosition.pdf.
  18. John Peter Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw. Migrating Gradual Types. Proc. ACM Program. Lang., 2(POPL):15:1-15:29, December 2017. URL: http://dx.doi.org/10.1145/3158103.
  19. John Peter Campora, Sheng Chen, and Eric Walkingshaw. Casts and Costs: Harmonizing Safety and Performance in Gradual Typing. Proc. ACM Program. Lang., 2(ICFP):98:1-98:30, July 2018. URL: http://dx.doi.org/10.1145/3236793.
  20. Robert Cartwright. User-Defined Data Types as an Aid to Verifying LISP Programs. In ICALP, 1976. Google Scholar
  21. Robert Cartwright and Mike Fagan. Soft Typing. In Programming Language Design and Implementation (PLDI), pages 278-292, New York, NY, USA, 1991. ACM. URL: http://dx.doi.org/10.1145/113445.113469.
  22. Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. Step-Indexed Normalization for a Language with General Recursion. In MSFP, volume 76, pages 25-39, 2012. Google Scholar
  23. Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. Combining proofs and programs in a dependently typed language. In Principles of Programming Languages (POPL), pages 33-46. ACM, 2014. Google Scholar
  24. Giuseppe Castagna and Victor Lanvin. Gradual Typing with Union and Intersection Types. Proc. ACM Program. Lang., 1(ICFP):41:1-41:28, August 2017. URL: http://dx.doi.org/10.1145/3110285.
  25. Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek. Gradual Typing: A New Perspective. Proc. ACM Program. Lang., 3(POPL):16:1-16:32, January 2019. URL: http://dx.doi.org/10.1145/3290329.
  26. Adam Chlipala. Ur: Statically-typed Metaprogramming with Type-level Record Computation. In Programming Language Design and Implementation (PLDI), pages 122-133, New York, NY, USA, 2010. ACM. URL: http://dx.doi.org/10.1145/1806596.1806612.
  27. Matteo Cimini and Jeremy G. Siek. The gradualizer: a methodology and algorithm for generating gradual type systems. In Principles of Programming Languages (POPL), pages 443-455, 2016. URL: http://dx.doi.org/10.1145/2837614.2837632.
  28. Pierre-Évariste Dagand, Nicolas Tabareau, and Éric Tanter. Foundations of dependent interoperability. Journal of Functional Programming, 28:e9, 2018. URL: http://dx.doi.org/10.1017/S0956796818000011.
  29. Tim Disney and Cormac Flanagan. Gradual Information Flow Typing. In Workshop on Script-to-Program Evolution (STOP), 2011. Google Scholar
  30. Paolo Donadeo. Lua-OCaml. URL: https://pdonadeo.github.io/ocaml-lua/.
  31. Richard Eisenberg. Haskell as a gradually typed dynamic language, January 2016. URL: https://typesandkinds.wordpress.com/2016/01/22/haskell-as-a-gradually-typed-dynamic-language/.
  32. Mike Fagan. Soft typing: An approach to type checking for dynamically typed languages. PhD thesis, Rice University, 1991. URL: https://scholarship.rice.edu/handle/1911/16439.
  33. L. Fennell and P. Thiemann. Gradual Security Typing with References. In Computer Security Foundations Symposium (CSF), pages 224-239, June 2013. URL: http://dx.doi.org/10.1109/CSF.2013.22.
  34. Robert Bruce Findler and Matthias Felleisen. Contracts for higher-order functions. In International Conference on Functional Programming (ICFP), pages 48-59, 2002. URL: http://dx.doi.org/10.1145/581478.581484.
  35. Robert Bruce Findler, Shu-Yu Guo, and Anne Rogers. Lazy Contract Checking for Immutable Data Structures. In Olaf Chitil, Zoltán Horváth, and Viktória Zsók, editors, Implementation and Application of Functional Languages, pages 111-128. Springer-Verlag, Berlin, Heidelberg, 2008. URL: http://dx.doi.org/10.1007/978-3-540-85373-2_7.
  36. Cormac Flanagan. Hybrid type checking. In Principles of Programming Languages (POPL), pages 245-256, 2006. URL: http://dx.doi.org/10.1145/1111037.1111059.
  37. The Node Foundation. ExpressJS. URL: https://expressjs.com/.
  38. Tim Freeman and Frank Pfenning. Refinement types for ML. In Programming Language Design and Implementation (PLDI), June 1991. Google Scholar
  39. Michael Furr, Jong-hoon (David) An, Jeffrey S. Foster, and Michael W. Hicks. Static type inference for Ruby. In Symposium on Applied Computing (SAC), pages 1859-1866, 2009. URL: http://dx.doi.org/10.1145/1529282.1529700.
  40. Ronald Garcia. Gradual Typing (keynote), 2018. ICFP. URL: https://www.youtube.com/watch?v=fQRRxaWsuxI.
  41. Ronald Garcia and Matteo Cimini. Principal Type Schemes for Gradual Programs. In Principles of Programming Languages (POPL), pages 303-315, New York, NY, USA, 2015. ACM. URL: http://dx.doi.org/10.1145/2676726.2676992.
  42. Ronald Garcia, Alison M. Clark, and Éric Tanter. Abstracting gradual typing. In Principles of Programming Languages (POPL), pages 429-442, 2016. URL: http://dx.doi.org/10.1145/2837614.2837670.
  43. Jacques Garrigue. Code reuse through polymorphic variants. In FOSE, 2000. Google Scholar
  44. Kathryn E. Gray, Robert Bruce Findler, and Matthew Flatt. Fine-grained Interoperability Through Mirrors and Contracts. In Object Oriented Programming Systems Languages and Applications (OOPSLA), pages 231-245, New York, NY, USA, 2005. ACM. URL: http://dx.doi.org/10.1145/1094811.1094830.
  45. Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich. Contracts made manifest. In Principles of Programming Languages (POPL), pages 353-364. ACM, 2010. Google Scholar
  46. Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich. Contracts made manifest. J. Funct. Program., 22(3):225-274, 2012. Google Scholar
  47. Ben Greenman and Matthias Felleisen. A Spectrum of Type Soundness and Performance. Proc. ACM Program. Lang., 2(ICFP):71:1-71:32, July 2018. URL: http://dx.doi.org/10.1145/3236766.
  48. Ben Greenman and Zeina Migeed. On the Cost of Type-Tag Soundness. In Partial Evaluation and Program Manipulation PEPM, pages 30-39, 2018. URL: http://dx.doi.org/10.1145/3162066.
  49. Ben Greenman, Asumu Takikawa, Max S. New, Daniel Feltey, Robert Bruce Findler, Jan Vitek, and Matthias Felleisen. How to evaluate the performance of gradual type systems. Journal of Functional Programming, 29:e4, 2019. URL: http://dx.doi.org/10.1017/S0956796818000217.
  50. Fritz Henglein. Dynamic Typing: Syntax and Proof Theory. In European Symposium on Programming (ESOP), pages 197-230, Amsterdam, The Netherlands, The Netherlands, 1994. Elsevier Science Publishers B. V. URL: http://dl.acm.org/citation.cfm?id=197475.190867.
  51. Fritz Henglein. Dynamic Typing: Syntax and Proof Theory. Sci. Comput. Program., 22(3):197-230, June 1994. URL: http://dx.doi.org/10.1016/0167-6423(94)00004-2.
  52. Stefan Heule, Deian Stefan, Edward Z. Yang, John C. Mitchell, and Alejandro Russo. IFC inside: Retrofitting languages with dynamic information flow control. In POST, volume 9036, pages 11-31. Springer, 2015. Google Scholar
  53. David Van Horn, September 2018. URL: https://twitter.com/lambda_calculus/status/1039702266679369730.
  54. Cătălin Hriţcu, Michael Greenberg, Ben Karel, Benjamin C. Pierce, and Greg Morrisett. All Your IFCException Are Belong to Us. In Security and Privacy (SP), pages 3-17, 2013. I am deeply embarrassed by the title of this paper. URL: http://dx.doi.org/10.1109/SP.2013.10.
  55. Atsushi Igarashi, Peter Thiemann, Vasco T. Vasconcelos, and Philip Wadler. Gradual session types. PACMPL, 1(ICFP):38:1-38:28, 2017. URL: http://dx.doi.org/10.1145/3110282.
  56. Andrew M. Kent, David Kempe, and Sam Tobin-Hochstadt. Occurrence typing modulo theories. In Programming Language Design and Implementation (PLDI), pages 296-309. ACM, 2016. Google Scholar
  57. Oleg Kiselyov and Ralf Lämmel. Haskell’s overlooked object system. CoRR, abs/cs/0509027, 2005. Google Scholar
  58. Oleg Kiselyov, Ralf Lämmel, and Keean Schupke. Strongly Typed Heterogeneous Collections. In ACM SIGPLAN Workshop on Haskell, pages 96-107, New York, NY, USA, 2004. ACM. URL: http://dx.doi.org/10.1145/1017472.1017488.
  59. S. Kleinschmager, R. Robbes, A. Stefik, S. Hanenberg, and E. Tanter. Do static type systems improve the maintainability of software systems? An empirical study. In IEEE International Conference on Program Comprehension (ICPC), pages 153-162, June 2012. URL: http://dx.doi.org/10.1109/ICPC.2012.6240483.
  60. Andre Kuhlenschmidt, Deyaaeldeen Almahallawi, and Jeremy G. Siek. Efficient Gradual Typing. In Programming Language Design and Implementation (PLDI), 2019. To appear. URL: http://arxiv.org/abs/1802.06375.
  61. Nico Lehmann and Éric Tanter. Gradual Refinement Types. In Principles of Programming Languages (POPL), pages 775-788, New York, NY, USA, 2017. ACM. URL: http://dx.doi.org/10.1145/3009837.3009856.
  62. Jacob Matthews and Amal Ahmed. Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices! In European Symposium on Programming (ESOP), pages 16-31, 2008. URL: http://dx.doi.org/10.1007/978-3-540-78739-6_2.
  63. Jacob Matthews and Robert Bruce Findler. Operational semantics for multi-language programs. ACM Trans. Program. Lang. Syst., 31(3):12:1-12:44, 2009. URL: http://dx.doi.org/10.1145/1498926.1498930.
  64. Clemens Mayer, Stefan Hanenberg, Romain Robbes, Éric Tanter, and Andreas Stefik. An Empirical Study of the Influence of Static Type Systems on the Usability of Undocumented Software. In Object Oriented Programming Systems Languages and Applications (OOPSLA), pages 683-702, New York, NY, USA, 2012. ACM. URL: http://dx.doi.org/10.1145/2384616.2384666.
  65. Microsoft. Dynamic Language Runtime overview. URL: https://docs.microsoft.com/en-us/dotnet/framework/reflection-and-codedom/dynamic-language-runtime-overview.
  66. Yusuke Miyazaki, Taro Sekiyama, and Atsushi Igarashi. Dynamic Type Inference for Gradual Hindley-Milner Typing. Proc. ACM Program. Lang., 3(POPL):18:1-18:29, January 2019. URL: http://dx.doi.org/10.1145/3290331.
  67. J. Garrett Morris and James McKinna. Abstracting Extensible Data Types: Or, Rows by Any Other Name. Proc. ACM Program. Lang., 3(POPL):12:1-12:28, January 2019. URL: http://dx.doi.org/10.1145/3290325.
  68. Fabian Muehlboeck and Ross Tate. Sound Gradual Typing is Nominally Alive and Well. In Object Oriented Programming Systems Languages and Applications (OOPSLA), New York, NY, USA, 2017. ACM. URL: http://dx.doi.org/10.1145/3133880.
  69. Max S. New and Amal Ahmed. Graduality from embedding-projection pairs. PACMPL, 2(ICFP):73:1-73:30, 2018. Google Scholar
  70. Max S. New, Daniel R. Licata, and Amal Ahmed. Gradual type theory. PACMPL, 3(POPL):15:1-15:31, 2019. Google Scholar
  71. Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn. Soft contract verification for higher-order stateful programs. PACMPL, 2(POPL):51:1-51:30, 2018. URL: http://dx.doi.org/10.1145/3158139.
  72. Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn. Size-Change Termination as a Contract. In Programming Language Design and Implementation (PLDI), 2019. To appear. URL: http://arxiv.org/abs/1808.02101.
  73. Alberto Oliart. An algorithm for inferring quasi-static types. Technical Report 1994-013, Boston University, 1994. URL: http://www.cs.bu.edu/techreports/pdf/1994-013-quasi-static-types.pdf.
  74. Peter-Michael Osera, Vilhelm Sjöberg, and Steve Zdancewic. Dependent interoperability. In PLPV, pages 3-14. ACM, 2012. Google Scholar
  75. James Parker, Niki Vazou, and Michael Hicks. LWeb: Information Flow Security for Multi-tier Web Applications. Proc. ACM Program. Lang., 3(POPL):75:1-75:30, January 2019. URL: http://dx.doi.org/10.1145/3290388.
  76. Daniel Patterson and Amal Ahmed. Linking Types for Multi-Language Software: Have Your Cake and Eat It Too. In Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi, editors, Summit on Advances in Programming Languages (SNAPL), volume 71, pages 12:1-12:15, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.SNAPL.2017.12.
  77. PLT. URL: https://docs.racket-lang.org/reference/strings.html.
  78. PLT. URL: https://docs.racket-lang.org/ts-guide/optimization.html.
  79. Norman Ramsey. Embedding an Interpreted Language Using Higher-order Functions and Types. In Workshop on Interpreters, Virtual Machines and Emulators (IVME), pages 6-14, New York, NY, USA, 2003. ACM. URL: http://dx.doi.org/10.1145/858570.858571.
  80. Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin M. Bierman, and Panagiotis Vekris. Safe & Efficient Gradual Typing for TypeScript. In Principles of Programming Languages (POPL), pages 167-180, 2015. URL: http://dx.doi.org/10.1145/2676726.2676971.
  81. Brianna M. Ren, John Toman, T. Stephen Strickland, and Jeffrey S. Foster. The ruby type checker. In Symposium on Applied Computing (SAC), pages 1565-1572, 2013. URL: http://dx.doi.org/10.1145/2480362.2480655.
  82. Gregor Richards, Christian Hammer, Brian Burg, and Jan Vitek. The Eval That Men Do. In Mira Mezini, editor, European Conference on Object-Oriented Programming (ECOOP), pages 52-78, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  83. Andrew Ruef, Michael Hicks, James Parker, Dave Levin, Michelle L. Mazurek, and Piotr Mardziel. Build It, Break It, Fix It: Contesting Secure Development. In Computer and Communications Security (CCS), pages 690-703, New York, NY, USA, 2016. ACM. URL: http://dx.doi.org/10.1145/2976749.2978382.
  84. Gabriel Scherer, Max New, Nick Rioux, and Amal Ahmed. Fabous Interoperability for ML and a Linear Language. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures (FoSSaCS), pages 146-162, Cham, 2018. Springer International Publishing. Google Scholar
  85. Ilya Sergey and Dave Clarke. Gradual Ownership Types. In European Symposium on Programming (ESOP), pages 579-599, Berlin, Heidelberg, 2012. Springer-Verlag. URL: http://dx.doi.org/10.1007/978-3-642-28869-2_29.
  86. Uri Shaked. TypeWiz, 2019. URL: https://github.com/urish/typewiz.
  87. Jeremy G. Siek and Walid Taha. Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop, pages 81-92, 2006. Google Scholar
  88. Jeremy G. Siek and Walid Taha. Gradual Typing for Objects. In European Conference on Object-Oriented Programming (ECOOP), pages 2-27, 2007. URL: http://dx.doi.org/10.1007/978-3-540-73589-2_2.
  89. Jeremy G. Siek and Sam Tobin-Hochstadt. The Recursive Union of Some Gradual Types. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, pages 388-410, 2016. URL: http://dx.doi.org/10.1007/978-3-319-30936-1_21.
  90. Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. Refined Criteria for Gradual Typing. In Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett, editors, Summit on Advances in Programming Languages (SNAPL), volume 32, pages 274-293, Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.SNAPL.2015.274.
  91. Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, Sam Tobin-Hochstadt, and Ronald Garcia. Monotonic References for Efficient Gradual Typing. In Jan Vitek, editor, European Symposium on Programming (ESOP), pages 432-456, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg. Google Scholar
  92. Michael Snoyman et al. Yesod. URL: https://www.yesodweb.com/.
  93. Vincent St-Amour, Sam Tobin-Hochstadt, Matthew Flatt, and Matthias Felleisen. Typing the Numeric Tower. In Practical Aspects of Declarative Languages (PADL), pages 289-303, 2012. URL: http://dx.doi.org/10.1007/978-3-642-27694-1_21.
  94. Deian Stefan, David Mazières, John C. Mitchell, and Alejandro Russo. Flexible dynamic information flow control in the presence of exceptions. J. Funct. Program., 27:e5, 2017. Google Scholar
  95. Deian Stefan, Alejandro Russo, John Mitchell, and David Maziéres. Flexible Dynamic Information Flow Control in Haskell. In Haskell Symposium, 2011. Google Scholar
  96. Nikhil Swamy, Michael Hicks, and Gavin M. Bierman. A Theory of Typed Coercions and Its Applications. In International Conference on Functional Programming (ICFP), pages 329-340, New York, NY, USA, 2009. ACM. URL: http://dx.doi.org/10.1145/1596550.1596598.
  97. Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin. Dependent Types and Multi-monadic Effects in F*. In Principles of Programming Languages (POPL), pages 256-270, New York, NY, USA, 2016. ACM. URL: http://dx.doi.org/10.1145/2837614.2837655.
  98. Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen. Position Paper: Performance Evaluation for Gradual Typing. In Workshop on Script-to-Program Evolution (STOP), New York, NY, USA, 2015. ACM. URL: http://www.ccs.neu.edu/home/types/publications/pe4gt/pe4gt.pdf.
  99. Asumu Takikawa, T. Stephen Strickland, Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. Gradual typing for first-class classes. In Object Oriented Programming Systems Languages and Applications (OOPSLA), pages 793-810, 2012. URL: http://dx.doi.org/10.1145/2384616.2384674.
  100. Satish R. Thatte. Quasi-Static Typing. In Principles of Programming Languages (POPL), pages 367-381, 1990. URL: http://dx.doi.org/10.1145/96709.96747.
  101. Sam Tobin-Hochstadt, September 2018. URL: https://twitter.com/samth/status/1039707471290478595.
  102. Sam Tobin-Hochstadt and Matthias Felleisen. Interlanguage migration: from scripts to programs. In Object Oriented Programming Systems Languages and Applications (OOPSLA), pages 964-974, 2006. URL: http://dx.doi.org/10.1145/1176617.1176755.
  103. Sam Tobin-Hochstadt and Matthias Felleisen. The Design and Implementation of Typed Scheme. In Principles of Programming Languages (POPL), pages 395-406, New York, NY, USA, 2008. ACM. URL: http://dx.doi.org/10.1145/1328438.1328486.
  104. Sam Tobin-Hochstadt and Matthias Felleisen. Logical types for untyped languages. In International Conference on Functional Programming (ICFP), pages 117-128. ACM, 2010. Google Scholar
  105. Sam Tobin-Hochstadt, Matthias Felleisen, Robert Findler, Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland, and Asumu Takikawa. Migratory Typing: Ten Years Later. In Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi, editors, Summit on Advances in Programming Languages (SNAPL), volume 71, pages 17:1-17:17, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.SNAPL.2017.17.
  106. Sam Tobin-Hochstadt and Robert Bruce Findler. Cycles Without Pollution: A Gradual Typing Poem. In Workshop on Script to Program Evolution (STOP), pages 47-57, New York, NY, USA, 2009. ACM. URL: http://dx.doi.org/10.1145/1570506.1570512.
  107. Matías Toro, Ronald Garcia, and Éric Tanter. Type-Driven Gradual Security with References. ACM Trans. Program. Lang. Syst., 40(4):16:1-16:55, 2018. URL: https://dl.acm.org/citation.cfm?id=3229061.
  108. Matías Toro, Elizabeth Labrada, and Éric Tanter. Gradual parametricity, revisited. PACMPL, 3(POPL):17:1-17:30, 2019. URL: https://dl.acm.org/citation.cfm?id=3290330.
  109. Jesse A. Tov and Riccardo Pucella. Practical Affine Types. In Principles of Programming Languages (POPL), 2011. URL: http://dx.doi.org/10.1145/1926385.1926436.
  110. Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, and Deian Stefan. From fine- to coarse-grained dynamic information flow control and back. PACMPL, 3(POPL):76:1-76:31, 2019. Google Scholar
  111. Niki Vazou. Liquid Haskell: Haskell as a Theorem Prover. PhD thesis, University of California, San Diego, 2016. URL: https://escholarship.org/uc/item/8dm057ws.
  112. Michael M. Vitousek, Andrew M. Kent, Jeremy G. Siek, and Jim Baker. Design and Evaluation of Gradual Typing for Python. In Symposium on Dynamic Languages (DLS), pages 45-56, New York, NY, USA, 2014. ACM. URL: http://dx.doi.org/10.1145/2661088.2661101.
  113. Michael M. Vitousek, Cameron Swords, and Jeremy G. Siek. Big Types in Little Runtime: Open-world Soundness and Collaborative Blame for Gradual Type Systems. In Principles of Programming Languages (POPL), pages 762-774, New York, NY, USA, 2017. ACM. URL: http://dx.doi.org/10.1145/3009837.3009849.
  114. Philip Wadler and Robert Bruce Findler. Well-Typed Programs Can't Be Blamed. In European Symposium on Programming (ESOP), pages 1-16, 2009. URL: http://dx.doi.org/10.1007/978-3-642-00590-9_1.
  115. Stephanie Weirich. The influence of dependent types (keynote). In Principles of Programming Languages (POPL), page 1. ACM, 2017. Google Scholar
  116. Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Aaron Stump, Harley Eades, Peng (Frank) Fu, Garrin Kimmell, Tim Sheard, Ki Yung Ahn, and Nathan Collins. The Preliminary Design of the Trellys Core Language, 2011. Discussion session at PLPV. Google Scholar
  117. Sam Tobin-Hochstadt with Jeremy Siek, Asumu Takikawa, Ben Greenman, et al. URL: https://github.com/samth/gradual-typing-bib.
  118. Roger Wolff, Ronald Garcia, Éric Tanter, and Jonathan Aldrich. Gradual Typestate. In European Conference on Object-Oriented Programming (ECOOP), pages 459-483, 2011. URL: http://dx.doi.org/10.1007/978-3-642-22655-7_22.
  119. Tobias Wrigstad, Francesco Zappa Nardelli, Sylvain Lebresne, Johan Östlund, and Jan Vitek. Integrating typed and untyped code in a scripting language. In Principles of Programming Languages (POPL), pages 377-388. ACM, 2010. Google Scholar
  120. Ningning Xie, Xuan Bi, and Bruno C. d. S. Oliveira. Consistent Subtyping for All. In Amal Ahmed, editor, European Symposium on Programming (ESOP), pages 3-30, Cham, 2018. Springer International Publishing. Google Scholar
  121. Zhe Yang. Encoding Types in ML-like Languages. In International Conference on Functional Programming (ICFP), pages 289-300, New York, NY, USA, 1998. ACM. URL: http://dx.doi.org/10.1145/289423.289458.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact