{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,18]],"date-time":"2026-01-18T01:35:26Z","timestamp":1768700126266,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642033582","type":"print"},{"value":"9783642033599","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_10","type":"book-chapter","created":{"date-parts":[[2009,8,20]],"date-time":"2009-08-20T01:46:12Z","timestamp":1250732772000},"page":"115-130","source":"Crossref","is-referenced-by-count":35,"title":["Some Domain Theory and Denotational Semantics in Coq"],"prefix":"10.1007","author":[{"given":"Nick","family":"Benton","sequence":"first","affiliation":[]},{"given":"Andrew","family":"Kennedy","sequence":"additional","affiliation":[]},{"given":"Carsten","family":"Varming","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11617990_1","volume-title":"Types for Proofs and Programs","author":"R. Adams","year":"2006","unstructured":"Adams, R.: Formalized metatheory with terms represented by an indexed family of types. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol.\u00a03839, pp. 1\u201316. Springer, Heidelberg (2006)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57826-9_143","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"S. Agerholm","year":"1994","unstructured":"Agerholm, S.: Domain theory in HOL. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol.\u00a0780. Springer, Heidelberg (1994)"},{"key":"10_CR3","unstructured":"Agerholm, S.: Formalizing a model of the lambda calculus in HOL-ST. Technical Report 354, University of Cambridge Computer Laboratory (1994)"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Agerholm, S.: LCF examples in HOL. The Computer Journal\u00a038(2) (1995)","DOI":"10.1093\/comjnl\/38.2.121"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/3-540-48168-0_32","volume-title":"Computer Science Logic","author":"T. Altenkirch","year":"1999","unstructured":"Altenkirch, T., Reus, B.: Monadic presentations of lambda terms using generalized inductive types. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 453\u2013468. Springer, Heidelberg (1999)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/11783596_6","volume-title":"Mathematics of Program Construction","author":"P. Audebaud","year":"2006","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol.\u00a04014, pp. 49\u201368. Springer, Heidelberg (2006)"},{"key":"10_CR7","unstructured":"Bartels, F., Dold, A., Pfeifer, H., Von Henke, F.W., Rue\u00df, H.: Formalizing fixed-point theory in PVS. Technical report, Universit\u00e4t Ulm (1996)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Benton, N., Hur, C.-K.: Biorthogonality, step-indexing and compiler correctness. In: ACM International Conference on Functional Programming (2009)","DOI":"10.1145\/1596550.1596567"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Capretta, V.: General recursion via coinductive types. Logical Methods in Computer Science\u00a01 (2005)","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"10_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58085-9_72","volume-title":"Types for Proofs and Programs","author":"T. Coquand","year":"1994","unstructured":"Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993, vol.\u00a0806. Springer, Heidelberg (1994)"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Freyd, P.: Recursive types reduced to inductive types. In: IEEE Symposium on Logic in Computer Science (1990)","DOI":"10.1109\/LICS.1990.113772"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Freyd, P.: Remarks on algebraically compact categories. In: Applications of Categories in Computer Science. LMS Lecture Notes, vol.\u00a0177 (1992)","DOI":"10.1017\/CBO9780511525902.006"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Joyal, A., Street, R.: The geometry of tensor calculus. Adv. in Math.\u00a088 (1991)","DOI":"10.1016\/0001-8708(91)90003-P"},{"key":"10_CR14","unstructured":"Kahn, G.: Elements of domain theory. In: The Coq users\u2019 contributions library (1993)"},{"key":"10_CR15","unstructured":"McBride, C.: Type-preserving renaming and substitution (unpublished draft)"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Milner, R.: Logic for computable functions: Description of a machine implementation. Technical Report STAN-CS-72-288, Stanford University (1972)","DOI":"10.21236\/AD0785072"},{"issue":"1","key":"10_CR17","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput.\u00a093(1), 55\u201392 (1991)","journal-title":"Inf. Comput."},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"M\u00fcller, O., Nipkow, T., von Oheimb, D., Slotosch, O.: HOLCF = HOL + LCF. J. Functional Programming\u00a09 (1999)","DOI":"10.1017\/S095679689900341X"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing\u00a010 (1998)","DOI":"10.1007\/s001650050009"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Paulin-Mohring, C.: A constructive denotational semantics for Kahn networks in Coq. In: From Semantics to Computer Science. Essays in Honour of G Kahn (2009)","DOI":"10.1017\/CBO9780511770524.018"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57826-9_122","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"K.D. Petersen","year":"1994","unstructured":"Petersen, K.D.: Graph model of LAMBDA in higher order logic. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol.\u00a0780. Springer, Heidelberg (1994)"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58027-1_3","volume-title":"Mathematical Foundations of Programming Semantics","author":"A.M. Pitts","year":"1994","unstructured":"Pitts, A.M.: Computational adequacy via \u2018mixed\u2019 inductive definitions. In: Main, M.G., Melton, A.C., Mislove, M.W., Schmidt, D., Brookes, S.D. (eds.) MFPS 1993. LNCS, vol.\u00a0802. Springer, Heidelberg (1994)"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Pitts, A.M.: Relational properties of domains. Inf. Comput.\u00a0127 (1996)","DOI":"10.1006\/inco.1996.0052"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60275-5_72","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"F. Regensburger","year":"1995","unstructured":"Regensburger, F.: HOLCF: Higher order logic of computable functions. In: Schubert, E.T., Alves-Foss, J., Windley, P. (eds.) HUG 1995. LNCS, vol.\u00a0971. Springer, Heidelberg (1995)"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Reus, B.: Formalizing a variant of synthetic domain theory. J. Automated Reasoning\u00a023 (1999)","DOI":"10.1023\/A:1006258506401"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Varming, C., Birkedal, L.: Higher-order separation logic in Isabelle\/HOLCF. In: Mathematical Foundations of Programming Semantics (2008)","DOI":"10.1016\/j.entcs.2008.10.022"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03359-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T02:48:31Z","timestamp":1558493311000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}