{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T20:15:22Z","timestamp":1743106522096,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540205371"},{"type":"electronic","value":"9783540400202"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-40020-2_7","type":"book-chapter","created":{"date-parts":[[2010,6,23]],"date-time":"2010-06-23T18:42:34Z","timestamp":1277318554000},"page":"129-144","source":"Crossref","is-referenced-by-count":0,"title":["Type Checking Parametrised Programs and Specifications in ASL\u2009+\u2009FPC"],"prefix":"10.1007","author":[{"given":"David","family":"Aspinall","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022243","volume-title":"Computer Science Logic","author":"D. Aspinall","year":"1995","unstructured":"Aspinall, D.: Subtyping with singleton types. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol.\u00a0933, Springer, Heidelberg (1995)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014424","volume-title":"Recent Trends in Data Type Specification","author":"D. Aspinall","year":"1995","unstructured":"Aspinall, D.: Types, subtypes, and ASL+. In: Reggio, G., Astesiano, E., Tarlecki, A. (eds.) Abstract Data Types 1994 and COMPASS 1994. LNCS, vol.\u00a0906. Springer, Heidelberg (1995)"},{"key":"7_CR3","unstructured":"Aspinall, D.: Type Systems for Modular Programs and Specification. PhD thesis, Department of Computer Science, University of Edinburgh (1997)"},{"key":"7_CR4","unstructured":"Cengarle, M.V.: Formal Specifications with Higher-Order Parameterisation. PhD thesis, Institut f\u00fcr Informatik, Ludwig-Maximilians- Universit\u00e4t M\u00fcnchen (1994)"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Dreyer, D., Crary, K., Harper, R.: A type system for higherorder modules. In: Proceedings of POPL 2003, New Orleans (2003)","DOI":"10.1145\/604131.604151"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"J.A. Goguen","year":"1992","unstructured":"Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. Journal of the ACM\u00a039, 95\u2013146 (1992)","journal-title":"Journal of the ACM"},{"key":"7_CR7","volume-title":"Introduction to HOL","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL. Cambridge University Press, Cambridge (1993)"},{"key":"7_CR8","volume-title":"Semantics of Programming Languages","author":"C.A. Gunter","year":"1992","unstructured":"Gunter, C.A.: Semantics of Programming Languages. MIT Press, Cambridge (1992)"},{"key":"7_CR9","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/174675.176927","volume-title":"Conference Record of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1994)","author":"R. Harper","year":"1994","unstructured":"Harper, R., Lillibridge, M.: A type-theoretic approach to higherorder modules with sharing. In: Conference Record of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1994), Portland, Oregon, January 17\u201321, pp. 123\u2013137. ACM Press, New York (1994)"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Harper, R., Mitchell, J.C., Moggi, E.: Higher-order modules and the phase distinction. In: Conference record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, CA, January 1990, pp. 341\u2013354 (1990)","DOI":"10.1145\/96709.96744"},{"key":"7_CR11","first-page":"21","volume-title":"Conference Record of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1996)","author":"M.P. Jones","year":"1996","unstructured":"Jones, M.P.: Using parameterized signatures to express modular structure. In: Conference Record of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1996), St. Petersburg, Florida, pp. 21\u201324. ACM Press, New York (1996)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1007\/BFb0030630","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"J. Courant","year":"1997","unstructured":"Courant, J.: An applicative module calculus. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol.\u00a01214, pp. 622\u2013636. Springer, Heidelberg (1997)"},{"key":"7_CR13","first-page":"109","volume-title":"Proc. 21st symp. Principles of Programming Languages","author":"X. Leroy","year":"1994","unstructured":"Leroy, X.: Manifest types, modules, and separate compilation. In: Proc. 21st symp. Principles of Programming Languages, pp. 109\u2013122. ACM press, New York (1994)"},{"key":"7_CR14","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1145\/199448.199476","volume-title":"Conference Record of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1995)","author":"X. Leroy","year":"1995","unstructured":"Leroy, X.: Applicative functors and fully transparent higher-order modules. In: Conference Record of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1995), San Francisco, California, January 22\u201325, pp. 142\u2013153. ACM Press, New York (1995)"},{"issue":"5","key":"7_CR15","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1017\/S0956796800001933","volume":"6","author":"X. Leroy","year":"1996","unstructured":"Leroy, X.: A syntactic theory of type generativity and sharing. Journal of Functional Programming\u00a06(5), 667\u2013698 (1996)","journal-title":"Journal of Functional Programming"},{"key":"7_CR16","series-title":"ACM SIGACT-SIGPLAN","first-page":"277","volume-title":"Proceedings, Thirteenth Annual ACM Symposium on Principles of Programming Languages","author":"D. MacQueen","year":"1986","unstructured":"MacQueen, D.: Using dependent types to express modular structure. In: Proceedings, Thirteenth Annual ACM Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, January 13\u201315. ACM SIGACT-SIGPLAN, pp. 277\u2013286. ACM Press, New York (1986)"},{"key":"7_CR17","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1017\/S095679689900341X","volume":"9","author":"O. M\u00fcller","year":"1999","unstructured":"M\u00fcller, O., Nipkow, T., von Oheimb, D., Slotosch, O.: HOLCF = HOL + LCF. Journal of Functional Programming\u00a09, 191\u2013223 (1999)","journal-title":"Journal of Functional Programming"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-44616-3_15","volume-title":"Recent Trends in Algebraic Development Techniques","author":"T. Mossakowski","year":"2000","unstructured":"Mossakowski, T.: Specifications in an arbitrary institution with symbols. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol.\u00a01827, pp. 252\u2013270. Springer, Heidelberg (2000)"},{"key":"7_CR19","unstructured":"Plotkin, G.: Denotational semantics with partial functions. Lecture at C.S.L.I. Summer School (1985)"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/10704567_5","volume-title":"Principles and Practice of Declarative Programming","author":"C.V. Russo","year":"1999","unstructured":"Russo, C.V.: Non-dependent types for standard ML modules. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol.\u00a01702, pp. 80\u201397. Springer, Heidelberg (1999)"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Stone, C.A., Harper, R.: Deciding type equivalence in a language with singleton kinds. In: ACM Symposium on Principles of Programming Languages (POPL), Boston, Massachusetts, pp. 214\u2013227, January 19\u201321 (2000)","DOI":"10.1145\/325694.325724"},{"key":"7_CR22","unstructured":"Shao, Z.: Parameterized signatures and higher-order modules, 1998. Technical Report YALEU\/DCS\/TR-1161, Dept. of Computer Science, Yale University (August 1998)"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Shao, Z.: Transparent modules with fully syntactic signatures. In: International Conference on Functional Programming, pp. 220\u2013232 (1999)","DOI":"10.21236\/ADA436465"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/3-540-45719-4_8","volume-title":"Algebraic Methodology and Software Technology","author":"L. Schr\u00f6der","year":"2002","unstructured":"Schr\u00f6der, L., Mossakowski, T.: HasCASL: Towards integrated specification and development of Haskell programs. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, p. 99. Springer, Heidelberg (2002)"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-45314-8_19","volume-title":"Fundamental Approaches to Software Engineering","author":"L. Schr\u00f6der","year":"2001","unstructured":"Schr\u00f6der, L., Mossakowski, T., Tarlecki, A., Klin, B., Hoffman, P.: Semantics of Architectural Specifications in CASL. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol.\u00a02029, pp. 253\u2013268. Springer, Heidelberg (2001)"},{"key":"7_CR26","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1007\/BF01191893","volume":"29","author":"D. Sannella","year":"1992","unstructured":"Sannella, D., Soko\u0142owski, S., Tarlecki, A.: Toward formal development of programs from algebraic specifications: Parameterisation revisited. Acta Informatica\u00a029, 689\u2013736 (1992)","journal-title":"Acta Informatica"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/3-540-17162-2_133","volume-title":"Category Theory and Computer Programming","author":"D. Sannella","year":"1986","unstructured":"Sannella, D., Tarlecki, A.: Extended ML: An institutionindependent framework for formal program development. In: Poign\u00e9, A., Pitt, D.H., Rydeheard, D.E., Abramsky, S. (eds.) Category Theory and Computer Programming. LNCS, vol.\u00a0240, pp. 364\u2013389. Springer, Heidelberg (1986)"},{"key":"7_CR28","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BF00283329","volume":"25","author":"D. Sannella","year":"1988","unstructured":"Sannella, D., Tarlecki, A.: Toward formal development of programs from algebraic specifications: implementation revisited. Acta Informatica\u00a025, 233\u2013281 (1988)","journal-title":"Acta Informatica"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","first-page":"452","volume-title":"ESOP \u201992","author":"A. Tarlecki","year":"1992","unstructured":"Tarlecki, A.: Modules for a model-oriented specification language: a proposal for MetaSoft. In: Krieg-Br\u00fcckner, B. (ed.) ESOP 1992. LNCS, vol.\u00a0582, pp. 452\u2013472. Springer, Heidelberg (1992)"}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Algebraic Development Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-40020-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T06:54:23Z","timestamp":1559199263000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-40020-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540205371","9783540400202"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-40020-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}