{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:42Z","timestamp":1751660502275,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664635"},{"type":"electronic","value":"9783540482567"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48256-3_10","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:15:22Z","timestamp":1186172122000},"page":"131-148","source":"Crossref","is-referenced-by-count":19,"title":["Universal Algebra in Type Theory"],"prefix":"10.1007","author":[{"given":"Venanzio","family":"Capretta","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"10_CR1","unstructured":"Peter Aczel. Notes towards a formalisation of constructive galois theory. draft report, 1994."},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"H. P. Barendregt. Lambda Calculi with Types. In S. Abramsky, Dov M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, Volume 2. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"10_CR3","unstructured":"Bruno Barras, Samuel Boutin, Cristina Cornes, Judica\u00ebl Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filli\u00e2tre, Eduardo Gim\u00e9nez, Hugo Herbelin, G\u00e9rard Huet, Henri Laulh\u00e8re, C\u00e9sar Mu\u00f1oz, Chetan Murthy, Catherine Parent-Vigouroux, Patrick Loiseleur, Christine Paulin-Mohring, Amokrane Sa\u00efbi, and Benjanin Werner. The Coq Proof Assistant Reference Manual. Version 6.2."},{"key":"10_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/3-540-61780-9_59","volume-title":"Types for Proofs and Programs (TYPES\u201995)","author":"G. Barthe","year":"1995","unstructured":"G. Barthe, M. Ruys, and H. P. Barendregt. A two-level approach towards lean proof-checking. In S. Berardi and M. Coppo, editors, Types for Proofs and Programs (TYPES\u201995), volume LNCS 1158, pages 16\u201335. Springer, 1995."},{"key":"10_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/BFb0014565","volume-title":"Theoretical Aspects of Computer Software. Third International Symposium, TACS\u201997","author":"S. Boutin","year":"1997","unstructured":"Samuel Boutin. Using reflection to build efficient and certified decision procedures. In Mart\u00edn Abadi and Takayasu Ito, editors, Theoretical Aspects of Computer Software. Third International Symposium, TACS\u201997, volume LNCS 1281, pages 515\u2013529. Springer, 1997."},{"key":"10_CR6","unstructured":"R. L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986."},{"key":"10_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of Colog\u2019 88","author":"T. Coquand","year":"1990","unstructured":"Thierry Coquand and Christine Paulin. Inductively defined types. In P. Martin-L\u00f6f, editor, Proceedings of Colog\u2019 88, volume 417 of Lecture Notes in Computer Science. Springer-Verlag, 1990."},{"key":"10_CR8","unstructured":"Thierry Coquand and Henrik Persson. Integrated Development of Algebra in Type Theory. Presented at the Calculemus and Types\u2019 98 workshop, 1998."},{"key":"10_CR9","unstructured":"Eduardo Gim\u00e9nez. A Tutorial on Recursive Types in Coq. Technical report, Unit\u00e9 de recherche INRIA Rocquencourt, 1998."},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Martin Hofmann. Elimination of extensionality in Martin-L\u00f6f type theory. In Barendregt and Nipkow, editors, Types for Proofs and Programs. International Workshop TYPES\u2019 93, pages 166\u201390. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-58085-9_76"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Martin Hofmann and Thomas Streicher. A groupoid model refutes uniqueness of identity proofs. In Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 208\u2013212. IEEE Computer Society Press, 1994.","DOI":"10.1109\/LICS.1994.316071"},{"key":"10_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/BFb0012835","volume-title":"9th International Conference on Automated Deduction","author":"D. J. Howe","year":"1988","unstructured":"Douglas J. Howe. Computational metatheory in Nuprl. In E. Lusk and R. Overbeek, editors, 9th International Conference on Automated Deduction, volume LNCS 310, pages 238\u2013257. Springer-Verlag, 1988."},{"key":"10_CR13","unstructured":"G\u00e9rard Huet and Amokrane Sa\u00efbi. Constructive category theory. In In honor of Robin Milner. Cambridge University Press, 1997."},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Paul Jackson. Exploring abstract algebra in constructive type theory. In Automated Deduction \u2014 CADE-12, volume Lectures Notes in Artificial Intelligence 814, pages 591\u2013604. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_43"},{"key":"10_CR15","unstructured":"Zhaohui Luo. Computation and Reasoning, A Type Theory for Computer Science, volume 11 of International Series of Monographs on Computer Science. Oxford University Press, 1994."},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Per Martin-L\u00f6f. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science, VI, 1979, pages 153\u2013175. North-Holland, 1982.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"10_CR17","unstructured":"Per Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, 1984. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980."},{"key":"10_CR18","unstructured":"K. Meinke and J. V. Tucker. Universal Algebra. In S. Abramsky, Dov M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, Volume 1. Oxford University Press, 1992."},{"key":"10_CR19","unstructured":"Bengt Nordstr\u00f6m, Kent Petersson, and Jan M. Smith. Programming in Martin-L\u00f6f\u2019s Type Theory. Clarendon Press, 1990."},{"key":"10_CR20","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the 1989 Conference on Category Theory and Computer Science, Manchester, U.K.","author":"K. Petersson","year":"1989","unstructured":"Kent Petersson and Dan Synek. A Set Constructor for Inductive Sets in Martin-L\u00f6f\u2019s Type Theory. In Proceedings of the 1989 Conference on Category Theory and Computer Science, Manchester, U.K., volume 389 of Lecture Notes in Computer Science. Springer-Verlag, 1989."},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Amokrane Sa\u00efbi. Typing algorithm in type theory with inheritance. In POPL\u201997: The 12th ACM SIGPLAN-SIGACT Symposium on Principles of Programming languages, pages 292\u2013301. Association for Computing Machinery, 1997.","DOI":"10.1145\/263699.263742"},{"key":"10_CR22","unstructured":"Milena Stefanova. Properties of Typing Systems. PhD thesis, Computer Science Institute, University of Nijmegen, 1999."},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Laurent Th\u00e9ry. Proving and Computing: a certified version of the Buchberger\u2019s algorithm. Technical report, INRIA, 1997.","DOI":"10.1007\/BFb0054271"}],"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-48256-3_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T03:46:39Z","timestamp":1737344799000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48256-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}