{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T03:07:50Z","timestamp":1725505670992},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540787389"},{"type":"electronic","value":"9783540787396"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78739-6_12","type":"book-chapter","created":{"date-parts":[[2008,4,2]],"date-time":"2008-04-02T08:39:06Z","timestamp":1207125546000},"page":"146-147","source":"Crossref","is-referenced-by-count":1,"title":["Constructive Mathematics and Functional Programming (Abstract)"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"Agda home page, http:\/\/appserv.cs.chalmers.se\/users\/ulfn\/wiki\/agda.php"},{"key":"12_CR2","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1016\/S0049-237X(08)70740-7","volume-title":"1970 Intuitionism and Proof Theory (Proc. Conf., Buffalo, N.Y., 1968)","author":"E. Bishop","year":"1970","unstructured":"Bishop, E.: Mathematics as a numerical language. In: 1970 Intuitionism and Proof Theory (Proc. Conf., Buffalo, N.Y., 1968), pp. 53\u201371. North-Holland, Amsterdam (1970)"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Berger, U.: Continuous Semantics for Strong Normalization. CiE, 23-34 (2005)","DOI":"10.1007\/11494645_4"},{"issue":"1","key":"12_CR4","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1017\/S0960129506005809","volume":"17","author":"Y. Bertot","year":"2007","unstructured":"Bertot, Y.: Affine functions and series with co-inductive real numbers. Mathematical Structures in Computer Science\u00a017(1), 37\u201363 (2007)","journal-title":"Mathematical Structures in Computer Science"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Coquand, T., Spiwack, A.: A proof of strong normalisation using domain theory. LMCS\u00a03(4:12) (2007)","DOI":"10.2168\/LMCS-3(4:12)2007"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Dufourd, J.-F.: A hypermap framework for computer-aided proofs in surface subdivisions: genus theorem and Euler\u2019s formula. In: SAC 2007, pp. 757\u2013761 (2007)","DOI":"10.1145\/1244002.1244171"},{"issue":"11","key":"12_CR7","doi-asserted-by":"publisher","first-page":"2974","DOI":"10.1016\/j.patcog.2007.02.013","volume":"40","author":"J.-F. Dufourd","year":"2007","unstructured":"Dufourd, J.-F.: Design and formal proof of a new optimal image segmentation program with hypermaps. Pattern Recognition\u00a040(11), 2974\u20132993 (2007)","journal-title":"Pattern Recognition"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-74591-4_8","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Gonthier","year":"2007","unstructured":"Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Th\u00e9ry, L.: A Modular Formalisation of Finite Group Theory. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 86\u2013101. Springer, Heidelberg (2007)"},{"key":"12_CR9","unstructured":"Gonthier, G.: A computer-checked proof of the Four Colour Theorem. (unpublished)"},{"issue":"9","key":"12_CR10","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1145\/583852.581501","volume":"37","author":"Benjamin Gr\u00e9goire","year":"2002","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: ICFP 2002, pp. 235\u2013246 (2002)","journal-title":"ACM SIGPLAN Notices"},{"issue":"4","key":"12_CR11","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1093\/comjnl\/6.4.308","volume":"6","author":"P. J. Landin","year":"1964","unstructured":"Landin, P.J.: The mechanical evaluation of expressions. Computer Journal\u00a06(4) (1964)","journal-title":"The Computer Journal"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: Constructive mathematics and computer programming. In: Logic, methodology and philosophy of science, VI (Hannover, 1979), Stud. Logic Found. Math., 104, pp. 153\u2013175. North-Holland, Amsterdam (1982)","DOI":"10.1016\/S0049-237X(09)70189-2"},{"issue":"1","key":"12_CR13","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1017\/S0960129506005871","volume":"17","author":"R. O\u2019Connor","year":"2007","unstructured":"O\u2019Connor, R.: A monadic, functional implementation of real numbers. Mathematical Structures in Computer Science\u00a017(1), 129\u2013159 (2007)","journal-title":"Mathematical Structures in Computer Science"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78739-6_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:20:45Z","timestamp":1619522445000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78739-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540787389","9783540787396"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78739-6_12","relation":{},"subject":[]}}