{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:40:35Z","timestamp":1725496835957},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665366"},{"type":"electronic","value":"9783540481683"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48168-0_37","type":"book-chapter","created":{"date-parts":[[2007,12,1]],"date-time":"2007-12-01T11:30:26Z","timestamp":1196508626000},"page":"530-545","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Specification Refinement with System F"],"prefix":"10.1007","author":[{"given":"Jo Erskine","family":"Hannay","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,5,13]]},"reference":[{"key":"37_CR1","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1016\/0304-3975(93)90082-5","volume":"121","author":"M. Abadi","year":"1993","unstructured":"M. Abadi, L. Cardelli, and P.-L. Curien. Formal parametric polymorphism. Theoretical Computer Science, 121:9\u201358, 1993.","journal-title":"Theoretical Computer Science"},{"unstructured":"D. Aspinall. Type Systems for Modular Programs and Specifications. PhD thesis, University of Edinburgh, 1998.","key":"37_CR2"},{"key":"37_CR3","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/0304-3975(90)90151-7","volume":"70","author":"E.S. Bainbridge","year":"1990","unstructured":"E.S. Bainbridge, P.J. Freyd, A. Scedrov, and P.J. Scott. Functorial polymorphism. Theoretical Computer Science, 70:35\u201364, 1990.","journal-title":"Theoretical Computer Science"},{"key":"37_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(96)00039-4","volume":"165","author":"M. Bidoit","year":"1996","unstructured":"M. Bidoit and R. Hennicker. Behavioural theories and the proof of behavioural properties. Theoretical Computer Science, 165:3\u201355, 1996.","journal-title":"Theoretical Computer Science"},{"key":"37_CR5","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/0167-6423(95)00014-3","volume":"25","author":"M. Bidoit","year":"1995","unstructured":"M. Bidoit, R. Hennicker, and M. Wirsing. Behavioural and abstractor specifications. Science of Computer Programming, 25:149\u2013186, 1995.","journal-title":"Science of Computer Programming"},{"key":"37_CR6","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1016\/S0304-3975(96)00162-4","volume":"173","author":"M. Bidoit","year":"1997","unstructured":"M. Bidoit, R. Hennicker, and M. Wirsing. Proof systems for structured specifications with observability operators. Theoretical Computer Sci., 173:393\u2013443, 1997.","journal-title":"Theoretical Computer Sci"},{"key":"37_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Algebraic System Specification and Development: A Survey and Annotated Bibliography","year":"1991","unstructured":"M. Bidoit, H.-J. Kreowski, P. Lescanne, F. Orejas, and D. Sannella (eds.). Algebraic System Specification and Development: A Survey and Annotated Bibliography, volume 501 of LNCS. Springer, 1991."},{"key":"37_CR8","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0304-3975(85)90135-5","volume":"39","author":"C. B\u00f6hm","year":"1985","unstructured":"C. B\u00f6hm and A. Beraducci. Automatic synthesis of typed ?-programs on term algebras. Theoretical Computer Science, 39:135\u2013154, 1985.","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"J.A. Goguen. Parameterized programming. IEEE Transactions on Software Engineering, SE-10(5):528\u2013543, 1984.","key":"37_CR9","DOI":"10.1109\/TSE.1984.5010277"},{"key":"37_CR10","volume-title":"Habilitationsschrift","author":"R. Hennicker","year":"1997","unstructured":"R. Hennicker. Structured specifications with behavioural operators: Semantics, proof methods and applications. Habilitationsschrift, LMU, M\u00fcnchen, 1997."},{"key":"37_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/BFb0014055","volume-title":"Proc. TLCA\u201995","author":"M. Hofmann","year":"1995","unstructured":"M. Hofmann. A simple model for quotient types. In Proc. TLCA\u201995, volume 902 of LNCS, pages 216\u2013234. Springer, 1995."},{"key":"37_CR12","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(96)00068-0","volume":"167","author":"M. Hofmann","year":"1996","unstructured":"M. Hofmann and D. Sannella. On behavioural abstraction and behavioural satisfaction in higher-order logic. Theoretical Computer Science, 167:3\u201345, 1996.","journal-title":"Theoretical Computer Science"},{"key":"37_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-48775-1","volume-title":"Proc. CSL\u201999","author":"F. Honsell","year":"1999","unstructured":"F. Honsell and D. Sannella. Pre-logical relations. In Proc. CSL\u201999, LNCS, 1999."},{"key":"37_CR14","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1016\/S0304-3975(96)00163-6","volume":"173","author":"S. Kahrs","year":"1997","unstructured":"S. Kahrs, D. Sannella, and A. Tarlecki. The definition of Extended ML: a gentle introduction. Theoretical Computer Science, 173:445\u2013484, 1997.","journal-title":"Theoretical Computer Science"},{"key":"37_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BFb0014552","volume-title":"Proceedings of TACS\u201997","author":"Y. Kinoshita","year":"1997","unstructured":"Y. Kinoshita, P.W. O\u2019Hearn, A.J. Power, M. Takeyama, and R.D. Tennent. An axiomatic approach to binary logical relations with applications to data refinement. In Proceedings of TACS\u201997, volume 1281 of LNCS, pages 191\u2013212. Springer, 1997."},{"key":"37_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/BFb0054239","volume-title":"Proc. AMAST\u201998","author":"H. Kirchner","year":"1998","unstructured":"H. Kirchner and P.D. Mosses. Algebraic specifications, higher-order types, and set-theoretic models. In Proc. AMAST\u201998, volume 1548 of LNCS, pages 378\u2013388. Springer, 1998."},{"key":"37_CR17","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1017\/S0960129500000256","volume":"3","author":"Z. Luo","year":"1993","unstructured":"Z. Luo. Program specification and data type refinement in type theory. Math. Struct. in Comp. Sci., 3:333\u2013363, 1993.","journal-title":"Math. Struct. in Comp. Sci."},{"key":"37_CR18","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Proc. 7th MFPS","author":"Q. Ma","year":"1991","unstructured":"Q. Ma and J.C. Reynolds. Types, abstraction and parametric polymorphism, part 2. In Proc. 7th MFPS, volume 598 of LNCS, pages 1\u201340. Springer, 1991."},{"key":"37_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/3540543961_15","volume-title":"ACM Symposium on Functional Programming and Computer Architecture","author":"H. Mairson","year":"1991","unstructured":"H. Mairson. Outline of a proof theory of parametricity. In ACM Symposium on Functional Programming and Computer Architecture, volume 523 of LNCS, pages 313\u2013327. Springer, 1991."},{"key":"37_CR20","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1016\/0304-3975(92)90310-C","volume":"100","author":"K. Meinke","year":"1992","unstructured":"K. Meinke. Universal algebra in higher types. Theoretical Computer Science, 100:385\u2013417, 1992.","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"J.C. Mitchell. On the equivalence of data representations. In V. Lifschitz, editor, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pages 305\u2013330. Academic Press, 1991.","key":"37_CR21","DOI":"10.1016\/B978-0-12-450010-5.50023-2"},{"unstructured":"J.C. Mitchell. Foundations for Programming Languages. Foundations of Computing Series. MIT Press, 1996.","key":"37_CR22"},{"key":"37_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/3-540-61629-2_55","volume-title":"Recent Trends in Data Type Spec., 11th WADT","author":"N. Mylonakis","year":"1995","unstructured":"N. Mylonakis. Behavioural specifications in type theory. In Recent Trends in Data Type Spec., 11th WADT, volume 1130 of LNCS, pages 394\u2013408. Springer, 1995."},{"key":"37_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/BFb0037118","volume-title":"Proc. of TLCA 93","author":"G. Plotkin","year":"1993","unstructured":"G. Plotkin and M. Abadi. A logic for parametric polymorphism. In Proc. of TLCA 93, volume 664 of LNCS, pages 361\u2013375. Springer, 1993."},{"key":"37_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"310","DOI":"10.1007\/3-540-48959-2_22","volume-title":"Proc. TLCA\u201999","author":"E. Poll","year":"1999","unstructured":"E. Poll and J. Zwanenburg. A logic for abstract data types as existential types. In Proc. TLCA\u201999, volume 1581 of LNCS, pages 310\u2013324, 1999."},{"key":"37_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"660","DOI":"10.1007\/3-540-57182-5_57","volume-title":"Proc. MFCS\u201993","author":"B. Reus","year":"1993","unstructured":"B. Reus and T. Streicher. Verifying properties of module construction in type theory. In Proc. MFCS\u201993, volume 711 of LNCS, pages 660\u2013670, 1993."},{"key":"37_CR27","first-page":"513","volume":"83","author":"J.C. Reynolds","year":"1983","unstructured":"J.C. Reynolds. Types, abstraction and parametric polymorphism. Information Processing, 83:513\u2013523, 1983.","journal-title":"Information Processing"},{"key":"37_CR28","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1007\/BF01191893","volume":"29","author":"D. Sannella","year":"1992","unstructured":"D. Sannella, S. Soko\u0142owski, and A. Tarlecki. Toward formal development of programs from algebraic specifications: parameterisation revisited. Acta Inform., 29:689\u2013736, 1992.","journal-title":"Acta Inform"},{"key":"37_CR29","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1016\/0022-0000(87)90023-7","volume":"34","author":"D. Sannella","year":"1987","unstructured":"D. Sannella and A. Tarlecki. On observational equivalence and algebraic specification. Journal of Computer and System Sciences, 34:150\u2013178, 1987.","journal-title":"Journal of Computer and System Sciences"},{"issue":"3","key":"37_CR30","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BF00283329","volume":"25","author":"D. Sannella","year":"1988","unstructured":"D. Sannella and A. Tarlecki. Toward formal development of programs from algebraic specifications: Implementations revisited. Acta Inform., 25(3):233\u2013281, 1988.","journal-title":"Acta Inform"},{"key":"37_CR31","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/BF01211084","volume":"9","author":"D. Sannella","year":"1997","unstructured":"D. Sannella and A. Tarlecki. Essential concepts of algebraic specification and program development. Formal Aspects of Computing, 9:229\u2013269, 1997.","journal-title":"Formal Aspects of Computing"},{"key":"37_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1007\/3-540-12689-9_122","volume-title":"Proc. 1983 Intl. Conf. on Foundations of Computation Theory","author":"D. Sannella","year":"1983","unstructured":"D. Sannella and M. Wirsing. A kernel language for algebraic specification and implementation. In Proc. 1983 Intl. Conf. on Foundations of Computation Theory, volume 158 of LNCS, pages 413\u2013427. Springer, 1983."},{"unstructured":"O. Schoett. Data Abstraction and the Correctness of Modular Programming. PhD thesis, University of Edinburgh, 1986.","key":"37_CR33"},{"key":"37_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/3-540-54496-8_17","volume-title":"Recent Trends in Data Type Spec","author":"T. Streicher","year":"1990","unstructured":"T. Streicher and M. Wirsing. Dependent types considered necessary for specification languages. In Recent Trends in Data Type Spec., volume 534 of LNCS, pages 323\u2013339. Springer, 1990."},{"key":"37_CR35","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/BFb0014443","volume-title":"Recent Trends in Data Type Spec., Proc. 10th WADT","author":"J. Underwood","year":"1994","unstructured":"J. Underwood. Typing abstract data types. In Recent Trends in Data Type Spec., Proc. 10th WADT, volume 906 of LNCS, pages 437\u2013452. Springer, 1994."},{"doi-asserted-by":"crossref","unstructured":"M. Wirsing. Structured specifications: Syntax, semantics and proof calculus. In Logic and Algebra of Specification, pages 411\u2013442. Springer, 1993.","key":"37_CR36","DOI":"10.1007\/978-3-642-58041-3_11"},{"key":"37_CR37","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/BFb0014423","volume-title":"Recent Trends in Data Type Specification","author":"M. Wirsing","year":"1994","unstructured":"M. Wirsing. Algebraic specification languages: An overview. In Recent Trends in Data Type Specification, volume 906 of LNCS, pages 81\u2013115. Springer, 1994."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48168-0_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T04:09:57Z","timestamp":1586146197000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48168-0_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665366","9783540481683"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/3-540-48168-0_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"13 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}