{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:20Z","timestamp":1761611300036},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581567"},{"type":"electronic","value":"9783540484677"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_43","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:22:59Z","timestamp":1330269779000},"page":"590-604","source":"Crossref","is-referenced-by-count":12,"title":["Exploring abstract algebra in constructive type theory"],"prefix":"10.1007","author":[{"given":"Paul","family":"Jackson","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"43_CR1","unstructured":"Mark Aagaard and Miriam Leeser. The implementation and proof of a boolean simplification system. Technical Report EE-CEG-90-2, Cornell School of Electrical Engineering, March 1990. In the Oxford Workshop on Designing Correct Circuits, September, 1990."},{"key":"43_CR2","unstructured":"Anthony Bailey. Representing algebra in LEGO. Master's thesis, University of Edinburgh, November 1993."},{"key":"43_CR3","unstructured":"David A. Basin and Robert L. Constable. Metalogical frameworks. In G\u00e9rard Huet and Gordon Plotkin, editors, Logical Environments. Cambridge University Press, 1993."},{"key":"43_CR4","doi-asserted-by":"crossref","unstructured":"David A. Basin and Peter Del Vecchio. Verification of combinational logic in Nuprl. In M. E. Leeser and G. M. Brown, editors, Hardware Specification, Verification, and Synthesis: Mathematical Aspects, pages 333\u2013357. Springer Verlag, 1990. LNCS 408.","DOI":"10.1007\/0-387-97226-9_36"},{"key":"43_CR5","unstructured":"Nicolas Bourbaki. Algebra, Part I. Elements of Mathematics. Addison-Wesley, 1974."},{"key":"43_CR6","doi-asserted-by":"crossref","unstructured":"Jawahar Chirimar and Douglas J. Howe. Implementing constructive real analysis: Preliminary report. In Constructivity in Computer Science, volume 613 of Lecture Notes in Computer Science, pages 165\u2013178. Springer-Verlag, 1992.","DOI":"10.1007\/BFb0021090"},{"key":"43_CR7","doi-asserted-by":"crossref","unstructured":"Edmund Clarke and Zhao Xudong. Analytica \u2014 a theorem prover in mathematica. In D. Kapur, editor, 11th Conference on Automated Deduction, volume 607 of Lecture Notes in Artifical Intelligence, pages 761\u2013765. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_220"},{"key":"43_CR8","volume-title":"Implementing Mathematics with The Nuprl Development System","author":"R. Constable","year":"1986","unstructured":"Robert Constable et al. Implementing Mathematics with The Nuprl Development System. Prentice-Hall, NJ, 1986."},{"key":"43_CR9","doi-asserted-by":"crossref","unstructured":"William M. Farmer, Joshua D. Guttman, and F. Javier Thayer. Little theories. In D. Kapur, editor, 11th Conference on Automated Deduction, volume 607 of Lecture Notes in Artifical Intelligence, pages 567\u2013581. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_192"},{"key":"43_CR10","unstructured":"Elsa L. Gunter. Doing algebra in simple type theory. Technical Report MS-CIS-89-38, Department of computer and Information Science, University of Pennsylvania, 1989."},{"key":"43_CR11","doi-asserted-by":"crossref","unstructured":"John V. Guttag and James J. Horning. Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science. Springer-Verlag, 1993.","DOI":"10.1007\/978-1-4612-2704-5"},{"key":"43_CR12","doi-asserted-by":"crossref","unstructured":"John Harrison and Laurent Th\u00e8ry. Extending the HOL theorem prover with a computer algebra system to reason about the reals. In Proceedings of the HOL '93 Workshop on Higher Order Logic Theorem Proving and its Applications, 1993.","DOI":"10.1007\/3-540-57826-9_134"},{"key":"43_CR13","doi-asserted-by":"crossref","unstructured":"Douglas J. Howe. Implementing number theory: An experiment with Nuprl. In Eighth Conference on Automated Deduction, volume 230 of Lecture Notes in Computer Science, pages 404\u2013415. Springer-Verlag, July 1987.","DOI":"10.1007\/3-540-16780-3_108"},{"key":"43_CR14","unstructured":"Douglas J. Howe. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell University, 1988."},{"key":"43_CR15","unstructured":"Paul B. Jackson. Nuprl and its use in circuit design. In R.T. Boute V. Stavridou, T.F.Melham, editor, Proceedings of the 1992 International Conference on Theorem Provers in Circuit Design, IFIP Transactions A-10. North-Holland, 1992."},{"key":"43_CR16","unstructured":"Paul B. Jackson. Enhancing the Nuprl Theorem Prover and Applying it to Constructive Algebra. PhD thesis, Cornell University, 1994. Forthcoming."},{"key":"43_CR17","doi-asserted-by":"crossref","unstructured":"Richard D. Jenks and Robert S. Sutor. AXIOM: the Scientific Computation System. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-2940-7"},{"key":"43_CR18","unstructured":"Serge Lang. Algebra. Addison-Wesley, 2nd edition, 1984."},{"key":"43_CR19","first-page":"153","volume-title":"Constructive mathematics and computer programming","author":"P. Martin-L\u00f6f","year":"1982","unstructured":"Per Martin-L\u00f6f. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153\u2013175, Amsterdam, 1982. North Holland."},{"key":"43_CR20","doi-asserted-by":"crossref","unstructured":"Ray Mines, Fred Richman, and Wim Ruitenburg. A Course in constructive Algebra. Universitext. Springer-Verlag, 1988.","DOI":"10.1007\/978-1-4419-8640-5"},{"key":"43_CR21","doi-asserted-by":"crossref","unstructured":"John C. Mitchell and Gordon Plotkin. Abstract types have existential type. In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages. Association for Computing Machinery, SIGACT, SIGPLAN, 1985.","DOI":"10.1145\/318593.318606"},{"key":"43_CR22","doi-asserted-by":"crossref","unstructured":"Martin Wirsing. Algebraic specification. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 13. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50018-4"},{"key":"43_CR23","doi-asserted-by":"crossref","unstructured":"Richard Zippel. The Weyl computer algebra substrate. In Alfonso Miola, editor, Design and Implementation of Symbolic Computation Systems, volume 722 of Lecture Notes in Computer Science, pages 303\u2013318. Springer Verlag, 1993.","DOI":"10.1007\/BFb0013185"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_43.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:41Z","timestamp":1605647861000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}