{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T23:06:46Z","timestamp":1781651206380,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540314288","type":"print"},{"value":"9783540314295","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11617990_7","type":"book-chapter","created":{"date-parts":[[2006,1,19]],"date-time":"2006-01-19T06:39:40Z","timestamp":1137652780000},"page":"98-114","source":"Crossref","is-referenced-by-count":6,"title":["A Semi-reflexive Tactic for (Sub-)Equational Reasoning"],"prefix":"10.1007","author":[{"given":"Claudio Sacerdoti","family":"Coen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"2","key":"7_CR1","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1017\/S0956796802004501","volume":"13","author":"G. Barthe","year":"2003","unstructured":"Barthe, G., Pons, O., Capretta, V.: Setoids in type theory. Journal of Functional Programming\u00a013(2), 261\u2013293 (2003)","journal-title":"Journal of Functional Programming"},{"issue":"5\/6","key":"7_CR2","first-page":"249","volume":"30","author":"D. Basin","year":"1994","unstructured":"Basin, D.: Generalized Rewriting in Type Theory. Journal of Information Processing and Cybernetics\u00a030(5\/6), 249\u2013259 (1994)","journal-title":"Journal of Information Processing and Cybernetics"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"554","DOI":"10.1007\/3-540-44802-0_39","volume-title":"Computer Science Logic","author":"P. Courtieu","year":"2001","unstructured":"Courtieu, P.: Normalized Types. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 554\u2013569. Springer, Heidelberg (2001)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/3-540-44659-1_25","volume-title":"Theorem Proving in Higher Order Logics","author":"C. L\u00fcth","year":"2000","unstructured":"L\u00fcth, C., Wolff, B.: TAS \u2014 A Generic Window Inference System. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 405\u2013422. Springer, Heidelberg (2000)"},{"key":"7_CR5","unstructured":"Gr\u00e9goire, B.: Compilation de termes de preuves: un (nouveau) mariage entre Coq et OCaml. PhD thesis. Universit\u00e9 Paris 7 (2004)"},{"issue":"4","key":"7_CR6","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1093\/comjnl\/39.4.291","volume":"39","author":"J. Grundy","year":"1996","unstructured":"Grundy, J.: Transformational hierarchical reasoning. The Computer Journal\u00a039(4), 291\u2013302 (1996)","journal-title":"The Computer Journal"},{"key":"7_CR7","unstructured":"Hofmann, M.: Extensional concepts in intensional type theory. PhD thesis. LFCS Edinburgh (1995)"},{"key":"7_CR8","unstructured":"Kreitz, C.: The NuPRL 5 Manual, pp. 135\u2013145"},{"key":"7_CR9","unstructured":"Renard, C.: Memoire de DEA: Un peu d\u2019extensionnalit\u00e9 en Coq. INRIA Rocquencourt (2001)"},{"key":"7_CR10","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1093\/logcom\/3.1.47","volume":"3","author":"P.J. Robinson","year":"1993","unstructured":"Robinson, P.J., Staples, J.: Formalizing a hierarchical structure of practical mathematical reasoning. Journal of Logic and Computation\u00a03, 47\u201361 (1993)","journal-title":"Journal of Logic and Computation"},{"key":"7_CR11","unstructured":"Staples, M.: Window Inference in Isabelle. In: Proceedings of the Isabelle Users Workshop, Cambridge, UK, September 18-19 (1995)"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11617990_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T03:12:02Z","timestamp":1619493122000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11617990_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540314288","9783540314295"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/11617990_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}