{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T14:40:10Z","timestamp":1746283210635,"version":"3.40.4"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319089690"},{"type":"electronic","value":"9783319089706"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08970-6_16","type":"book-chapter","created":{"date-parts":[[2014,6,28]],"date-time":"2014-06-28T11:13:26Z","timestamp":1403954006000},"page":"242-257","source":"Crossref","is-referenced-by-count":1,"title":["Hypermap Specification and Certified Linked Implementation Using Orbits"],"prefix":"10.1007","author":[{"given":"Jean-Fran\u00e7ois","family":"Dufourd","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/3-540-56610-4_57","volume-title":"TAPSOFT \u201993: Theory and Practice of Software Development","author":"Y. Bertrand","year":"1993","unstructured":"Bertrand, Y., Dufourd, J.-F., Fran\u00e7on, J., Lienhardt, P.: Algebraic Specification and Development in Geometric Modeling. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993, FASE 1993, and TAPSOFT 1993. LNCS, vol.\u00a0668, pp. 75\u201389. Springer, Heidelberg (1993)"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/10722010_8","volume-title":"Mathematics of Program Construction","author":"R. Bornat","year":"2000","unstructured":"Bornat, R.: Proving Pointer Programs in Hoare Logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol.\u00a01837, pp. 102\u2013126. Springer, Heidelberg (2000)"},{"key":"16_CR4","first-page":"23","volume":"7","author":"R.M. Burstall","year":"1972","unstructured":"Burstall, R.M.: Some Techniques for Proving Correctness of Programs which Alter Data Structures. Machine Intelligence\u00a07, 23\u201350 (1972)","journal-title":"Machine Intelligence"},{"key":"16_CR5","unstructured":"CEA-LIST and INRIA-Saclay-Proval Team. Frama-C Project (2013), http:\/\/frama-c.com\/about.html"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Mostly-Automated Verification of Low-level Programs in Computational Separation Logic. In: Int. ACM Conf. PLDI 2011, pp. 234\u2013245 (2011)","DOI":"10.1145\/1993316.1993526"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-14295-6_28","volume-title":"Computer Aided Verification","author":"C.L. Conway","year":"2010","unstructured":"Conway, C.L., Barrett, C.: Verifying Low-Level Implementations of High-Level Datatypes. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 306\u2013320. Springer, Heidelberg (2010)"},{"key":"16_CR8","unstructured":"Cori, R.: Un code pour les graphes planaires et ses applications. Soc. Math. de France, Ast\u00e9risque\u00a027 (1970)"},{"issue":"2-3","key":"16_CR9","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/j.tcs.2008.02.012","volume":"403","author":"J.-F. Dufourd","year":"2008","unstructured":"Dufourd, J.-F.: Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof. Theor. Comp. Science\u00a0403(2-3), 133\u2013159 (2008)","journal-title":"Theor. Comp. Science"},{"issue":"1","key":"16_CR10","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/s10817-009-9117-x","volume":"43","author":"J.-F. Dufourd","year":"2009","unstructured":"Dufourd, J.-F.: An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps. J. of Automated Reasoning\u00a043(1), 19\u201351 (2009)","journal-title":"J. of Automated Reasoning"},{"key":"16_CR11","unstructured":"Dufourd, J.-F.: Hmap Specification and Implementation - On-line Coq Development (2013), http:\/\/dpt-info.u-strasbg.fr\/~jfd\/Hmap.tar.gz"},{"key":"16_CR12","unstructured":"Dufourd, J.-F.: Formal Study of Functional Orbits in Finite Domains. Submitted to TCS, 40 pages (2013)"},{"key":"16_CR13","unstructured":"Dufourd, J.-F.: D\u00e9rivation de l\u2019Algorithme de Schorr-Waite par une M\u00e9thode Alg\u00e9brique. In: JFLA 2012, INRIA, hal-00665909, Carnac, 15 p. (February 2012)"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-642-14052-5_16","volume-title":"Interactive Theorem Proving","author":"J.-F. Dufourd","year":"2010","unstructured":"Dufourd, J.-F., Bertot, Y.: Formal Study of Plane Delaunay Triangulation. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 211\u2013226. Springer, Heidelberg (2010)"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Chlipala, A., et al.: Effective Interactive Proofs for Higher-Order Imperative programs. In: ICFP 2009, pp. 79\u201390 (2009)","DOI":"10.1145\/1631687.1596565"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-37036-6_9","volume-title":"Programming Languages and Systems","author":"C. Enea","year":"2013","unstructured":"Enea, C., Saveluc, V., Sighireanu, M.: Compositional Invariant Checking for Overlaid and Nested Linked Lists. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol.\u00a07792, pp. 129\u2013148. Springer, Heidelberg (2013)"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-540-73368-3_22","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2007","unstructured":"Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W., Wies, T., Yang, H.: Shape Analysis for Composite Data Structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 178\u2013192. Springer, Heidelberg (2007)"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/11901433_22","volume-title":"Formal Methods and Software Engineering","author":"N. Marti","year":"2006","unstructured":"Marti, N., Affeldt, R.: Formal Verification of the Heap Manager of an Operating System Using Separation Logic. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 400\u2013419. Springer, Heidelberg (2006)"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-27705-4_8","volume-title":"Verified Software: Theories, Tools, Experiments","author":"J.-C. Filli\u00e2tre","year":"2012","unstructured":"Filli\u00e2tre, J.-C.: Verifying Two Lines of C with Why3: An exercise in program verification. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 83\u201397. Springer, Heidelberg (2012)"},{"issue":"11","key":"16_CR20","first-page":"1382","volume":"55","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal Proof - the Four Color Theorem. Notices of the AMS\u00a055(11), 1382\u20131393 (2008)","journal-title":"Notices of the AMS"},{"issue":"1","key":"16_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"X. Leroy","year":"2008","unstructured":"Leroy, X., Blazy, S.: Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. J. of Autom. Reas.\u00a041(1), 1\u201331 (2008)","journal-title":"J. of Autom. Reas."},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-642-14808-8_17","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2010","author":"G. Malecha","year":"2010","unstructured":"Malecha, G., Morrisett, G.: Mechanized Verification with sharing. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol.\u00a06255, pp. 245\u2013259. Springer, Heidelberg (2010)"},{"key":"16_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-540-73147-4_12","volume-title":"Rewriting, Computation and Proof","author":"C. March\u00e9","year":"2007","unstructured":"March\u00e9, C.: Towards Modular Algebraic Specifications for Pointer Programs: A Case Study. In: Comon-Lundh, H., Kirchner, C., Kirchner, H. (eds.) Jouannaud Festschrift. LNCS, vol.\u00a04600, pp. 235\u2013258. Springer, Heidelberg (2007)"},{"issue":"1-2","key":"16_CR24","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1016\/j.ic.2004.10.007","volume":"199","author":"F. Mehta","year":"2005","unstructured":"Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Information and Computation\u00a0199(1-2), 200\u2013227 (2005)","journal-title":"Information and Computation"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. ACM TOPLAS\u00a031(3) (2009)","DOI":"10.1145\/1498926.1498929"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS 2002, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"16_CR27","unstructured":"CGAL Team. Computational Geometry Algorithms Library Project, Chapter 27: Combinatorial Maps (2013), http:\/\/www.cgal.org"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Wirsing, M.: Algebraic Specification. In: Handbook of TCS, vol. B. Elsevier\/MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50018-4"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08970-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T14:01:41Z","timestamp":1746280901000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08970-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319089690","9783319089706"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08970-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}