{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:32:32Z","timestamp":1774837952916,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642393198","type":"print"},{"value":"9783642393204","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"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":[[2013]]},"DOI":"10.1007\/978-3-642-39320-4_29","type":"book-chapter","created":{"date-parts":[[2013,7,1]],"date-time":"2013-07-01T07:22:52Z","timestamp":1372663372000},"page":"359-363","source":"Crossref","is-referenced-by-count":11,"title":["Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Barras","sequence":"first","affiliation":[]},{"given":"Lourdes","family":"del Carmen Gonz\u00e1lez Huesca","sequence":"additional","affiliation":[]},{"given":"Hugo","family":"Herbelin","sequence":"additional","affiliation":[]},{"given":"Yann","family":"R\u00e9gis-Gianas","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[]},{"given":"Makarius","family":"Wenzel","sequence":"additional","affiliation":[]},{"given":"Burkhart","family":"Wolff","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"Acar, U.A., Blelloch, G.E., Harper, R.: Adaptive functional programming. ACM Trans. Program. Lang. Syst. 28(6) (November 2006)","DOI":"10.1145\/1186632.1186634"},{"key":"29_CR2","doi-asserted-by":"crossref","unstructured":"Claret, G., Gonzalez Huesca, L.D.C., Regis-Gianas, Y., Ziliani, B.: Lightweight proof by reflection by a posteriori simulation of effectful computations. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving (ITP 2013). LNCS. Springer (2013)","DOI":"10.1007\/978-3-642-39634-2_8"},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"Doligez, D., Leroy, X.: A concurrent, generational garbage collector for a multithreaded implementation of ML. In: 20th ACM Symposium on Principles of Programming Languages (POPL). ACM Press (1993)","DOI":"10.1145\/158511.158611"},{"key":"29_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M.J. Gordon","year":"1979","unstructured":"Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"Matthews, D., Wenzel, M.: Efficient parallel programming in Poly\/ML and Isabelle\/ML. In: ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming (DAMP 2010) (2010)","DOI":"10.1145\/1708046.1708058"},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"Sutter, H.: The free lunch is over \u2014 a fundamental turn toward concurrency in software. Dr. Dobb\u2019s Journal 30(3) (2005)","DOI":"10.1145\/1095408.1095421"},{"key":"29_CR7","unstructured":"Tassi, E., Barras, B.: Designing a state transaction machine for Coq. In: The Coq Workshop 2012 (co-located with ITP 2012) (2012)"},{"key":"29_CR8","unstructured":"Wenzel, M.: Parallel proof checking in Isabelle\/Isar. In: Dos Reis, G., Th\u00e9ry, L. (eds.) ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009). ACM Digital Library (2009)"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1007\/978-3-642-31374-5_38","volume-title":"Intelligent Computer Mathematics","author":"M. Wenzel","year":"2012","unstructured":"Wenzel, M.: Isabelle\/jEdit \u2013 A prover IDE within the PIDE framework. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol.\u00a07362, pp. 468\u2013471. Springer, Heidelberg (2012)"},{"key":"29_CR10","unstructured":"Wenzel, M.: PIDE as front-end technology for Coq. ArXiv (April 2013), \n                    \n                      http:\/\/arxiv.org\/abs\/1304.6626"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: READ-EVAL-PRINT in parallel and asynchronous proof-checking. In: User Interfaces for Theorem Provers (UITP 2012). EPTCS (2013)","DOI":"10.4204\/EPTCS.118.4"},{"key":"29_CR12","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Shared-memory multiprocessing for interactive theorem proving. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving (ITP 2013). LNCS. Springer (2013)","DOI":"10.1007\/978-3-642-39634-2_30"},{"key":"29_CR13","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"The Seventeen Provers of the World","year":"2006","unstructured":"Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS (LNAI), vol.\u00a03600. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39320-4_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T21:48:39Z","timestamp":1558302519000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39320-4_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642393198","9783642393204"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39320-4_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}