{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:11:41Z","timestamp":1725484301882},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540440390"},{"type":"electronic","value":"9783540456858"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_7","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T20:47:53Z","timestamp":1179607673000},"page":"83-97","source":"Crossref","is-referenced-by-count":7,"title":["Type-Theoretic Functional Semantics"],"prefix":"10.1007","author":[{"given":"Yves","family":"Bertot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Venanzio","family":"Capretta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kuntal Das","family":"Barman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"7_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44659-1_1","volume-title":"Theorem Proving in Higher Order Logics:13th International Conference, TPHOLs 2000","author":"A. Balaa","year":"2000","unstructured":"Antonia Balaa and Yves Bertot. Fix-point equations for well-founded recursion in type theory. In Harrison and Aagaard [8], pages 1\u201316."},{"key":"7_CR2","series-title":"Lect Notes Comput Sci","volume-title":"International Joint Conference of Theory and Practice of Software Development (TAPSOFT\/FASE\u201995)","author":"Y. Bertot","year":"1995","unstructured":"Yves Bertot and Ranan Fraer. Reasoning with executable specifications. In International Joint Conference of Theory and Practice of Software Development (TAPSOFT\/FASE\u201995), volume 915 of LNCS. Springer-Verlag, 1995."},{"issue":"1","key":"7_CR3","first-page":"22","volume":"8","author":"A. Bove","year":"2001","unstructured":"A. Bove. Simple general recursion in type theory. Nordic Journal of Computing, 8(1):22\u201342, Spring 2001.","journal-title":"Nordic Journal of Computing"},{"key":"7_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-44755-5_10","volume-title":"Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001","author":"A. Bove","year":"2001","unstructured":"Ana Bove and Venanzio Capretta. Nested general recursion and partiality in type theory. In Richard J. Boulton and Paul B. Jackson, editors, Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001, volume 2152 of Lecture Notes in Computer Science, pages 121\u2013135. Springer-Verlag, 2001."},{"key":"7_CR5","unstructured":"Catherine Dubois and V\u00e9ronique Vigui\u00e9 Donzeau-Gouge. A step towards the mechanization of partial functions: Domains as inductive predicates. Presented at CADE-15, Workshop on Mechanization of Partial Functions, 1998."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2), June 2000.","DOI":"10.2307\/2586554"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Simon Finn, Michael Fourman, and John Longley. Partial functions in a total setting. Journal of Automated Reasoning, 18(1):85\u2013104, February 1997.","DOI":"10.1023\/A:1005702928286"},{"key":"7_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000","year":"2000","unstructured":"J. Harrison and M. Aagaard, editors. Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science. Springer-Verlag, 2000."},{"key":"7_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1007\/3-540-62034-6_48","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"T. Nipkow","year":"1996","unstructured":"Tobias Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. In V. Chandru and V. Vinay, editors, Foundations of Software Technology and Theoretical Computer Science, volume 1180 of LNCS, pages 180\u2013192. Springer, 1996."},{"key":"7_CR10","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1016\/S0747-7171(06)80007-6","volume":"15","author":"C. Paulin-Mohring","year":"1993","unstructured":"Christine Paulin-Mohring and Benjamin Werner. Synthesis of ML programs in the system Coq. Journal of Symbolic Computation, 15:607\u2013640, 1993.","journal-title":"Journal of Symbolic Computation"},{"key":"7_CR11","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/BF00246023","volume":"2","author":"L. C. Paulson","year":"1986","unstructured":"Lawrence C. Paulson. Proving termination of normalization functions for conditional expressions. Journal of Automated Reasoning, 2:63\u201374, 1986.","journal-title":"Journal of Automated Reasoning"},{"key":"7_CR12","unstructured":"The Coq Development Team. LogiCal Project. The Coq Proof Assistant. Reference Manual. Version 7.2. INRIA, 2001."},{"key":"7_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1007\/3-540-44659-1_31","volume-title":"Theorem Proving in Higher Order Logics:13th International Conference, TPHOLs 2000","author":"K. Slind","year":"2000","unstructured":"K. Slind. Another look at nested recursion. In Harrison and Aagaard [8], pages 498\u2013518."},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Freek Wiedijk and Jan Zwanenburg. First order logic with domain conditions. Available at http:\/\/www.cs.kun.nl\/~freek\/notes\/partial.ps.gz , 2002.","DOI":"10.1007\/10930755_15"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Glynn Winskel. The Formal Semantics of Programming Languages, an introduction. Foundations of Computing. The MIT Press, 1993.","DOI":"10.7551\/mitpress\/3054.001.0001"}],"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\/3-540-45685-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,22]],"date-time":"2020-04-22T05:38:35Z","timestamp":1587533915000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}