{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T23:26:28Z","timestamp":1725578788340},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642198281"},{"type":"electronic","value":"9783642198298"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-19829-8_8","type":"book-chapter","created":{"date-parts":[[2011,3,16]],"date-time":"2011-03-16T10:20:41Z","timestamp":1300270841000},"page":"112-127","source":"Crossref","is-referenced-by-count":13,"title":["A Type-Theoretic Framework for Certified Model Transformations"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Calegari","sequence":"first","affiliation":[]},{"given":"Carlos","family":"Luna","sequence":"additional","affiliation":[]},{"given":"Nora","family":"Szasz","sequence":"additional","affiliation":[]},{"given":"\u00c1lvaro","family":"Tasistro","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/3-540-47884-1_16","volume-title":"Integrated Formal Methods","author":"S. Kent","year":"2002","unstructured":"Kent, S.: Model-Driven Engineering. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol.\u00a02335, pp. 286\u2013298. Springer, Heidelberg (2002)"},{"key":"8_CR2","unstructured":"OMG: Meta Object Facility (MOF) 2.0 Core Specification. Object Management Group, Specification Version 2.0 (2003)"},{"key":"8_CR3","unstructured":"ATLAS Group: Kernel MetaMetaModel. LINA & INRIA. Manual v0.3 (2005)"},{"key":"8_CR4","unstructured":"OMG: UML 2.0 Object Constraint Language. Object Management Group, Specification Version 2.0 (2006)"},{"key":"8_CR5","series-title":"ENTCS","first-page":"125","volume-title":"A Taxonomy of Model Transformation","author":"T. Mens","year":"2006","unstructured":"Mens, T., Czarnecki, K., van Gorp, P.: A Taxonomy of Model Transformation. ENTCS, vol.\u00a0152, pp. 125\u2013142. Springer, Heidelberg (2006)"},{"issue":"3","key":"8_CR6","doi-asserted-by":"publisher","first-page":"621","DOI":"10.1147\/sj.453.0621","volume":"45","author":"K. Czarnecki","year":"2006","unstructured":"Czarnecki, K., Helsen, S.: Feature-Based Survey of Model Transformation Approaches. IBM Systems Journal\u00a045(3), 621\u2013645 (2006)","journal-title":"IBM Systems Journal"},{"key":"8_CR7","unstructured":"OMG: Meta Object Facility (MOF) 2.0 Query\/View\/Transformation. Object Management Group, Specification Version 1.0 (2008)"},{"key":"8_CR8","unstructured":"ATLAS Group: Atlas Transformation Language. LINA & INRIA. User Guide (2009)"},{"key":"8_CR9","unstructured":"Anastasakis, K., Bordbar, B., K\u00fcster, J.M.: Analysis of Model Transformations via Alloy. In: Proc. 4\n                  th\n                 Workshop on Model-Driven Engineering, Verification and Validation, pp. 47\u201356 (2007)"},{"key":"8_CR10","series-title":"ENTCS","first-page":"43","volume-title":"A Lightweight Approach for the Semantic Validation of Model Refinements","author":"C. Pons","year":"2008","unstructured":"Pons, C., Garc\u00eda, D.: A Lightweight Approach for the Semantic Validation of Model Refinements. ENTCS, vol.\u00a0220, pp. 43\u201361. Springer, Heidelberg (2008)"},{"key":"8_CR11","unstructured":"Giese, H., et al.: Towards Verified Model Transformations. In: Proc. 3rd International Workshop on Model Development, Validation and Verification, pp. 78\u201393 (2006)"},{"key":"8_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions.","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"key":"8_CR13","unstructured":"The Coq Development Team: The Coq Proof Assistant: Reference Manual (2009)"},{"key":"8_CR14","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: Formal Verification of a Realistic Compiler. Commun. ACM\u00a052, 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/11786160_15","volume-title":"Architecting Systems with Trustworthy Components","author":"I. Poernomo","year":"2006","unstructured":"Poernomo, I.: A Type Theoretic Framework for Formal Metamodelling. In: Reussner, R., Stafford, J.A., Ren, X.-M. (eds.) Architecting Systems with Trustworthy Components. LNCS, vol.\u00a03938, pp. 262\u2013298. Springer, Heidelberg (2006)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-540-69927-9_15","volume-title":"Theory and Practice of Model Transformations","author":"I. Poernomo","year":"2008","unstructured":"Poernomo, I.: Proofs-as-Model Transformations. In: Vallecillo, A., Gray, J., Pierantonio, A. (eds.) ICMT 2008. LNCS, vol.\u00a05063, pp. 214\u2013228. Springer, Heidelberg (2008)"},{"key":"8_CR17","unstructured":"Calegari, D., Luna, C., Szasz, N., Tasistro, A.: Experiment with a Type-Theoretic Approach to the Verification of Model Transformations. In: Proc. 2nd Chilean Workshop on Formal Methods, pp. 29\u201336 (2009), \n                  \n                    http:\/\/jcc2009.usach.cl\/?page_id=631\n                  \n                  \n                 (last visit: August 2010)"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"COLOG-88","author":"T. Coquand","year":"1990","unstructured":"Coquand, T., Paulin, C.: Inductively Defined Types. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol.\u00a0417, pp. 50\u201366. Springer, Heidelberg (1990)"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/11663430_13","volume-title":"Satellite Events at the MoDELS 2005 Conference","author":"J. B\u00e9zivin","year":"2006","unstructured":"B\u00e9zivin, J., Rumpe, B., Sch\u00fcrr, A., Tratt, L.: Model Transformations in Practice Workshop. In: Bruel, J.-M. (ed.) MoDELS 2005. LNCS, vol.\u00a03844, pp. 120\u2013127. Springer, Heidelberg (2006)"},{"key":"8_CR20","unstructured":"Verification of UML-Based Behavioral Model Transformations Project, \n                  \n                    http:\/\/www.fing.edu.uy\/inco\/grupos\/coal\/field.php\/Proyectos\/ANII09\n                  \n                  \n                 (last visit: August 2010)"},{"key":"8_CR21","first-page":"401","volume":"6","author":"J. Steel","year":"2007","unstructured":"Steel, J., J\u00e9z\u00e9quel, J.M.: On Model Typing. SoSyM\u00a06, 401\u2013413 (2007)","journal-title":"SoSyM"},{"key":"8_CR22","unstructured":"Beckert, B., Keller, U., Schmitt, P.: Translating the Object Constraint Language into First-Order Predicate Logic. In: Workshop at Federated Logic Conferences (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19829-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T07:03:56Z","timestamp":1558422236000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19829-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642198281","9783642198298"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19829-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}