{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:46:38Z","timestamp":1725540398207},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642050886"},{"type":"electronic","value":"9783642050893"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-05089-3_31","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T17:31:40Z","timestamp":1257269500000},"page":"483-498","source":"Crossref","is-referenced-by-count":6,"title":["Towards an Operational Semantics for Alloy"],"prefix":"10.1007","author":[{"given":"Theophilos","family":"Giannakopoulos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel J.","family":"Dougherty","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kathi","family":"Fisler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shriram","family":"Krishnamurthi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"31_CR1","volume-title":"Software Abstractions","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions. MIT Press, Cambridge (2006)"},{"key":"31_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J.R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"31_CR3","volume-title":"The Z Notation: A Reference Manual","author":"J.M. Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice Hall, Englewood Cliffs (1992)","edition":"2"},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"Krishnamurthi, S., Dougherty, D.J., Fisler, K., Yoo, D.: Alchemy: Transmuting base alloy specifications into implementations. In: ACM SIGSOFT International Symposium on the Foundations of Software Engineering (2008)","DOI":"10.1145\/1453101.1453123"},{"key":"31_CR5","doi-asserted-by":"crossref","unstructured":"Dougherty, D.J.: An improved algorithm for generating database transactions from relational algebra specifications. In: International Workshop on Rule-Based Programming (2009)","DOI":"10.4204\/EPTCS.21.7"},{"issue":"2","key":"31_CR6","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology\u00a011(2), 256\u2013290 (2002)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"31_CR7","doi-asserted-by":"crossref","unstructured":"Edwards, J., Jackson, D., Torlak, E.: A type system for object models. In: ACM SIGSOFT International Symposium on the Foundations of Software Engineering (2004)","DOI":"10.1145\/1029894.1029921"},{"issue":"4","key":"31_CR8","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/s10990-007-9008-y","volume":"20","author":"S. Krishnamurthi","year":"2007","unstructured":"Krishnamurthi, S., Hopkins, P.W., McCarthy, J.A., Graunke, P.T., Pettyjohn, G., Felleisen, M.: Implementation and use of the PLT Scheme web server. Higher-Order and Symbolic Computation\u00a020(4), 431\u2013460 (2007)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"31_CR9","doi-asserted-by":"crossref","unstructured":"Plotkin, G.D.: LCF considered as a programming language. Theoretical Computer Science, 223\u2013255 (1977)","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"Frias, M.F., L\u00f3pez Pombo, C.G., Galeotti, J.P., Aguirre, N.M.: Efficient analysis of DynAlloy specifications. ACM Transactions on Software Engineering and Methodology\u00a017(1) (December 2007)","DOI":"10.1145\/1314493.1314497"},{"key":"31_CR11","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/j.entcs.2007.08.033","volume":"195","author":"T. Massoni","year":"2008","unstructured":"Massoni, T., Gheyi, R., Borba, P.: A framework for establishing formal conformance between object models and object-oriented programs. Electronic Notes in Theoretical Computer Science\u00a0195, 189\u2013209 (2008)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"1","key":"31_CR12","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1145\/2363.2528","volume":"7","author":"J.L. Bates","year":"1985","unstructured":"Bates, J.L., Constable, R.L.: Proofs as programs. ACM Transactions on Programming Languages and Systems\u00a07(1), 113\u2013136 (1985)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"31_CR13","unstructured":"The Coq development team: The Coq proof assistant reference manual. LogiCal Project, Version 8.0 (2004)"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"Green, C.C.: Application of theorem proving to problem solving. In: International Joint Conference on Artificial Intelligence (1969)","DOI":"10.21236\/ADA459656"},{"key":"31_CR15","unstructured":"Waldinger, R.J., Lee, R.C.T.: PROW: A step toward automatic program writing. In: International Joint Conference on Artificial Intelligence (1969)"},{"issue":"8","key":"31_CR16","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/2.75","volume":"21","author":"C. Rich","year":"1988","unstructured":"Rich, C., Waters, R.C.: Automatic programming: Myths and prospects. IEEE Computer\u00a021(8), 40\u201351 (1988)","journal-title":"IEEE Computer"}],"container-title":["Lecture Notes in Computer Science","FM 2009: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-05089-3_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:47:36Z","timestamp":1606168056000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-05089-3_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642050886","9783642050893"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-05089-3_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}