{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T22:40:05Z","timestamp":1740004805253,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642122507"},{"type":"electronic","value":"9783642122514"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-12251-4_7","type":"book-chapter","created":{"date-parts":[[2010,4,9]],"date-time":"2010-04-09T23:32:42Z","timestamp":1270855962000},"page":"72-86","source":"Crossref","is-referenced-by-count":1,"title":["A Functional Framework for Result Checking"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pablo","family":"Buiras","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C\u00e9sar","family":"Kunz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-92188-2_1","volume-title":"Formal Methods for Components and Objects","author":"G. Barthe","year":"2008","unstructured":"Barthe, G., Cr\u00e9gut, P., Gr\u00e9goire, B., Jensen, T.P., Pichardie, D.: The mobius proof carrying code infrastructure. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol.\u00a05382, pp. 1\u201324. Springer, Heidelberg (2008)"},{"issue":"1","key":"7_CR2","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1145\/200836.200880","volume":"42","author":"M. Blum","year":"1995","unstructured":"Blum, M., Kannan, S.: Designing programs that check their work. J. ACM\u00a042(1), 269\u2013291 (1995)","journal-title":"J. ACM"},{"key":"7_CR3","unstructured":"Bright, J.D.: Checking and Certifying Computational Results. PhD thesis (1994)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/BFb0054287","volume-title":"Mathematics of Program Construction","author":"T. Brunn","year":"1998","unstructured":"Brunn, T., Moller, B., Russling, M.: Layered graph traversals and hamiltonian path problems-an algebraic approach. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol.\u00a01422, pp. 96\u2013121. Springer, Heidelberg (1998)"},{"issue":"1\/2","key":"7_CR5","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1006\/jsco.2001.0457","volume":"32","author":"O. Caprotti","year":"2001","unstructured":"Caprotti, O., Oostdijk, M.: Formal and efficient primality proofs by use of computer algebra oracles. J. Symb. Comput.\u00a032(1\/2), 55\u201370 (2001)","journal-title":"J. Symb. Comput."},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1145\/258948.258955","volume-title":"Proceedings of the second ACM SIGPLAN international conference on Functional programming","author":"M. Erwig","year":"1997","unstructured":"Erwig, M.: Functional programming with graphs. In: Proceedings of the second ACM SIGPLAN international conference on Functional programming, pp. 52\u201365. ACM, New York (1997)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/11737414_8","volume-title":"Functional and Logic Programming","author":"B. Gr\u00e9goire","year":"2006","unstructured":"Gr\u00e9goire, B., Th\u00e9ry, L., Werner, B.: A computational approach to pocklington certificates in type theory. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol.\u00a03945, pp. 97\u2013113. Springer, Heidelberg (2006)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-74591-4_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2007","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 102\u2013118. Springer, Heidelberg (2007)"},{"issue":"5","key":"7_CR9","first-page":"1","volume":"27","author":"P. Hudak","year":"1992","unstructured":"Hudak, P., Peyton Jones, S.L., Wadler, P., Boutel, B., Fairbairn, J., Fasel, J.H., Guzm\u00e1n, M.M., Hammond, K., Hughes, J., Johnsson, T., Kieburtz, R.B., Nikhil, R.S., Partain, W., Peterson, J.: Report on the Programming Language Haskell, A Non-strict, Purely Functional Language. SIGPLAN Notices\u00a027(5), R1\u2013R164 (1992)","journal-title":"SIGPLAN Notices"},{"key":"7_CR10","unstructured":"Hudak, P., Peterson, J., Fasel, J.: A gentle introduction to Haskell 98 (1999), http:\/\/www.haskell.org\/tutorial\/"},{"key":"7_CR11","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1145\/1159803.1159811","volume-title":"Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming","author":"S.P. Jones","year":"2006","unstructured":"Jones, S.P., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. In: Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, pp. 50\u201361. ACM, New York (2006)"},{"key":"7_CR12","first-page":"42","volume-title":"POPL","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Morrisett, J.G., Peyton Jones, S.L. (eds.) POPL, pp. 42\u201354. ACM, New York (2006)"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL, pp. 106\u2013119 (1997)","DOI":"10.1145\/263699.263712"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Sullivan, G.F., Masson, G.M.: Using certification trails to achieve software fault tolerance. In: 20th International Symposium on Fault-Tolerant Computing, FTCS-20. Digest of Papers, June 1990, pp. 423\u2013431 (1990)","DOI":"10.1109\/FTCS.1990.89397"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/3-540-59451-5_2","volume-title":"Advanced Functional Programming","author":"P. Wadler","year":"1995","unstructured":"Wadler, P.: Monads for functional programming. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol.\u00a0925, pp. 24\u201352. Springer, Heidelberg (1995)"},{"key":"7_CR16","unstructured":"Zipitr\u00eda, F.: Towards secure distributed computations. Master\u2019s thesis, Universidad de la Rep\u00fablica, Uruguay (2008)"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12251-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T22:23:03Z","timestamp":1740003783000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12251-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642122507","9783642122514"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12251-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}