{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:12:38Z","timestamp":1770275558150,"version":"3.49.0"},"publisher-location":"Boston","reference-count":13,"publisher":"Kluwer Academic Publishers","isbn-type":[{"value":"1402081405","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/1-4020-8141-3_34","type":"book-chapter","created":{"date-parts":[[2006,2,21]],"date-time":"2006-02-21T15:15:11Z","timestamp":1140534911000},"page":"437-450","source":"Crossref","is-referenced-by-count":59,"title":["Dynamic Typing with Dependent Types"],"prefix":"10.1007","author":[{"given":"Xinming","family":"Ou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gang","family":"Tan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yitzhak","family":"Mandelbaum","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Walker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"34_CR1","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1145\/103135.103138","volume":"13","author":"M. Abadi","year":"1991","unstructured":"Mart\u00edn Abadi, Luca Cardelli, Benjamin C. Pierce, and Gordon Plotkin. Dynamic typing in a statically typed language. ACM Transactions on Programming Languages and Systems, 13(2):237\u2013268, April 1991.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"34_CR2","doi-asserted-by":"crossref","unstructured":"Alex Aiken, Edward L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In Twenty-First ACM Symposium on Principles of Programming Languages, pages 163\u2013173, January 1994.","DOI":"10.1145\/174675.177847"},{"key":"34_CR3","doi-asserted-by":"crossref","unstructured":"R. Cartwright and M. Fagan. Soft typing. In ACM Conference on Programming Language Design and Implementation, pages 278\u2013292, 1991.","DOI":"10.1145\/113445.113469"},{"issue":"1","key":"34_CR4","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1145\/239912.239917","volume":"19","author":"R. Cartwright","year":"1997","unstructured":"R. Cartwright and M. Fagan. A practical soft type system for Scheme. ACM transactions on programming languages and systems, 19(1):87\u2013152, January 1997.","journal-title":"ACM transactions on programming languages and systems"},{"key":"34_CR5","doi-asserted-by":"crossref","unstructured":"Rob Deline and Manuel F\u00e4hndrich. Enforcinghigh-level protocols in low-level software. In ACM Conference on Programming Language Design and Implementation, pages 59\u201369, Snowbird, Utah, June 2001. ACM Press.","DOI":"10.1145\/381694.378811"},{"key":"34_CR6","doi-asserted-by":"crossref","unstructured":"Robert Bruce Findler and Matthias Felleisen. Contracts for higher-order functions. In ACM International Conference on Functional Programming, pages 48\u201359, Pittsburgh, October 2002. ACM Press.","DOI":"10.1145\/581478.581484"},{"key":"34_CR7","doi-asserted-by":"crossref","unstructured":"Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. In Twenty-First ACM Symposium on Principles of Programming Languages, pages 123\u2013137, Portland, OR, January 1994.","DOI":"10.1145\/174675.176927"},{"key":"34_CR8","doi-asserted-by":"crossref","unstructured":"George C. Necula, Scott McPeak, and Westley Weimer. Ccured: Type-safe retrofitting of legacy code. In ACM Symposium on Principles of Programming Languages, London, January 2002. ACM Press.","DOI":"10.1145\/503272.503286"},{"key":"34_CR9","unstructured":"Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. Dynamic typing with dependent types. Technical Report TR-695-04, Department of Computer Science, Princeton University, 2004."},{"key":"34_CR10","doi-asserted-by":"crossref","unstructured":"S. Thatte. Quasi-static typing. In Seventeenth ACM Symposium on Principles of Programming Languages, pages 367\u2013381, January 1990.","DOI":"10.1145\/96709.96747"},{"key":"34_CR11","doi-asserted-by":"crossref","unstructured":"David Walker. A type system for expressive security policies. In Twenty-Seventh ACM Symposium on Principles of Programming Languages, pages 254\u2013267, Boston, January 2000.","DOI":"10.1145\/325694.325728"},{"key":"34_CR12","doi-asserted-by":"crossref","unstructured":"Hongwei Xi and Frank Pfenning. Eliminating array bound checking through dependent types. In ACM Conference on Programming Language Design and Implementation, pages 249\u2013257, Montreal, June 1998.","DOI":"10.1145\/277650.277732"},{"key":"34_CR13","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0304-3975(97)00062-5","volume":"187","author":"C. Zenger","year":"1997","unstructured":"Christoph Zenger. Indexed types. In Theoretical Computer Science, volume 187, pages 147\u2013165. Elsevier, November 1997.","journal-title":"Theoretical Computer Science"}],"container-title":["IFIP International Federation for Information Processing","Exploring New Frontiers of Theoretical Informatics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/1-4020-8141-3_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T20:28:18Z","timestamp":1619555298000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/1-4020-8141-3_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["1402081405"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/1-4020-8141-3_34","relation":{},"subject":[]}}