{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,9]],"date-time":"2025-12-09T15:30:10Z","timestamp":1765294210224,"version":"3.41.0"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2006,10,1]],"date-time":"2006-10-01T00:00:00Z","timestamp":1159660800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2006,10]]},"abstract":"<jats:p>\n            We study the \u03bb\n            <jats:sup>\n              \u03a0\u03a3\n              <jats:italic>S<\/jats:italic>\n            <\/jats:sup>\n            <jats:sub>\u2264<\/jats:sub>\n            calculus, which contains singleton types\n            <jats:italic>S<\/jats:italic>\n            (\n            <jats:italic>M<\/jats:italic>\n            ) classifying terms of base type provably equivalent to the term\n            <jats:italic>M<\/jats:italic>\n            . The system includes dependent types for pairs and functions (\u03a3 and \u03a0) and a subtyping relation induced by regarding singletons as subtypes of the base type. The decidability of type checking for this language is non-obvious, since to type check we must be able to determine equivalence of well-formed terms. But in the presence of singleton types, the provability of an equivalence judgment \u0393 \u22a2\n            <jats:italic>M<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            \u2261\n            <jats:italic>M<\/jats:italic>\n            <jats:sub>2<\/jats:sub>\n            :\n            <jats:italic>A<\/jats:italic>\n            can depend both on the typing context \u0393 and on the particular type\n            <jats:italic>A<\/jats:italic>\n            at which\n            <jats:italic>M<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            and\n            <jats:italic>M<\/jats:italic>\n            <jats:sub>2<\/jats:sub>\n            are compared.We show how to prove decidability of term equivalence, hence of type checking, in \u03bb\n            <jats:sup>\n              \u03a0\u03a3\n              <jats:italic>S<\/jats:italic>\n            <\/jats:sup>\n            <jats:sub>\u2264<\/jats:sub>\n            by exhibiting a type-directed algorithm for directly computing normal forms. The correctness of normalization is shown using an unusual variant of Kripke logical relations organized around sets; rather than defining a logical equivalence relation, we work directly with (subsets of) the corresponding equivalence classes.We then provide a more efficient algorithm for checking type equivalence without constructing normal forms. We also show that type checking, subtyping, and all other judgments of the system are decidable.The \u03bb\n            <jats:sup>\n              \u03a0\u03a3\n              <jats:italic>S<\/jats:italic>\n            <\/jats:sup>\n            <jats:sub>\u2264<\/jats:sub>\n            calculus models type constructors and kinds in the intermediate language used by the TILT compiler for Standard ML to implement the SML module system. The decidability of \u03bb\n            <jats:sup>\n              \u03a0\u03a3\n              <jats:italic>S<\/jats:italic>\n            <\/jats:sup>\n            <jats:sub>\u2264<\/jats:sub>\n            term equivalence allows us to show decidability of type checking for TILT's intermediate language. We also obtain a consistency result that allows us to prove type safety for the intermediate language. The algorithms derived here form the core of the type checker used for internal type checking in TILT.\n          <\/jats:p>","DOI":"10.1145\/1183278.1183281","type":"journal-article","created":{"date-parts":[[2007,1,16]],"date-time":"2007-01-16T19:38:29Z","timestamp":1168976309000},"page":"676-722","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["Extensional equivalence and singleton types"],"prefix":"10.1145","volume":"7","author":[{"given":"Christopher A.","family":"Stone","sequence":"first","affiliation":[{"name":"Harvey Mudd College, Claremont, CA"}]},{"given":"Robert","family":"Harper","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA"}]}],"member":"320","published-online":{"date-parts":[[2006,10]]},"reference":[{"key":"e_1_2_1_1_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Computer Science Logic (CSL '94)","author":"Aspinall D.","unstructured":"Aspinall , D. 1995. Subtyping with singleton types . In Proceedings of the Computer Science Logic (CSL '94) . Lecture Notes in Computer Science , vol. 933 , Springer-Verlag , New York .]] Aspinall, D. 1995. Subtyping with singleton types. In Proceedings of the Computer Science Logic (CSL '94). Lecture Notes in Computer Science, vol. 933, Springer-Verlag, New York.]]"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the Computer Science Logic (CSL","volume":"1862","author":"Aspinall D.","year":"2000","unstructured":"Aspinall , D. 2000 . Subtyping with power types . In Proceedings of the Computer Science Logic (CSL 2000). Lecture Notes in Computer Science , vol. 1862 , Springer-Verlag, New York. 156--171.]] Aspinall, D. 2000. Subtyping with power types. In Proceedings of the Computer Science Logic (CSL 2000). Lecture Notes in Computer Science, vol. 1862, Springer-Verlag, New York. 156--171.]]"},{"volume-title":"Proceedings 1997 ACM International Conference on Functional Programming (ICFP '97)","author":"Blume M.","unstructured":"Blume , M. and Appel , A. W . 1997. Lambda-splitting: A higher-order approach to cross-module optimizations . In Proceedings 1997 ACM International Conference on Functional Programming (ICFP '97) . 112--124.]] 10.1145\/258948.258960 Blume, M. and Appel, A. W. 1997. Lambda-splitting: A higher-order approach to cross-module optimizations. In Proceedings 1997 ACM International Conference on Functional Programming (ICFP '97). 112--124.]] 10.1145\/258948.258960","key":"e_1_2_1_5_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1145\/6041.6042"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1016\/S0890-5401(03)00062-2"},{"volume-title":"Logical frameworks","author":"Coquand T.","unstructured":"Coquand , T. 1991. An algorithm for testing conversion in type theory . In Logical frameworks , G. Huet and G. Plotkin, Eds. Cambridge University Press , Cambridge, MA , 255--277.]] Coquand, T. 1991. An algorithm for testing conversion in type theory. In Logical frameworks, G. Huet and G. Plotkin, Eds. Cambridge University Press, Cambridge, MA, 255--277.]]","key":"e_1_2_1_8_1"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the Typed Lambda Calculi and Applications (TLCA","volume":"2701","author":"Coquand T.","year":"2003","unstructured":"Coquand , T. , Pollack , R. , and Takeyama , M . 2003. A logical framework with dependently typed records . In Proceedings of the Typed Lambda Calculi and Applications (TLCA 2003 ). 105--119. (Available as LNCS 2701). Lecture Notes in Computer Science , vol. 2701 , Springer-Verlag, New York.]] Coquand, T., Pollack, R., and Takeyama, M. 2003. A logical framework with dependently typed records. In Proceedings of the Typed Lambda Calculi and Applications (TLCA 2003). 105--119. (Available as LNCS 2701). Lecture Notes in Computer Science, vol. 2701, Springer-Verlag, New York.]]"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the Second Workshop on Intersection Types and Related Systems (ITRS '02)","volume":"70","author":"Courant J.","year":"2002","unstructured":"Courant , J. 2002 . Strong normalization with singleton types . In Proceedings of the Second Workshop on Intersection Types and Related Systems (ITRS '02) . ENTCS, vol. 70 .]] Courant, J. 2002. Strong normalization with singleton types. In Proceedings of the Second Workshop on Intersection Types and Related Systems (ITRS '02). ENTCS, vol. 70.]]"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 1999 ACM International Conference on Functional Programming (ICFP '99)","author":"Crary K.","year":"1999","unstructured":"Crary , K. 1999 . A simple proof technique for certain parametricity results . In Proceedings of the 1999 ACM International Conference on Functional Programming (ICFP '99) . ACM, New York, 82--89.]] 10.1145\/317636.317787 Crary, K. 1999. A simple proof technique for certain parametricity results. In Proceedings of the 1999 ACM International Conference on Functional Programming (ICFP '99). ACM, New York, 82--89.]] 10.1145\/317636.317787"},{"volume-title":"Advanced Topics in Types and Programming Languages","author":"Crary K.","unstructured":"Crary , K. 2005. Logical relations and a case study in equivalence checking . In Advanced Topics in Types and Programming Languages , B. C. Pierce, Ed. MIT Press, Cambridge , MA .]] Crary, K. 2005. Logical relations and a case study in equivalence checking. In Advanced Topics in Types and Programming Languages, B. C. Pierce, Ed. MIT Press, Cambridge, MA.]]","key":"e_1_2_1_13_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1006\/inco.1994.1014"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (POPL '05)","author":"Goguen H.","year":"2005","unstructured":"Goguen , H. 2005 . A syntactic approach to eta equality in type theory . In Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (POPL '05) . ACM, New York.]] 10.1145\/1040305.1040312 Goguen, H. 2005. A syntactic approach to eta equality in type theory. In Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (POPL '05). ACM, New York.]] 10.1145\/1040305.1040312"},{"volume-title":"Proceedings of the 21st ACM Symposium on Principles of Programming Languages (POPL '94)","author":"Harper R.","unstructured":"Harper , R. and Lillibridge , M . 1994. A type-theoretic approach to higher-order modules with sharing . In Proceedings of the 21st ACM Symposium on Principles of Programming Languages (POPL '94) . ACM, New York, 123--137.]] 10.1145\/174675.176927 Harper, R. and Lillibridge, M. 1994. A type-theoretic approach to higher-order modules with sharing. In Proceedings of the 21st ACM Symposium on Principles of Programming Languages (POPL '94). ACM, New York, 123--137.]] 10.1145\/174675.176927","key":"e_1_2_1_19_1"},{"volume-title":"Proceedings of the 17th ACM Symposium on Principles of Programming Languages (POPL '90)","author":"Harper R.","unstructured":"Harper , R. , Mitchell , J. C. , and Moggi , E . 1990. Higher-order modules and the phase distinction . In Proceedings of the 17th ACM Symposium on Principles of Programming Languages (POPL '90) . ACM, New York, 341--354.]] 10.1145\/96709.96744 Harper, R., Mitchell, J. C., and Moggi, E. 1990. Higher-order modules and the phase distinction. In Proceedings of the 17th ACM Symposium on Principles of Programming Languages (POPL '90). ACM, New York, 341--354.]] 10.1145\/96709.96744","key":"e_1_2_1_20_1"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the 22nd ACM Symposium on Principles of Programming Languages (POPL '95)","author":"Harper R.","year":"1994","unstructured":"Harper , R. and Morrisett , G . 1995. Compiling polymorphism using intensional type analysis . In Proceedings of the 22nd ACM Symposium on Principles of Programming Languages (POPL '95) . ACM, New York, 130--141.]] 10.1145\/ 1994 48.199475 Harper, R. and Morrisett, G. 1995. Compiling polymorphism using intensional type analysis. In Proceedings of the 22nd ACM Symposium on Principles of Programming Languages (POPL '95). ACM, New York, 130--141.]] 10.1145\/199448.199475"},{"volume-title":"Proceedings of the Workshop on Logical Frameworks and Meta-Languages. Extended version available as Tech. Rep. CMU-CS-99-159","author":"Harper R.","unstructured":"Harper , R. and Pfenning , F . 1999. On equivalence and canonical forms in the LF type theory . In Proceedings of the Workshop on Logical Frameworks and Meta-Languages. Extended version available as Tech. Rep. CMU-CS-99-159 .]] Harper, R. and Pfenning, F. 1999. On equivalence and canonical forms in the LF type theory. In Proceedings of the Workshop on Logical Frameworks and Meta-Languages. Extended version available as Tech. Rep. CMU-CS-99-159.]]","key":"e_1_2_1_22_1"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 21st ACM Symposium on Principles of Programming Languages (POPL '94)","author":"Leroy X.","year":"1994","unstructured":"Leroy , X. 1994 . Manifest types, modules, and separate compilation . In Proceedings of the 21st ACM Symposium on Principles of Programming Languages (POPL '94) . ACM, New York, 109--122.]] 10.1145\/174675.176926 Leroy, X. 1994. Manifest types, modules, and separate compilation. In Proceedings of the 21st ACM Symposium on Principles of Programming Languages (POPL '94). ACM, New York, 109--122.]] 10.1145\/174675.176926"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the 22nd ACM Symposium on Principles of Programming Languages (POPL '95)","author":"Leroy X.","year":"1995","unstructured":"Leroy , X. 1995 . Applicative Functors and Fully Transparent Higher-Order Modules . In Proceedings of the 22nd ACM Symposium on Principles of Programming Languages (POPL '95) . ACM, New York, 142--153.]] 10.1145\/ 199448.199476 Leroy, X. 1995. Applicative Functors and Fully Transparent Higher-Order Modules. In Proceedings of the 22nd ACM Symposium on Principles of Programming Languages (POPL '95). ACM, New York, 142--153.]] 10.1145\/199448.199476"},{"unstructured":"Lillibridge M. 1997. Translucent Sums: A Foundation for Higher-Order Module Systems. Ph.D. dissertation School of Computer Science Carnegie Mellon University. (Available as Technical Report) CMU-CS-97-122.]]  Lillibridge M. 1997. Translucent Sums: A Foundation for Higher-Order Module Systems. Ph.D. dissertation School of Computer Science Carnegie Mellon University. (Available as Technical Report) CMU-CS-97-122.]]","key":"e_1_2_1_26_1"},{"unstructured":"Martin-L\u00f6f P. 1984. Intuitionistic Type Theory. Bibliopolis-Napoli.]]  Martin-L\u00f6f P. 1984. Intuitionistic Type Theory. Bibliopolis-Napoli.]]","key":"e_1_2_1_27_1"},{"volume-title":"Proceedings of the 23rd ACM Symposium on Principles of Programming Languages (POPL '96)","author":"Minamide Y.","unstructured":"Minamide , Y. , Morrisett , G. , and Harper , R . 1996. Typed closure conversion . In Proceedings of the 23rd ACM Symposium on Principles of Programming Languages (POPL '96) . ACM, New York, 271--283.]] 10.1145\/237721.237791 Minamide, Y., Morrisett, G., and Harper, R. 1996. Typed closure conversion. In Proceedings of the 23rd ACM Symposium on Principles of Programming Languages (POPL '96). ACM, New York, 271--283.]] 10.1145\/237721.237791","key":"e_1_2_1_28_1"},{"key":"e_1_2_1_29_1","volume-title":"Tech. Rep. TR97-1651, Department of Computer Science","author":"Morrisett G.","year":"1997","unstructured":"Morrisett , G. , Walker , D. , Crary , K. , and Glew , N . 1997 . From system F to typed assembly language. Tech. Rep. TR97-1651, Department of Computer Science , Cornell University.]] Morrisett, G., Walker, D., Crary, K., and Glew, N. 1997. From system F to typed assembly language. Tech. Rep. TR97-1651, Department of Computer Science, Cornell University.]]"},{"key":"e_1_2_1_30_1","volume-title":"Tech. Rep. CMU-CS-00-180, School of Computer Science","author":"Petersen L.","year":"2000","unstructured":"Petersen , L. , Cheng , P. , Harper , R. , and Stone, C. 2000 . Implementing the TILT internal language. Tech. Rep. CMU-CS-00-180, School of Computer Science , Carnegie Mellon University , Pittsburgh, PA.]] Petersen, L., Cheng, P., Harper, R., and Stone, C. 2000. Implementing the TILT internal language. Tech. Rep. CMU-CS-00-180, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA.]]"},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the Logical Foundations of Computer Science '94","volume":"813","author":"Severi P.","unstructured":"Severi , P. and Poll , E . 1994. Pure Type Systems with definitions . In Proceedings of the Logical Foundations of Computer Science '94 . Lecture Notes in Computer Science , vol. 813 , Springer-Verlag, New York.]] Severi, P. and Poll, E. 1994. Pure Type Systems with definitions. In Proceedings of the Logical Foundations of Computer Science '94. Lecture Notes in Computer Science, vol. 813, Springer-Verlag, New York.]]"},{"volume-title":"The Dylan Reference Manual: The Definitive Guide to the New Object-Oriented Dynamic Language","author":"Shalit A.","unstructured":"Shalit , A. 1996. The Dylan Reference Manual: The Definitive Guide to the New Object-Oriented Dynamic Language . Addison-Wesley, Reading , MA .]] Shalit, A. 1996. The Dylan Reference Manual: The Definitive Guide to the New Object-Oriented Dynamic Language. Addison-Wesley, Reading, MA.]]","key":"e_1_2_1_32_1"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 1998 ACM International Conference on Functional Programming (ICFP '98)","author":"Shao Z.","year":"1998","unstructured":"Shao , Z. 1998 . Typed Cross-Module Compilation . In Proceedings of the 1998 ACM International Conference on Functional Programming (ICFP '98) . ACM, New York, 141--152.]] 10.1145\/289423.289436 Shao, Z. 1998. Typed Cross-Module Compilation. In Proceedings of the 1998 ACM International Conference on Functional Programming (ICFP '98). ACM, New York, 141--152.]] 10.1145\/289423.289436"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the Advanced Topics in Types and Programming Languages, B. C. Pierce, Ed. MIT Press","author":"Stone C. A.","year":"2005","unstructured":"Stone , C. A. 2005 . Type definitions . In Proceedings of the Advanced Topics in Types and Programming Languages, B. C. Pierce, Ed. MIT Press , Cambridge, MA.]] Stone, C. A. 2005. Type definitions. In Proceedings of the Advanced Topics in Types and Programming Languages, B. C. Pierce, Ed. MIT Press, Cambridge, MA.]]"},{"volume-title":"Proceedings of the 27th ACM Symposium on Principles of Programming Languages (POPL '00)","author":"Stone C. A.","unstructured":"Stone , C. A. and Harper , R . 2000. Decidable type equivalence with singleton kinds . In Proceedings of the 27th ACM Symposium on Principles of Programming Languages (POPL '00) . ACM, New York, 214--227.]] 10.1145\/325694.325724 Stone, C. A. and Harper, R. 2000. Decidable type equivalence with singleton kinds. In Proceedings of the 27th ACM Symposium on Principles of Programming Languages (POPL '00). ACM, New York, 214--227.]] 10.1145\/325694.325724","key":"e_1_2_1_36_1"},{"key":"e_1_2_1_37_1","volume-title":"Tech. Rep. HMC-CS-04-100, Computer Science Department","author":"Stone C. A.","year":"2004","unstructured":"Stone , C. A. and Harper , R . 2004 . Extensional equivalence and singleton types. Tech. Rep. HMC-CS-04-100, Computer Science Department , Harvey Mudd College .]] Stone, C. A. and Harper, R. 2004. Extensional equivalence and singleton types. Tech. Rep. HMC-CS-04-100, Computer Science Department, Harvey Mudd College.]]"},{"volume-title":"Proceedings of the ACM 1996 Conference on Programming Language Design and Implementation (PLDI '96)","author":"Tarditi D.","unstructured":"Tarditi , D. , Morrisett , G. , Cheng , P. , Stone , C. , Harper , R. , and Lee , P . 1996. TIL: A Type-Directed Optimizing Compiler for ML . In Proceedings of the ACM 1996 Conference on Programming Language Design and Implementation (PLDI '96) . ACM, New York, 181--192.]] 10.1145\/231379.231414 Tarditi, D., Morrisett, G., Cheng, P., Stone, C., Harper, R., and Lee, P. 1996. TIL: A Type-Directed Optimizing Compiler for ML. In Proceedings of the ACM 1996 Conference on Programming Language Design and Implementation (PLDI '96). ACM, New York, 181--192.]] 10.1145\/231379.231414","key":"e_1_2_1_38_1"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1183278.1183281","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1183278.1183281","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:06:37Z","timestamp":1750259197000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1183278.1183281"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10]]},"references-count":30,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,10]]}},"alternative-id":["10.1145\/1183278.1183281"],"URL":"https:\/\/doi.org\/10.1145\/1183278.1183281","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2006,10]]},"assertion":[{"value":"2006-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}