{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:56Z","timestamp":1779836756248,"version":"3.53.1"},"reference-count":52,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2020,8,6]],"date-time":"2020-08-06T00:00:00Z","timestamp":1596672000000},"content-version":"unspecified","delay-in-days":218,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    In ML-style module type theory, sealing often leads to situations in which type variables must leave scope, and this creates a need for signatures that avoid such variables. Unfortunately, in general, there is no best signature that avoids a variable, so modules do not always enjoy principal signatures. This observation is called the\n                    <jats:italic>avoidance problem.<\/jats:italic>\n                    In the past, the problem has been circumvented using a variety of devices for moving variables so they can remain in scope. These devices work, but have heretofore lacked a logical foundation. They have also lacked a presentation in which the dynamic semantics is given on the same phrases as the static semantics, which limits their applications. We can provide a best supersignature avoiding a variable by fiat, by adding an existential signature that is the least upper bound of its instances. This idea is old, but a workable metatheory has not previously been worked out. This work resolves the metatheoretic issues using ideas borrowed from focused logic. We show that the new theory results in a type discipline very similar to the aforementioned devices used in prior work. In passing, this gives a type-theoretic justification for the generative stamps used in the early days of the static semantics of ML modules. All the proofs are formalized in Coq.\n                  <\/jats:p>","DOI":"10.1017\/s0956796820000222","type":"journal-article","created":{"date-parts":[[2020,8,6]],"date-time":"2020-08-06T03:44:08Z","timestamp":1596685448000},"source":"Crossref","is-referenced-by-count":5,"title":["A focused solution to the avoidance problem"],"prefix":"10.1017","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1556-2183","authenticated-orcid":false,"given":"KARL","family":"CRARY","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2020,8,6]]},"reference":[{"key":"S0956796820000222_ref6","doi-asserted-by":"crossref","unstructured":"Crary, K. (2018, July) Strong sums in focused logic. In Thirty-Third IEEE Symposium on Logic in Computer Science, pp. 265\u2013274.","DOI":"10.1145\/3209108.3209145"},{"key":"S0956796820000222_ref19","doi-asserted-by":"crossref","unstructured":"Harper, R. & Stone, C. (2000) A type-theoretic interpretation of Standard ML. In Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT. Extended version published as CMU Technical Report CMU-CS-97-147, pp. 341\u2013387.","DOI":"10.7551\/mitpress\/5641.003.0019"},{"key":"S0956796820000222_ref21","doi-asserted-by":"crossref","unstructured":"Harper, R. , Mitchell, J. C. & Moggi, E. (1990, January) Higher-order modules and the phase distinction. In Seventeenth ACM Symposium on Principles of Programming Languages, pp. 341\u2013354.","DOI":"10.1145\/96709.96744"},{"key":"S0956796820000222_ref2","doi-asserted-by":"crossref","unstructured":"Biswas, S. K. (1995) Higher-order functors with transparent signatures. In Twenty-Second ACM Symposium on Principles of Programming Languages, pp. 154\u2013163.","DOI":"10.1145\/199448.199478"},{"key":"S0956796820000222_ref22","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","article-title":"A framework for defining logics","volume":"40","author":"Harper","year":"1993","journal-title":"J. ACM"},{"key":"S0956796820000222_ref29","doi-asserted-by":"crossref","unstructured":"Licata, D. R. , Zeilberger, N. & Harper, R. (2008) Focusing on binding and computation. In Twenty-Third IEEE Symposium on Logic in Computer Science.","DOI":"10.1109\/LICS.2008.48"},{"key":"S0956796820000222_ref31","volume-title":"The Definition of Standard ML","author":"Milner","year":"1990"},{"key":"S0956796820000222_ref25","doi-asserted-by":"crossref","unstructured":"Leroy, X. (1994, January). Manifest types, modules and separate compilation. In Twenty-First ACM Symposium on Principles of Programming Languages, pp. 109\u2013122.","DOI":"10.1145\/174675.176926"},{"key":"S0956796820000222_ref17","doi-asserted-by":"crossref","unstructured":"Harper, R. & Lillibridge, M. (1994, January) A type-theoretic approach to higher-order modules with sharing. In Twenty-First ACM Symposium on Principles of Programming Languages, pp. 123\u2013137.","DOI":"10.1145\/174675.176927"},{"key":"S0956796820000222_ref33","first-page":"470","article-title":"Trans. Program. Lang.","volume":"10","author":"Mitchell","year":"1988","journal-title":"Syst."},{"key":"S0956796820000222_ref36","unstructured":"Reynolds, J. C. (1983) Types, abstraction and parametric polymorphism. In Information Processing 1983, Proceedings of the IFIP 9th World Computer Congress. North-Holland, pp. 513\u2013523."},{"key":"S0956796820000222_ref37","doi-asserted-by":"crossref","unstructured":"Rossberg, A. (2015) 1ML \u2014 core and modules united. In 2015 ACM International Conference on Functional Programming, pp. 35\u201347.","DOI":"10.1145\/2858949.2784738"},{"key":"S0956796820000222_ref39","unstructured":"Russo, C. V. (1998, March) Types for modules. Ph.D. thesis, Edinburgh University."},{"key":"S0956796820000222_ref32","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML (revised)","author":"Milner","year":"1997"},{"key":"S0956796820000222_ref35","unstructured":"Plotkin, G. D. (1981) A structural approach to operational semantics. Technical report. DAIMI FN-19. Computer Science Department, Aarhus University."},{"key":"S0956796820000222_ref41","unstructured":"Schack-Nielsen, A. (2011, January) Implementing substructural logical frameworks. Ph.D. thesis, IT University of Copenhagen, Copenhagen, Denmark."},{"key":"S0956796820000222_ref7","doi-asserted-by":"crossref","unstructured":"Crary, K. (2019, January). Fully abstract module compilation. In Forty-Sixth ACM Symposium on Principles of Programming Languages.","DOI":"10.1145\/3291650"},{"key":"S0956796820000222_ref43","unstructured":"Simmons, R. J. (2012, November). Substructural logical specifications. Ph.D. thesis, Carnegie Mellon University, School of Computer Science, Pittsburgh, Pennsylvania."},{"key":"S0956796820000222_ref45","unstructured":"Stone, C. A. (2000, August). Singleton kinds and singleton types. Ph.D. thesis, Carnegie Mellon University, School of Computer Science, Pittsburgh, Pennsylvania."},{"key":"S0956796820000222_ref10","doi-asserted-by":"crossref","unstructured":"Dreyer, D. , Crary, K. & Harper, R (2003, January). A type system for higher-order modules. In Thirtieth ACM Symposium on Principles of Programming Languages, pp. 236\u2013249.","DOI":"10.1145\/640128.604151"},{"key":"S0956796820000222_ref27","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0956796800001933","article-title":"A syntactic theory of type generativity and sharing","volume":"6","author":"Leroy","year":"1996","journal-title":"J. Funct. Program."},{"key":"S0956796820000222_ref44","doi-asserted-by":"crossref","unstructured":"Simmons, R. J. (2014) Structural focalization. ACM Trans. Comput. Logic, 15(3).","DOI":"10.1145\/2629678"},{"key":"S0956796820000222_ref20","doi-asserted-by":"crossref","unstructured":"Harper, R. , Milner, R. & Tofte, M. (1987) A type discipline for program modules. In TAPSOFT 1987: Proceedings of the International Joint Conference on Theory and Practice of Software Development. Lecture Notes in Computer Science, vol. 250 Springer, pp. 308\u2013319.","DOI":"10.1007\/BFb0014988"},{"key":"S0956796820000222_ref12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1997.2627","article-title":"Propositional lax logic","volume":"137","author":"Fairtlough","year":"1997","journal-title":"Inform. Comput."},{"key":"S0956796820000222_ref26","doi-asserted-by":"crossref","unstructured":"Leroy, X. (1995, January) Applicative functors and fully transparent higher-order modules. In Twenty-Second ACM Symposium on Principles of Programming Languages.","DOI":"10.1145\/199448.199476"},{"key":"S0956796820000222_ref34","doi-asserted-by":"crossref","unstructured":"Moggi, E. (1989) Computational lambda-calculus and monads. In Fourth IEEE Symposium on Logic in Computer Science, pp. 14\u201323.","DOI":"10.1109\/LICS.1989.39155"},{"key":"S0956796820000222_ref16","unstructured":"Harper, R. (2011) The Holy Trinity. Blog post at https:\/\/existentialtype.wordpress.com\/2011\/03\/27\/the-holy-trinity\/"},{"key":"S0956796820000222_ref50","doi-asserted-by":"crossref","unstructured":"Watkins, K. , Cervesato, I. , Pfenning, F. & Walker, D. (2002) A concurrent logical framework I: Judgments and properties. Technical report. CMU-CS-02-101. Carnegie Mellon University, School of Computer Science. Revised May 2003.","DOI":"10.21236\/ADA418517"},{"key":"S0956796820000222_ref28","doi-asserted-by":"crossref","unstructured":"Levy, P. B. (1999, April) Call-by-push-value: A subsuming paradigm. In 1999 International Conference on Typed Lambda Calculi and Applications, pp. 228\u2013243.","DOI":"10.1007\/3-540-48959-2_17"},{"key":"S0956796820000222_ref42","doi-asserted-by":"crossref","unstructured":"Shao, Z. (1999, September). Transparent modules with fully syntactic signatures. In 1999 ACM International Conference on Functional Programming, pp. 220\u2013232.","DOI":"10.1145\/317765.317801"},{"key":"S0956796820000222_ref18","first-page":"211","article-title":"Trans. Program. Lang.","volume":"15","author":"Harper","year":"1993","journal-title":"Syst."},{"key":"S0956796820000222_ref47","unstructured":"Stone, C. A. & Harper, R. (2006) Extensional equivalence and singleton types. ACM Trans. Computat. Log. 7(4). An earlier version appeared in the 2000 Symposium on Principles of Programming Languages."},{"key":"S0956796820000222_ref24","doi-asserted-by":"crossref","unstructured":"Lee, D. K. , Crary, K. & Harper, R. (2007, January) Towards a mechanized metatheory of Standard ML. In Thirty-Fourth ACM Symposium on Principles of Programming Languages, pp. 173\u2013184.","DOI":"10.1145\/1190215.1190245"},{"key":"S0956796820000222_ref40","first-page":"348","article-title":"First-class structures for Standard ML","volume":"7","author":"Russo","year":"2000","journal-title":"Nord. J. Comput."},{"key":"S0956796820000222_ref38","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1017\/S0956796814000264","article-title":"F-ing modules","volume":"24","author":"Rossberg","year":"2014","journal-title":"J. Funct. Program."},{"key":"S0956796820000222_ref48","doi-asserted-by":"crossref","unstructured":"Swasey, D. , Murphy, T. VII , Crary, K. & Harper, R. (2006) A separate compilation extension to Standard ML. In Workshop on ML.","DOI":"10.21236\/ADA457137"},{"key":"S0956796820000222_ref49","unstructured":"VanInwegen, M. (1996, May) The machine-assisted proof of programming language properties. Ph.D. thesis, University of Pennsylvania, Philadelphia, Pennsylvania."},{"key":"S0956796820000222_ref4","doi-asserted-by":"crossref","unstructured":"Crary, K. (2009) A syntactic account of singleton types via hereditary substitution. In 2009 Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, pp. 21\u201329.","DOI":"10.1145\/1577824.1577829"},{"key":"S0956796820000222_ref15","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","article-title":"The undecidability of the second-order unification problem","volume":"13","author":"Goldfarb","year":"1981","journal-title":"Theor. Comput. Sci."},{"key":"S0956796820000222_ref5","doi-asserted-by":"crossref","unstructured":"Crary, K. (2017, January). Modules, abstraction, and parametric polymorphism. In Forty-Fourth ACM Symposium on Principles of Programming Languages, pp. 100\u2013113.","DOI":"10.1145\/3093333.3009892"},{"key":"S0956796820000222_ref11","unstructured":"Elliott, C. M. (1990, May) Extensions and applications of higher-order unification. Ph.D. thesis, Carnegie Mellon University, School of Computer Science, Pittsburgh, Pennsylvania."},{"key":"S0956796820000222_ref51","doi-asserted-by":"crossref","unstructured":"Watkins, K. , Cervesato, I. , Pfenning, F. & Walker, D. (2004). A concurrent logical framework: The propositional fragment. In Types for Proofs and Programs, Berardi, S. , Coppo, M. & Damiani, F. (eds), Lecture Notes in Computer Science, vol. 3085. Springer, pp. 355\u2013377. Papers from the Third International Workshop on Types for Proofs and Programs, April 2003, Torino, Italy.","DOI":"10.1007\/978-3-540-24849-1_23"},{"key":"S0956796820000222_ref1","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","article-title":"Logic programming with focusing proofs in linear logic","volume":"2","author":"Andreoli","year":"1992","journal-title":"J. Logic Comput."},{"key":"S0956796820000222_ref13","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/S0304-3975(96)00300-3","article-title":"Bounded existentials and minimal typing","volume":"193","author":"Ghelli","year":"1998","journal-title":"Theor. Comput. Sci."},{"key":"S0956796820000222_ref46","doi-asserted-by":"crossref","unstructured":"Stone, C. A. & Harper, R. (2000, January). Deciding type equivalence in a language with singleton kinds. In Twenty-Seventh ACM Symposium on Principles of Programming Languages. Extended version published as CMU Technical Report CMU-CS-99-155, pp. 214\u2013227.","DOI":"10.1145\/325694.325724"},{"key":"S0956796820000222_ref52","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1016\/j.apal.2008.01.001","article-title":"On the unity of duality","volume":"153","author":"Zeilberger","year":"2008","journal-title":"Ann. Pure Appl. Log."},{"key":"S0956796820000222_ref9","unstructured":"Dreyer, D. (2005, May). Understanding and evolving the ML module system. Ph.D. thesis, Carnegie Mellon University, School of Computer Science, Pittsburgh, Pennsylvania."},{"key":"S0956796820000222_ref23","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","article-title":"A unification algorithm for typed \u03bb-calculus","volume":"1","author":"Huet","year":"1975","journal-title":"Theor. Comput. Sci."},{"key":"S0956796820000222_ref30","unstructured":"Lillibridge, M. (1997, May). Translucent sums: A foundation for higher-order module systems. Ph.D. thesis, Carnegie Mellon University, School of Computer Science, Pittsburgh, Pennsylvania."},{"key":"S0956796820000222_ref3","doi-asserted-by":"crossref","unstructured":"Crary, K. (2007) Sound and complete elimination of singleton kinds. ACM Trans. Comput. Log. 8(2). An earlier version appeared in 2000 Workshop on Types in Compilation.","DOI":"10.1145\/1227839.1227840"},{"key":"S0956796820000222_ref8","unstructured":"Crary, K. & Harper, R. (2009) Mechanized definition of Standard ML. Available at https:\/\/www.cs.cmu.edu\/~crary\/papers\/mldef-alpha.tar.gz"},{"key":"S0956796820000222_ref14","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1016\/0168-0072(93)90093-S","article-title":"On the unity of logic","volume":"59","author":"Girard","year":"1993","journal-title":"Ann. Pure Appl. Log."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796820000222","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:51Z","timestamp":1779835011000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796820000222\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"references-count":52,"alternative-id":["S0956796820000222"],"URL":"https:\/\/doi.org\/10.1017\/s0956796820000222","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"article-number":"e24"}}