Document Open Access Logo

Type Tailoring

Authors Ashton Wiersdorf , Stephen Chang , Matthias Felleisen , Ben Greenman

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.44.pdf
  • Filesize: 1.19 MB
  • 27 pages

Document Identifiers

Author Details

Ashton Wiersdorf
  • University of Utah, Salt Lake City, UT, USA
Stephen Chang
  • University of Massachusetts Boston, MA, USA
Matthias Felleisen
  • Northeastern University, Boston, MA, USA
Ben Greenman
  • University of Utah, Salt Lake City, UT, USA

Funding

This work was partially supported by DOE Office of Science Contract DE-SC0022252, XStack, ComPort, "Rigorous Testing Methods to Safeguard Software Porting" and by NSF grants https://www.nsf.gov/awardsearch/showAward?AWD_ID=1518844, https://www.nsf.gov/awardsearch/showAward?AWD_ID=2217154, and https://www.nsf.gov/awardsearch/showAward?AWD_ID=2030859 to the CRA for the https://cifellows2020.org project. Felleisen’s research was partially supported by several NSF grants (SHF 2007686, 2116372, 2315884).

Acknowledgements

Thanks to Sam Tobin-Hochstadt for inspiring tailoring in Typed Racket, to Mark Ericksen for teaching best practices of Phoenix Verified Routes, to Ryan Culpepper for syntax parse support, to Matthew Flatt for help with Rhombus annotations, and to Alex Knauth, Asumu Takikawa, Gabriel Scherer, Justin Slepak, Leif Andersen, Scott Wiersdorf, and Zeina Migeed for comments on early drafts.

Cite AsGet BibTex

Ashton Wiersdorf, Stephen Chang, Matthias Felleisen, and Ben Greenman. Type Tailoring. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 44:1-44:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ECOOP.2024.44

Abstract

Type systems evolve too slowly to keep up with the quick evolution of libraries - especially libraries that introduce abstractions. Type tailoring offers a lightweight solution by equipping the core language with an API for modifying the elaboration of surface code into the internal language of the typechecker. Through user-programmable elaboration, tailoring rules appear to improve the precision and expressiveness of the underlying type system. Furthermore, type tailoring cooperates with the host type system by expanding to code that the host then typechecks. In the context of a hygienic metaprogramming system, tailoring rules can even harmoniously compose with one another. Type tailoring has emerged as a theme across several languages and metaprogramming systems, but never with direct support and rarely in the same shape twice. For example, both OCaml and Typed Racket enable forms of tailoring, but in quite different ways. This paper identifies key dimensions of type tailoring systems and tradeoffs along each dimension. It demonstrates the usefulness of tailoring with examples that cover sized vectors, database queries, and optional types. Finally, it outlines a vision for future research at the intersection of types and metaprogramming.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Extensible languages
Keywords
  • Types
  • Metaprogramming
  • Macros
  • Partial Evaluation

Metrics

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

Supplementary Materials

References

  1. Michael D. Adams. Towards the essence of hygiene. In POPL, pages 457-469. ACM, 2015. URL: https://doi.org/10.1145/2676726.2677013.
  2. Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. Towards certified meta-programming with typed Template-Coq. In ITP, pages 20-39. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94821-8_2.
  3. Lennart Augustsson. Cayenne - a language with dependent types. In ICFP, pages 239-250. ACM, 1998. URL: https://doi.org/10.1145/289423.289451.
  4. Christiaan Baaij. GHC type checker plugins: adding new type-level operations, 2016. . Accessed 2016-06-30. URL: http://christiaanb.github.io/posts/type-checker-plugin/.
  5. Langston Barrett, David Thrane Christiansen, and Samuel Gélineau. Predictable macros for Hindley-Milner. In TyDE, 2020. Extended abstract. Google Scholar
  6. Gary Bernhardt. Software: static-path. . Accessed 2024-01-17. URL: https://github.com/garybernhardt/static-path.
  7. Jeff Bezanson, Alan Edelman, Stefan Karpinski, and Viral B. Shah. Julia: A fresh approach to numerical computing. SIAM Review, 59(1):65-98, 2017. URL: https://doi.org/10.1137/141000671.
  8. Gilad Bracha and David Griswold. Strongtalk: Typechecking Smalltalk in a production environment. In OOPSLA, pages 215-230, 1993. URL: https://doi.org/10.1145/165854.165893.
  9. Eugene Burmako. Scala macros: Let our powers combine!: On how rich syntax and static types work with metaprogramming. In SCALA, pages 3:1-3:10. ACM, 2013. URL: https://doi.org/10.1145/2489837.2489840.
  10. Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. Journal of Functional Programming, 19(5):509-543, 2009. URL: https://doi.org/10.1017/S0956796809007205.
  11. Stephen Chang, Michael Ballantyne, Milo Turner, and William J. Bowman. Dependent type systems as macros. PACMPL, 4(POPL):3:1-3:29, 2020. URL: https://doi.org/10.1145/3371071.
  12. Stephen Chang, Alex Knauth, and Ben Greenman. Type systems as macros. In POPL, pages 694-705. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009886.
  13. David R. Christiansen and Edwin C. Brady. Elaborator reflection: Extending Idris in Idris. In ICFP, pages 284-297. ACM, 2016. URL: https://doi.org/10.1145/2951913.2951932.
  14. David Raymond Christiansen. Dependent type providers. In WGP, pages 25-34. ACM, 2013. URL: https://doi.org/10.1145/2502488.2502495.
  15. William D. Clinger and Jonathan Rees. Macros that work. In POPL, pages 155-162. ACM, 1991. URL: https://doi.org/10.1145/99583.99607.
  16. William D. Clinger and Mitchell Wand. Hygienic macro technology. PACMPL, 4(HOPL):80:1-80:110, 2020. URL: https://doi.org/10.1145/3386330.
  17. Clojure Contributors. Software: Clojure/tools.macro. . Accessed 2024-01-18. URL: https://github.com/clojure/tools.macro.
  18. Clojure Contributors. Clojure macros, 2024. . Accessed 2024-01-17. URL: https://clojure.org/reference/macros.
  19. Clojure Contributors. Clojure metadata documentation, 2024. . Accessed 2024-01-17. URL: https://clojure.org/reference/metadata.
  20. Ryan Culpepper. Fortifying macros. Journal of Functional Programming, 22(4-5):439-476, 2012. URL: https://doi.org/10.1017/S0956796812000275.
  21. Ryan Culpepper, Sam Tobin-Hochstadt, and Matthew Flatt. Advanced macrology and the implementation of Typed Scheme. In SFP. Université Laval, DIUL-RT-0701, pages 1-14, 2007. URL: http://www2.ift.ulaval.ca/~dadub100/sfp2007/procPaper1.pdf.
  22. Werner Dietl, Stephanie Dietzel, Michael D. Ernst, Kıvanç Muşlu, and Todd W. Schiller. Building and using pluggable type checkers. In ICSE, pages 681-690, 2011. URL: https://doi.org/10.1145/1985793.1985889.
  23. R. Kent Dybvig. Chez Scheme Users Guide. Cadence Research Systems, 2nd edition, 2011. Google Scholar
  24. Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. A metaprogramming framework for formal verification. PACMPL, 1(ICFP):34:1-34:29, 2017. URL: https://doi.org/10.1145/3110278.
  25. ECMA International. ECMAScript language specification: 11.2.2 strict mode code, 2024. URL: https://262.ecma-international.org/15.0/index.html#sec-strict-mode-code.
  26. Richard A. Eisenberg and Stephanie Weirich. Dependently typed programming with singletons. In Haskell, pages 117-130. ACM, 2012. URL: https://doi.org/10.1145/2364506.2364522.
  27. Elixir Contributors. Elixir macro documentation, 2024. . Accessed 2024-01-17. URL: https://hexdocs.pm/elixir/1.16/Macro.html.
  28. Elixir Contributors. Elixir standard library, 2024. . Accessed 2024-01-17. URL: https://hexdocs.pm/elixir/1.16.0/Kernel.html.
  29. Matthias Felleisen. Software: 7GUI, 2020. . Accessed 2023-12-21. URL: https://github.com/mfelleisen/7GUI.
  30. David Fisher and Olin Shivers. Building language towers with Ziggurat. Journal of Functional Programming, 18(5-6):707-780, 2008. URL: https://doi.org/10.1017/S0956796808006928.
  31. Matthew Flatt. Composable and compilable macros: You want it when? In ICFP, pages 72-83. ACM, 2002. URL: https://doi.org/10.1145/581478.581486.
  32. Matthew Flatt. Binding as sets of scopes. In POPL, pages 705-717, 2016. URL: https://doi.org/10.1145/2837614.2837620.
  33. Matthew Flatt, Taylor Allred, Nia Angle, Stephen De Gabrielle, Robert Bruce Findler, Jack Firth, Kiran Gopinathan, Ben Greenman, Siddhartha Kasivajhula, Alex Knauth, Jay McCarthy, Sam Phillips, Sorawee Porncharoenwase, Jens Axel Søgaard, and Sam Tobin-Hochstadt. Rhombus: A new spin on macros without all the parentheses. PACMPL, 7(OOPSLA2), 2023. URL: https://doi.org/10.1145/3622818.
  34. Matthew Flatt, Ryan Culpepper, David Darais, and Robert Bruce Findler. Macros that work together: Compile-time bindings, partial expansion, and definition contexts. Journal of Functional Programming, 22(2):181-216, 2012. URL: https://doi.org/10.1017/S0956796812000093.
  35. Kimball Germane, Jay McCarthy, Michael D. Adams, and Matthew Might. Demand control-flow analysis. In VMCAI, pages 226-246. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-11245-5_11.
  36. GitHub. GitHub search: use Phoenix.VerifiedRoutes in Elixir, 2024. . Accessed 2024-01-17. URL: https://github.com/search?q=%22use+Phoenix.VerifiedRoutes%22+AND+%22def+verified_routes%22+language%3AElixir&type=code.
  37. Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, and Derek Dreyer. How to make ad hoc proof automation less ad hoc. In ICFP, pages 163-175. ACM, 2011. URL: https://doi.org/10.1145/2034773.2034798.
  38. Thomas R. G. Green and Marian Petre. Usability analysis of visual programming environments: A `cognitive dimensions' framework. Journal of Visual Languages and Computing, 7(2):131-174, 1996. URL: https://doi.org/10.1006/JVLC.1996.0009.
  39. Michael Greenberg. The dynamic practice and static theory of gradual typing. In SNAPL, pages 6:1-6:20. Schloss Dagstuhl, 2019. URL: https://doi.org/10.4230/LIPICS.SNAPL.2019.6.
  40. Ben Greenman. Type Tailoring, 2017. . Accessed 2024-01-08. URL: https://blog.racket-lang.org/2017/04/type-tailoring.html.
  41. Ben Greenman. Trivial: Type tailored library functions, 2020. . Accessed 2024-01-07. URL: https://docs.racket-lang.org/trivial/index.html.
  42. Ben Greenman. GTP benchmarks for gradual typing performance. In REP, pages 102-114. ACM, 2023. URL: https://doi.org/10.1145/3589806.3600034.
  43. Adam Gundry. A typechecker plugin for units of measure: Domain-specific constraint solving in GHC Haskell. In Haskell, pages 11-22. ACM, 2015. URL: https://doi.org/10.1145/2804302.2804305.
  44. Susumu Hayashi. Singleton, union and intersection types for program extraction. Information and Computation, 109(1/2):174-210, 1994. URL: https://doi.org/10.1006/INCO.1994.1016.
  45. David Herman and Philippe Meunier. Improving the static analysis of embedded languages via partial evaluation. In ICFP, pages 16-27. ACM, 2004. URL: https://doi.org/10.1145/1016850.1016857.
  46. Joel Jakubovic, Jonathan Edwards, and Tomas Petricek. Technical dimensions of programming systems. Programming, 7(3), 2023. URL: https://doi.org/10.22152/PROGRAMMING-JOURNAL.ORG/2023/7/13.
  47. Guy L. Steele Jr. Growing a language. In Addendum to OOPSLA. ACM, 1998. URL: https://doi.org/10.1145/346852.346922.
  48. Julia Contributors. Julia AST documentation, 2024. . Accessed 2024-01-17. URL: https://docs.julialang.org/en/v1/devdocs/ast/.
  49. Julia Contributors. Julia metaprogramming, 2024. . Accessed 2024-01-17. URL: https://docs.julialang.org/en/v1/manual/metaprogramming/.
  50. Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S. Foster, and David Van Horn. Type-level computations for Ruby libraries. In PLDI, pages 966-979. ACM, 2019. URL: https://doi.org/10.1145/3314221.3314630.
  51. Daniel Keep and Lukas Wirth. The little book of Rust macros, 2024. . Accessed 2024-01-17. URL: https://veykril.github.io/tlborm/proc-macros/hygiene.html.
  52. Oleg Kiselyov. Reconciling abstraction with high performance: A MetaOCaml approach. Foundations and Trendsregistered in Programming Languages, 5(1):1-101, 2018. URL: https://doi.org/10.1561/2500000038.
  53. Eugen Kiss. 7GUIs: A GUI programming benchmark. . Accessed 2023-12-21. URL: https://eugenkiss.github.io/7guis/.
  54. Eugen Kiss. Comparison of Object-Oriented and Functional Programming for GUI Development. PhD thesis, Leibniz Universitaet Hannover, 2014. Google Scholar
  55. Eugene E. Kohlbecker, Daniel P. Friedman, Matthias Felleisen, and Bruce F. Duba. Hygienic macro expansion. In LFP, pages 151-161. ACM, 1986. URL: https://doi.org/10.1145/319838.319859.
  56. Eugene E. Kohlbecker and Mitchell Wand. Macro-by-example: Deriving syntactic transformations from their specifications. In POPL, pages 77-84. ACM, 1987. URL: https://doi.org/10.1145/41625.41632.
  57. Pepijn Kokke and Wouter Swierstra. Auto in Agda - programming proof search using reflection. In MPC, pages 276-301. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-19797-5_14.
  58. Joomy Korkut and David Thrane Christiansen. Extensible type-directed editing. In TyDe, pages 38-50. ACM, 2018. URL: https://doi.org/10.1145/3240719.3241791.
  59. LaunchBadge. Software: SQLx, 2023. . Accessed 2024-01-17. URL: https://github.com/launchbadge/sqlx.
  60. Fredrik Lindblad and Marcin Benke. A tool for automated theorem proving in Agda. In TYPES, pages 154-169. Springer, 2004. URL: https://doi.org/10.1007/11617990_10.
  61. Yiyun Liu and Stephanie Weirich. Dependently-typed programming with logical equality reflection. PACMPL, 7(ICFP):210:1-210:37, 2023. URL: https://doi.org/10.1145/3607852.
  62. Florian Lorenzen and Sebastian Erdweg. Sound type-dependent syntactic language extension. In POPL, pages 204-216. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837644.
  63. Gregory Malecha and Jesper Bengtson. Extensible and efficient automation through reflective tactics. In ESOP, pages 532-559. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_21.
  64. Michał Marczyk. Answer to "does Clojure have identifier macros?". . Accessed 2024-01-18. URL: https://stackoverflow.com/a/33426863/7327755.
  65. Chris McCord. Phoenix 1.7.0 released: Built-in Tailwind, Verified Routes, LiveView Streams, and what’s next, 2023. . Accessed 2024-01-17. URL: https://phoenixframework.org/blog/phoenix-1.7-final-released.
  66. Alp Mestanogullari, Sönke Hahn, Julian K. Arni, and Andres Löh. Type-level web APIs with Servant: An exercise in domain-specific generic programming. In WGP, pages 1-12. ACM, 2015. URL: https://doi.org/10.1145/2808098.2808099.
  67. Ana L. Milanova and Wei Huang. Inference and checking of context-sensitive pluggable types. In FSE, page 26. ACM, 2012. URL: https://doi.org/10.1145/2393596.2393626.
  68. David A. Moon. MACLISP reference manual, Revision 0. Technical report, MIT Project MAC, 1974. Google Scholar
  69. Multiple Authors. Language: Macros, 2023. . Accessed 2024-01-17. URL: https://clojure-doc.org/articles/language/macros/.
  70. OCaml Contributors. OCaml PPX, 2024. . Accessed 2024-01-17. URL: https://ocaml.org/docs/metaprogramming.
  71. Cyrus Omar, Darya Kurilova, Ligia Nistor, Benjamin Chung, Alex Potanin, and Jonathan Aldrich. Safely composable type-specific languages. In ECOOP, pages 105-130. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44202-9_5.
  72. Matthew M. Papi, Mahmood Ali, Telmo Luis Correa Jr., Jeff H. Perkins, and Michael D. Ernst. Practical pluggable types for Java. In ISSTA, pages 201-212. ACM, 2008. URL: https://doi.org/10.1145/1390630.1390656.
  73. Lionel Parreaux. Squid - type-safe metaprogramming for Scala, 2024. . Accessed 2024-01-17. URL: https://epfldata.github.io/squid/home.html.
  74. Lionel Parreaux, Antoine Voizard, Amir Shaikhha, and Christoph E. Koch. Unifying analytic and statically-typed quasiquotes. PACMPL, 2(POPL):13:1-13:33, 2018. URL: https://doi.org/10.1145/3158101.
  75. Tomas Petricek, Gustavo Guerra, and Don Syme. Types from data: Making structured data first-class citizens in F#. In PLDI, pages 477-490. ACM, 2016. URL: https://doi.org/10.1145/2908080.2908115.
  76. Phoenix Contributors. Phoenix verified routes, 2023. https://hexdocs.pm/phoenix/Phoenix.VerifiedRoutes.html. Accessed 2023-11-28.
  77. Justin Pombrio and Shriram Krishnamurthi. Hygienic resugaring of compositional desugaring. In ICFP, pages 75-87. ACM, 2015. URL: https://doi.org/10.1145/2784731.2784755.
  78. Racket Contributors. Racket syntax properties documentation, 2024. . Accessed 2024-01-17. URL: https://docs.racket-lang.org/reference/stxprops.html.
  79. Racket Contributors. Syntax transformers, 2024. . Accessed 2024-01-17. URL: https://docs.racket-lang.org/reference/stxtrans.html.
  80. Rhombus Contributors. Rhombus documentation: Static and dynamic lookup, 2024. . Accessed 2024-01-17. URL: https://docs.racket-lang.org/rhombus/Static_and_Dynamic_Lookup.html.
  81. Rhombus Contributors. Rhombus syntax object documentation, 2024. . Accessed 2024-01-17. URL: https://docs.racket-lang.org/rhombus/stxobj.html.
  82. Tiark Rompf. Reflections on LMS: exploring front-end alternatives. In SCALA, pages 41-50. ACM, 2016. URL: https://doi.org/10.1145/2998392.2998399.
  83. Tiark Rompf and Nada Amin. A SQL to C compiler in 500 lines of code. Journal of Functional Programming, 29:e9, 2019. URL: https://doi.org/10.1017/S0956796819000054.
  84. Tiark Rompf and Martin Odersky. Lightweight modular staging: A pragmatic approach to runtime code generation and compiled DSLs. In GPCE, pages 127-136. ACM, 2010. URL: https://doi.org/10.1145/1868294.1868314.
  85. Tiark Rompf, Arvind K. Sujeeth, Nada Amin, Kevin J. Brown, Vojin Jovanovic, HyoukJoong Lee, Manohar Jonnalagedda, Kunle Olukotun, and Martin Odersky. Optimizing data structures in high-level programs: New directions for extensible compilers based on staging. In POPL, pages 497-510. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429128.
  86. Rust Contributors. Rust macros, 2024. . Accessed 2024-01-17. URL: https://doc.rust-lang.org/reference/procedural-macros.html.
  87. Scala 3 Contributors. Scala 3 macros, 2024. . Accessed 2024-01-17. URL: https://docs.scala-lang.org/scala3/guides/macros/macros.html.
  88. Scala 3 Contributors. Scala 3 reference: Macros, 2024. . Accessed 2024-01-17. URL: https://docs.scala-lang.org/scala3/reference/metaprogramming/macros.html.
  89. SciML Contributors. Software: OrdinaryDiffEq.jl, 2024. . Accessed 2024-01-17. URL: https://github.com/SciML/OrdinaryDiffEq.jl.
  90. Tim Sheard and Simon Peyton Jones. Template meta-programming for Haskell. In Haskell, pages 1-16. ACM, 2002. URL: https://doi.org/10.1145/581690.581691.
  91. Olin Shivers. Control-flow analysis in Scheme. In PLDI, pages 164-174. ACM, 1988. URL: https://doi.org/10.1145/53990.54007.
  92. Jeremy G. Siek and Walid Taha. Gradual typing for functional languages. In SFP. University of Chicago, TR-2006-06, pages 81-92, 2006. URL: http://scheme2006.cs.uchicago.edu/scheme2006.pdf.
  93. Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. Refined criteria for gradual typing. In SNAPL, pages 274-293. Schloss Dagstuhl, 2015. URL: https://doi.org/10.4230/LIPICS.SNAPL.2015.274.
  94. Suzanne Soy. Software: type-expander, 2020. . Accessed 2023-12-21. URL: https://github.com/SuzanneSoy/type-expander.
  95. Eric Spishak, Werner Dietl, and Michael D. Ernst. A type system for regular expressions. In FTfJP, pages 20-26. ACM, 2012. URL: https://doi.org/10.1145/2318202.2318207.
  96. Antonis Stampoulis and Zhong Shao. VeriML: Typed computation of logical terms inside a language with effects. In ICFP, pages 333-344. ACM, 2010. URL: https://doi.org/10.1145/1863543.1863591.
  97. StaticArrays Contributors. StaticArrays, 2024. . Accessed 2024-01-17. URL: https://juliahub.com/ui/Packages/General/StaticArrays/.
  98. Guy L. Steele, Jr. Common Lisp. Digital Press, 2nd edition, 1990. Google Scholar
  99. T. Stephen Strickland, Sam Tobin-Hochstadt, and Matthias Felleisen. Practical variable-arity polymorphism. In ESOP, pages 32-46, 2009. URL: https://doi.org/10.1007/978-3-642-00590-9_3.
  100. Satish Thatte. Quasi-static typing. In POPL, pages 367-381, 1990. URL: https://doi.org/10.1145/96709.96747.
  101. Sam Tobin-Hochstadt and Matthias Felleisen. Interlanguage migration: from scripts to programs. In DLS, pages 964-974, 2006. URL: https://doi.org/10.1145/1176617.1176755.
  102. Sam Tobin-Hochstadt and Matthias Felleisen. The design and implementation of Typed Scheme. In POPL, pages 395-406, 2008. URL: https://doi.org/10.1145/1328438.1328486.
  103. Sam Tobin-Hochstadt, Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland, and Asumu Takikawa. Migratory typing: Ten years later. In SNAPL, pages 17:1-17:17. Schloss Dagstuhl, 2017. URL: https://doi.org/10.4230/LIPICS.SNAPL.2017.17.
  104. Sam Tobin-Hochstadt, Vincent St-Amour, Ryan Culpepper, Matthew Flatt, and Matthias Felleisen. Languages as libraries. In PLDI, pages 132-141, 2011. URL: https://doi.org/10.1145/1993498.1993514.
  105. José Valim. Nx: Numerical Elixir, 2023. . Accessed 2024-01-16. URL: https://github.com/elixir-nx/nx.
  106. David Van Horn. Software: zombie, 2020. . Accessed 2023-02-20. URL: https://github.com/philnguyen/soft-contract/tree/master/soft-contract/benchmark-contract-overhead.
  107. Stephanie Weirich. The influence of dependent types (keynote). SIGPLAN Notices, 52(1), 2017. URL: https://doi.org/10.1145/3093333.3009923.
  108. Ashton Wiersdorf, Stephen Chang, Matthias Felleisen, and Ben Greenman. Artifact for Type Tailoring (ECOOP 2024), July 2024. URL: https://doi.org/10.5281/zenodo.12726060.
  109. Hongwei Xi. Dependent ML: An approach to practical programming with dependent types. Journal of Functional Programming, 17(2):215-286, 2007. URL: https://doi.org/10.1017/S0956796806006216.
  110. Ningning Xie, Leo White, Olivier Nicole, and Jeremy Yallop. MacoCaml: Staging composable and compilable macros. PACMPL, 7(ICFP), 2023. URL: https://doi.org/10.1145/3607851.
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