{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:50:06Z","timestamp":1725511806762},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540680840"},{"type":"electronic","value":"9783540681038"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-68103-8_1","type":"book-chapter","created":{"date-parts":[[2008,5,6]],"date-time":"2008-05-06T00:10:07Z","timestamp":1210032607000},"page":"1-17","source":"Crossref","is-referenced-by-count":2,"title":["Algorithmic Equality in Heyting Arithmetic Modulo"],"prefix":"10.1007","author":[{"given":"Lisa","family":"Allali","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"Allali, L.: Memoire de DEA, http:\/\/www.lix.polytechnique.fr\/Labo\/Lisa.Allali\/rapport_MPRI.pdf"},{"key":"1_CR2","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1023\/A:1027357912519","volume":"31","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning\u00a031, 32\u201372 (2003)","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"1_CR3","doi-asserted-by":"publisher","first-page":"1289","DOI":"10.2178\/jsl\/1067620188","volume":"68","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Werner, B.: Proof normalization modulo. The Journal of Symbolic Logic\u00a068(4), 1289\u20131316 (2003)","journal-title":"The Journal of Symbolic Logic"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/978-3-540-32033-3_31","volume-title":"Term Rewriting and Applications","author":"G. Dowek","year":"2005","unstructured":"Dowek, G., Werner, B.: Arithmetic as a theory modulo. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 423\u2013437. Springer, Heidelberg (2005)"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74464-1_8","volume-title":"Types for Proofs and Programs","author":"G. Dowek","year":"2007","unstructured":"Dowek, G.: Truth values algebras and normalization. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, Springer, Heidelberg (2007)"},{"key":"1_CR6","series-title":"Proof theory: a selection of papers from the Leeds Proof Theory Programme 1990","volume-title":"Proofs as programs","author":"H. Schwichtenberg","year":"1992","unstructured":"Schwichtenberg, H.: Proofs as programs. Proof theory: a selection of papers from the Leeds Proof Theory Programme 1990. Cambridge University Press, Cambridge (1992)"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"van Oostrom, V., van Raamsdonk, F.: Weak Orthogonality Implies Confluence: The High-Order Case. Technical Report: ISRL-94-5 (December 1994)","DOI":"10.1007\/3-540-58140-5_35"},{"key":"1_CR8","unstructured":"Poincar\u00e8, H.: La Science et l\u2019hypoth\u00e8se, 1902, Flammarion (1968)"},{"key":"1_CR9","unstructured":"Dowek, G.: La part du calcul. M\u00e8moire d\u2019Habilitation \u00e0 Diriger des Recherches, Universit\u00e8 Paris\u00a07 (1999)"},{"key":"1_CR10","unstructured":"The Coq Development Team. Manuel de R\u00e8f\u00e8rence de Coq V8.0. LogiCal Project (2004-2006), http:\/\/coq.inria.fr\/doc\/main.html"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68103-8_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T00:32:48Z","timestamp":1620001968000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68103-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540680840","9783540681038"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68103-8_1","relation":{},"subject":[]}}