{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:27:20Z","timestamp":1767929240054,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2008,7,15]],"date-time":"2008-07-15T00:00:00Z","timestamp":1216080000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2008,7,15]]},"DOI":"10.1145\/1389449.1389461","type":"proceedings-article","created":{"date-parts":[[2008,7,22]],"date-time":"2008-07-22T13:46:39Z","timestamp":1216734399000},"page":"89-96","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Fixed point semantics and partial recursion in Coq"],"prefix":"10.1145","author":[{"given":"Yves","family":"Bertot","sequence":"first","affiliation":[{"name":"INRIA Sophia Antipolis, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vladimir","family":"Komendantsky","sequence":"additional","affiliation":[{"name":"INRIA Sophia Antipolis, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,7,15]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.4153\/CJM-1961-007-5"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71120-0"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/763787.763792"},{"key":"e_1_3_2_1_4_1","volume-title":"Journ\u00e9es Francophones pour les Langages Applicatifs","author":"Balaa A.","year":"2002","unstructured":"A. Balaa and Y. Bertot . Fonctions r\u00e9cursives g\u00e9n\u00e9rales par it\u00e9ration en th\u00e9orie des types . In Journ\u00e9es Francophones pour les Langages Applicatifs , Jan. 2002 . A. Balaa and Y. Bertot. Fonctions r\u00e9cursives g\u00e9n\u00e9rales par it\u00e9ration en th\u00e9orie des types. In Journ\u00e9es Francophones pour les Langages Applicatifs, Jan. 2002."},{"key":"e_1_3_2_1_5_1","volume-title":"Theorem proving support in programming language semantics","author":"Bertot Y.","year":"2007","unstructured":"Y. Bertot . Theorem proving support in programming language semantics , 2007 . htp:\/hal.inra.fr\/inra-016309. Y. Bertot. Theorem proving support in programming language semantics, 2007. htp:\/hal.inra.fr\/inra-016309."},{"key":"e_1_3_2_1_6_1","series-title":"Texts in Theoretical Computer Science: an EATCS series","volume-title":"Coq'art: the calculus of inductive constructions","author":"Bertot Y.","year":"2004","unstructured":"Y. Bertot and P. Cast\u00e9ran . Interactive theorem proving and program development , Coq'art: the calculus of inductive constructions . Texts in Theoretical Computer Science: an EATCS series . Springer-Verlag , 2004 . Y. Bertot and P. Cast\u00e9ran. Interactive theorem proving and program development, Coq'art: the calculus of inductive constructions. Texts in Theoretical Computer Science: an EATCS series. Springer-Verlag, 2004."},{"key":"e_1_3_2_1_7_1","unstructured":"Y. Bertot and V. Komendantsky. Proofs on domain theory and partial Yves.Breecrutrosio\/nt a2r0s0k8i.htmlp:\/w-sop.inra.fr\/marel\/ .  Y. Bertot and V. Komendantsky. Proofs on domain theory and partial Yves.Breecrutrosio\/nt a2r0s0k8i.htmlp:\/w-sop.inra.fr\/marel\/ ."},{"key":"e_1_3_2_1_8_1","volume-title":"International Workshop TYPES 2002","author":"Bove A.","year":"2003","unstructured":"A. Bove . General recursion in type theory. In H. Geuvers and F. Wiedijk, editors, Types for Proofs and Programs , International Workshop TYPES 2002 , The Netherlands, number 2646 in Lecture Notes in Computer Science, pages 39- -58, March 2003 . A. Bove. General recursion in type theory. In H. Geuvers and F. Wiedijk, editors, Types for Proofs and Programs, International Workshop TYPES 2002, The Netherlands, number 2646 in Lecture Notes in Computer Science, pages 39--58, March 2003."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770203.1770210"},{"key":"e_1_3_2_1_10_1","volume-title":"Reasoning with inductively defined relations in the HOL theorem prover. Technical report","author":"Camilleri J.","year":"1992","unstructured":"J. Camilleri and T. Melham . Reasoning with inductively defined relations in the HOL theorem prover. Technical report , University of Cambridge , 1992 . J. Camilleri and T. Melham. Reasoning with inductively defined relations in the HOL theorem prover. Technical report, University of Cambridge, 1992."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1762639.1762645"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/319838.319847"},{"key":"e_1_3_2_1_13_1","volume-title":"The Coq Proof Assistant Reference Manual, version 8.1","author":"Coq","year":"2006","unstructured":"Coq development team. The Coq Proof Assistant Reference Manual, version 8.1 , 2006 . Coq development team. The Coq Proof Assistant Reference Manual, version 8.1, 2006."},{"key":"e_1_3_2_1_14_1","volume-title":"July","author":"Dubois C.","year":"1998","unstructured":"C. Dubois and V. V. Donzeau-Gouge . A step towards the mechanization of partial functions: domains as inductive predicates , July 1998 . www.cs.bham.uk\/~mmk\/cade98-partialty. C. Dubois and V. V. Donzeau-Gouge. A step towards the mechanization of partial functions: domains as inductive predicates, July 1998. www.cs.bham.uk\/~mmk\/cade98-partialty."},{"key":"e_1_3_2_1_15_1","volume-title":"Garantie formelle de correction pour l'extraction Coq","author":"Glondu S.","year":"2007","unstructured":"S. Glondu . Garantie formelle de correction pour l'extraction Coq , 2007 . htp:\/stephane.glondu.net\/raport.207.pdf. S. Glondu. Garantie formelle de correction pour l'extraction Coq, 2007. htp:\/stephane.glondu.net\/raport.207.pdf."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/646522.694547"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/29580.29600"},{"key":"e_1_3_2_1_18_1","volume-title":"Elements of constructive geometry group theory and domain theory","author":"Kahn G.","year":"1995","unstructured":"G. Kahn . Elements of constructive geometry group theory and domain theory , 1995 . available as a Coq user contribution at http:\/\/coq.inra.fr\/contribs-eng.html. G. Kahn. Elements of constructive geometry group theory and domain theory, 1995. available as a Coq user contribution at http:\/\/coq.inra.fr\/contribs-eng.html."},{"key":"e_1_3_2_1_19_1","series-title":"Lecture Notes in Computer Science","volume-title":"A new extraction for Coq","author":"Letouzey P.","year":"2002","unstructured":"P. Letouzey . A new extraction for Coq . In H. Geuvers and F.Wiedijk, editors, TYPES 2002 , volume 2646 of Lecture Notes in Computer Science . Springer-Verlag , 2003. P. Letouzey. A new extraction for Coq. In H. Geuvers and F.Wiedijk, editors, TYPES 2002, volume 2646 of Lecture Notes in Computer Science. Springer-Verlag, 2003."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292601"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679689900341X"},{"key":"e_1_3_2_1_22_1","volume-title":"Semantics with Applications: A Formal Introduction","author":"Nielson H. R.","year":"1992","unstructured":"H. R. Nielson and F. Nielson . Semantics with Applications: A Formal Introduction . Wiley , 1992 . H. R. Nielson and F. Nielson. Semantics with Applications: A Formal Introduction. Wiley, 1992."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050009"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01941137"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/645891.671440"},{"key":"e_1_3_2_1_26_1","volume-title":"A constructive denotational semantics for Kahn networks in Coq","author":"Paulin-Mohring C.","year":"2007","unstructured":"C. Paulin-Mohring . A constructive denotational semantics for Kahn networks in Coq , 2007 . paulin07kahn.pdf htp:\/w.lri.fr\/~paulin\/PUBLIS\/ . C. Paulin-Mohring. A constructive denotational semantics for Kahn networks in Coq, 2007. paulin07kahn.pdf htp:\/w.lri.fr\/~paulin\/PUBLIS\/ ."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(06)80007-6"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/34057"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/646522.694537"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/151145"}],"event":{"name":"PPDP08: Principles and Practice of Declarative Programming","location":"Valencia Spain","acronym":"PPDP08","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1389449.1389461","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1389449.1389461","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:57:38Z","timestamp":1750255058000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1389449.1389461"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,7,15]]},"references-count":30,"alternative-id":["10.1145\/1389449.1389461","10.1145\/1389449"],"URL":"https:\/\/doi.org\/10.1145\/1389449.1389461","relation":{},"subject":[],"published":{"date-parts":[[2008,7,15]]},"assertion":[{"value":"2008-07-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}