{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:47:03Z","timestamp":1725475623312},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672814"},{"type":"electronic","value":"9783540464211"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10720084_10","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T14:36:30Z","timestamp":1167402990000},"page":"136-150","source":"Crossref","is-referenced-by-count":3,"title":["Integrating Computer Algebra and Reasoning through the Type System of Aldor"],"prefix":"10.1007","author":[{"given":"Erik","family":"Poll","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon","family":"Thompson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"Alexandre, G.: De Aldor \u00e1 Zermelo. PhD thesis, Universit\u00e9 Paris VI (1998)"},{"key":"10_CR2","volume-title":"Cayenne \u2013 a language with dependent types.","author":"L. Augustsson","year":"1998","unstructured":"Augustsson, L.: Cayenne \u2013 a language with dependent types. ACM Press, New York (1998)"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Bauer, A., Clarke, E., Zhao, X.: Analytica - an experiment in combining theorem proving and symbolic computation. In: Pfalzgraf, J., Calmet, J., Campbell, J. (eds.) AISMC 1996. LNCS, vol.\u00a01138. Springer, Heidelberg (1996)","DOI":"10.1007\/3-540-61732-9_48"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Buchberger, B.: Symbolic Computation: Computer Algebra and Logic. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems. Kluwer, Dordrecht (1996)","DOI":"10.1007\/978-94-009-0349-4_10"},{"key":"10_CR5","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1145\/258726.258853","volume-title":"Proceedings of ISSAC 1997 (International Symposium on Symbolic and Algebraic Computation)","author":"B. Buchberger","year":"1997","unstructured":"Buchberger, B., Jebelean, T., Kriftner, F., Marin, M., Tomuta, E., Vasaru, D.: A survey of the Theorema project. In: Proceedings of ISSAC 1997 (International Symposium on Symbolic and Algebraic Computation), pp. 384\u2013391. ACM, New York (1997)"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Calmet, J., Homann, K.: Classification of communication and cooperation mechanisms for logical and symbolic computation systems. In: FroCos 1996. Kluwer, Dordrecht (1996)","DOI":"10.1007\/978-94-009-0349-4_11"},{"key":"10_CR7","unstructured":"Constable, R.L., et al.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall Inc., Englewood Cliffs (1986)"},{"key":"10_CR8","unstructured":"Cornes, C., et al.: The Coq proof assistant reference manual, version 5.10. Rapport technique RT-0177, INRIA (1995)"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Dunstan, M., Kelsey, T.: Lightweight Formal Methods for Computer Algebra Systems. In: ISSAC 1998 (1998)","DOI":"10.1145\/281508.281560"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Fateman, R.: Why computer algebra systems can\u2019t solve simple equations. ACM SIGSAM Bulletin\u00a030 (1996)","DOI":"10.1145\/235699.235701"},{"key":"10_CR11","unstructured":"Girard, J.-Y.: Int\u00e9rpretation fonctionelle et \u00e9limination des coupures dans l\u2019arithm etique d\u2019ordre sup\u00e9rieure. Th\u00e8se d\u2019Etat, Universit\u00e9 Paris VII (1972)"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Henglein, F.: Type Inference with Polymorphic Recursion. ACM Transactions on Programming Languages and Systems\u00a015 (1993)","DOI":"10.1145\/169701.169692"},{"key":"10_CR13","volume-title":"Axiom: The Scientific Computation System","author":"R.D. Jenks","year":"1992","unstructured":"Jenks, R.D., Sutor, R.S.: Axiom: The Scientific Computation System. Springer, Heidelberg (1992)"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Martin, U.: Computers, reasoning and mathematical practice. In: Schwichtenberg, H. (ed.) Computational Logic, Marktoberdorf 1997. Springer, Heidelberg (1998)","DOI":"10.1007\/978-3-642-58622-4_9"},{"key":"#cr-split#-10_CR15.1","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory. Bibliopolis, Naples (1984);"},{"key":"#cr-split#-10_CR15.2","unstructured":"Based on a set of notes taken by Giovanni Sambin of a series of lectures given in Padova (June 1980)"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"McAllester, D., Arkondas, K.: Walther recursion. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104. Springer, Heidelberg (1996)","DOI":"10.1007\/3-540-61511-3_119"},{"key":"10_CR17","volume-title":"The Definition of Standard ML","author":"R. Milner","year":"1990","unstructured":"Milner, R., Tofte, M., Harper, R.: The Definition of Standard ML. MIT Press, Cambridge (1990)"},{"issue":"3","key":"10_CR18","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1145\/44501.45065","volume":"10","author":"J.C. Mitchell","year":"1988","unstructured":"Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Trans. on Prog. Lang. and Syst.\u00a010(3), 470\u2013502 (1988)","journal-title":"ACM Trans. on Prog. Lang. and Syst."},{"key":"10_CR19","volume-title":"Programming in Martin L\u00f6f \u2019s Type Theory \u2013An Introduction","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.M.: Programming in Martin L\u00f6f \u2019s Type Theory \u2013An Introduction. Oxford University Press, Oxford (1990)"},{"key":"10_CR20","unstructured":"Paulin-Mohring, C.: Inductive definitions in the system Coq. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664. Springer, Heidelberg (1993)"},{"key":"10_CR21","unstructured":"Peterson, J., Hammond, K. (eds.): Report on the Programming Language Haskell, Version 1.4 (1997), http:\/\/www.haskell.org\/report\/"},{"key":"10_CR22","unstructured":"Poll, E., Thompson, S.: The Type System of Aldor. Technical Report 11-99, Computing Laboratory, University of Kent at Canterbury (1999)"},{"key":"10_CR23","unstructured":"Ryder, C., Thompson, S.: Aldor meets Haskell. Technical Report 15-99, Computing Laboratory, University of Kent at Canterbury (1999)"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Santas, P.S.: A type system for computer algebra. Journal of Symbolic Computation\u00a019 (1995)","DOI":"10.1006\/jsco.1995.1006"},{"key":"10_CR25","first-page":"189","volume":"3","author":"J.R. Shackell","year":"1995","unstructured":"Shackell, J.R.: Symbolic asymptotics and the calculation of limits. Journal of Analysis\u00a03, 189\u2013204 (1995); Volume commemorating Maurice Blambert","journal-title":"Journal of Analysis"},{"key":"10_CR26","volume-title":"Type Theory and Functional Programming.","author":"S. Thompson","year":"1991","unstructured":"Thompson, S.: Type Theory and Functional Programming. Addison Wesley, Reading (1991)"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Turner, D.: Elementary strong functional programming. In: Hartel, P.H., Plasmeijer, R. (eds.) FPLE 1995. LNCS, vol.\u00a01022. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-60675-0_35"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Wadler, P., Blott, S.: Making ad hoc polymorphism less ad hoc. In: Proceedings of the 16th ACM Symposium on Principles of Programming Languages. ACM Press, New York (1989)","DOI":"10.1145\/75277.75283"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Watt, S.M., et al.: A First Report on the A# Compiler. In: ISSAC 1994. ACM Press, New York (1994)","DOI":"10.1145\/190347.190356"},{"key":"10_CR30","unstructured":"Watt, S.M., et al.: AXIOM: Library Compiler User Guide. NAG Ltd. (1995)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10720084_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,10]],"date-time":"2023-05-10T07:06:06Z","timestamp":1683702366000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10720084_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672814","9783540464211"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/10720084_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}