{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:11:27Z","timestamp":1725484287910},"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_20","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T16:47:53Z","timestamp":1179593273000},"page":"298-313","source":"Crossref","is-referenced-by-count":2,"title":["Algebraic Structures and Dependent Records"],"prefix":"10.1007","author":[{"given":"Virgile","family":"Prevosto","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Damien","family":"Doligez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Th\u00e9r\u00e8se","family":"Hardin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"20_CR1","unstructured":"G. Betarte. Dependent Record Types and Formal Abstract Reasoning: Theory and Practice. PhD thesis, University of G\u00f6teborg, 1998."},{"key":"20_CR2","unstructured":"S. Boulm\u00e9, T. Hardin, and R. Rioboo. Polymorphic data types, objects, modules and functors: is it too much? Research Report 14, LIP6, 2000. available at http:\/\/www.Iip6.fr\/reports\/lip6.2000.014.html ."},{"key":"20_CR3","unstructured":"S. Boulm\u00e9. Sp\u00e9cification d\u2019un environnement d\u00e9di\u00e9 \u00e1 la programmation certifi\u00e9e de biblioth\u00e9ques de Calcul Formel. PhD thesis, Universit\u00e9 Paris 6, december 2000."},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"B. Buchberger and all. A survey on the theorema project. In W. Kuechlin, editor, Proceedings of ISSAG\u201997. ACM Press, 1997.","DOI":"10.1145\/258726.258853"},{"key":"20_CR5","unstructured":"D. Delahaye. Conception de langages pour d\u00e9crire les preuves et les automatisations dans les outils d\u2019aide \u00e1 la preuve. PhD thesis, Universit\u00e9 Paris 6, 2001."},{"key":"20_CR6","unstructured":"G. Dowek, T. Hardin, and C. Kirchner. Theorem proving modulo. Research Report 3400, INRIA, 1998."},{"issue":"l","key":"20_CR7","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1017\/S0960129500003236","volume":"11","author":"G. Dowek","year":"2001","unstructured":"G. Dowek, T. Hardin, and C. Kirchner. Hol-\u03bb\u03c3: an intentional first-order expression of higher-order logic. Mathematical Structures in Computer Science, 11(l):21\u201345, 2001.","journal-title":"Mathematical Structures in Computer Science"},{"key":"20_CR8","volume-title":"Technical Report M-93B138","author":"W. M. Farmer","year":"1995","unstructured":"W. M. Farmer, J. D. Guttman, and F. J. Thayer. The imps user\u2019s manual. Technical Report M-93B138, The mitre Corporation, 202 Burlington Road, Bedford, MA 01730-1420, USA, November 1995. Available at ftp:\/\/math.harvard.edu\/imps\/doc\/ ."},{"key":"20_CR9","unstructured":"H. Geuvers, R. Pollack, F. Wiedijk, and J. Zwanenburg. The algebraic hierarchy of the fta project. In Proceedings of the Calculemus Workshop, 2001."},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In 21st Symposium on Principle of Programming Languages, 1994.","DOI":"10.1145\/174675.176927"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"P. Jackson. Exploring abstract algebra in constructive type theory. In Proceedings of 12th International Conference on Automated Deduction, July 1994.","DOI":"10.1007\/3-540-58156-1_43"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"R. Pollack. Dependently typed records for representing mathematical structures. In TPHOLs 2000. Springer-Verlag, 2000.","DOI":"10.1007\/3-540-44659-1_29"},{"key":"20_CR13","unstructured":"L. Pottier. contrib algebra pour coq, mars 1999. http:\/\/pauillac.inria.fr\/coq\/contribs-eng.html ."},{"key":"20_CR14","unstructured":"V. Prevosto, D. Doligez, and T. Hardin. Overview of the Foc compiler, to appear as a research report, LIP6, 2002. available at http:\/\/www-spi.Iip6.fr\/~prevosto\/papiers\/foc2002.ps.gz >."},{"key":"20_CR15","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual. Projet LogiCal, INRIA-Rocquencourt-LRI Paris 11, Nov. 1996."}],"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_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T01:38:09Z","timestamp":1556415489000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_20","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}