{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:13:38Z","timestamp":1763468018310,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642177958"},{"type":"electronic","value":"9783642177965"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-17796-5_10","type":"book-chapter","created":{"date-parts":[[2011,1,11]],"date-time":"2011-01-11T12:08:27Z","timestamp":1294747707000},"page":"163-179","source":"Crossref","is-referenced-by-count":6,"title":["Program Calculation in Coq"],"prefix":"10.1007","author":[{"given":"Julien","family":"Tesson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hideki","family":"Hashimoto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenjiang","family":"Hu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fr\u00e9d\u00e9ric","family":"Loulergue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Masato","family":"Takeichi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Bird, R.: Constructive functional programming. In: STOP Summer School on Constructive Algorithmics, Abeland (September 1989)","DOI":"10.1007\/978-3-642-74884-4_5"},{"key":"10_CR2","volume-title":"Programming: the derivation of algorithms","author":"A. Kaldewaij","year":"1990","unstructured":"Kaldewaij, A.: Programming: the derivation of algorithms. Prentice-Hall, Inc., Upper Saddle River (1990)"},{"key":"10_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61455-2_12","volume-title":"Algebra of Programming","author":"R. Bird","year":"1996","unstructured":"Bird, R., de Moor, O.: Algebra of Programming. Prentice-Hall, Englewood Cliffs (1996)"},{"key":"10_CR4","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-642-87374-4_1","volume-title":"Logic of Programming and Calculi of Discrete Design","author":"R. Bird","year":"1987","unstructured":"Bird, R.: An introduction to the theory of lists. In: Broy, M. (ed.) Logic of Programming and Calculi of Discrete Design, pp. 5\u201342. Springer, Heidelberg (1987)"},{"key":"#cr-split#-10_CR5.1","unstructured":"Gibbons, J.: Algebras for Tree Algorithms. D. phil thesis (1991);"},{"key":"#cr-split#-10_CR5.2","unstructured":"Also available as Technical Monograph PRG-94"},{"key":"10_CR6","unstructured":"de Moor, O.: Categories, relations and dynamic programming. Ph.D thesis, Programming research group, Oxford Univ. (1992) Technical Monograph PRG-98"},{"key":"10_CR7","first-page":"316","volume-title":"POPL 1998: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Z. Hu","year":"1998","unstructured":"Hu, Z., Takeichi, M., Chin, W.N.: Parallelization in calculational forms. In: POPL 1998: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 316\u2013328. ACM Press, New York (1998)"},{"key":"10_CR8","unstructured":"Smith, D.R.: KIDS \u2014 a knowledge-based software development system. In: Lowry, M.R., Mccartney, R.D. (eds.) Automating Software Design, Menlo Park, CA, pp. 483\u2013514. AAAI Press \/ The MIT Press (1991)"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Advanced Functional Programming","author":"O. Moor de","year":"1999","unstructured":"de Moor, O., Sittampalam, G.: Generic program transformation. In: Swierstra, S.D., Oliveira, J.N. (eds.) AFP 1998. LNCS, vol.\u00a01608. Springer, Heidelberg (1999)"},{"key":"10_CR10","unstructured":"Yokoyama, T., Hu, Z., Takeichi, M.: Yicho: A system for programming program calculations. Technical Report METR 2002\u201307, Department of Mathematical Engineering, University of Tokyo (June 2002)"},{"key":"10_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development \u2013 Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development \u2013 Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-Class Type Classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 278\u2013293. Springer, Heidelberg (2008)"},{"issue":"1","key":"10_CR13","doi-asserted-by":"publisher","first-page":"831","DOI":"10.1016\/j.jsc.2004.12.011","volume":"40","author":"E. Visser","year":"2005","unstructured":"Visser, E.: A survey of strategies in rule-based program transformation systems. J. Symb. Comput.\u00a040(1), 831\u2013873 (2005)","journal-title":"J. Symb. Comput."},{"issue":"5","key":"10_CR14","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1017\/S0956796809007345","volume":"19","author":"S.c. Mu","year":"2009","unstructured":"Mu, S.c., Ko, H.s., Jansson, P.: Algebra of programming in agda: Dependent types for relational program derivation. J. Funct. Program\u00a019(5), 545\u2013579 (2009)","journal-title":"J. Funct. Program"},{"key":"10_CR15","first-page":"239","volume-title":"In International Conference on Functional Programming","author":"L. Augustsson","year":"1998","unstructured":"Augustsson, L.: Cayenne - a language with dependent types. In: In International Conference on Functional Programming, pp. 239\u2013250. ACM Press, New York (1998)"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/11546382_3","volume-title":"Advanced Functional Programming","author":"C. McBride","year":"2005","unstructured":"McBride, C.: Epigram: Practical programming with dependent types. In: Vene, V., Uustalu, T. (eds.) AFP 2004. LNCS, vol.\u00a03622, pp. 130\u2013170. Springer, Heidelberg (2005)"},{"key":"10_CR17","first-page":"1","volume-title":"TLDI","author":"U. Norell","year":"2009","unstructured":"Norell, U.: Dependently typed programming in agda. In: Kennedy, A., Ahmed, A. (eds.) TLDI, pp. 1\u20132. ACM, New York (2009)"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-540-68103-8_5","volume-title":"Types for Proofs and Programs","author":"P. Corbineau","year":"2008","unstructured":"Corbineau, P.: A Declarative Language for the Coq Proof Assistant. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol.\u00a04941, pp. 69\u201384. Springer, Heidelberg (2008)"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-61756-6_73","volume-title":"Programming Languages: Implementations, Logics, and Programs","author":"L. Meertens","year":"1996","unstructured":"Meertens, L.: Calculate Polytypically! In: Kuchen, H., Swierstra, S.D. (eds.) PLILP 1996. LNCS, vol.\u00a01140, pp. 1\u201316. Springer, Heidelberg (1996)"},{"key":"10_CR20","first-page":"49","volume-title":"WGP 2008: Proceedings of the ACM SIGPLAN Workshop on Generic Programming","author":"W. Verbruggen","year":"2008","unstructured":"Verbruggen, W., de Vries, E., Hughes, A.: Polytypic programming in Coq. In: WGP 2008: Proceedings of the ACM SIGPLAN Workshop on Generic Programming, pp. 49\u201360. ACM Press, New York (2008)"},{"key":"10_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1596614.1596616","volume-title":"WGP 2009: Proceedings of the 2009 ACM SIGPLAN Workshop on Generic Programming","author":"W. Verbruggen","year":"2009","unstructured":"Verbruggen, W., de Vries, E., Hughes, A.: Polytypic properties and proofs in Coq. In: WGP 2009: Proceedings of the 2009 ACM SIGPLAN Workshop on Generic Programming, pp. 1\u201312. ACM Press, New York (2009)"},{"key":"10_CR22","unstructured":"The Coq Development Team: The Coq Proof Assistant, http:\/\/coq.inria.fr"},{"key":"10_CR23","unstructured":"Bertot, Y.: Coq in a hurry (2006), http:\/\/hal.inria.fr\/inria-00001173"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17796-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T15:16:39Z","timestamp":1559920599000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17796-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642177958","9783642177965"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17796-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}