{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T23:09:46Z","timestamp":1771888186723,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540678632","type":"print"},{"value":"9783540446590","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44659-1_29","type":"book-chapter","created":{"date-parts":[[2007,7,21]],"date-time":"2007-07-21T13:40:26Z","timestamp":1185025226000},"page":"462-479","source":"Crossref","is-referenced-by-count":11,"title":["Dependently Typed Records for Representing Mathematical Structure"],"prefix":"10.1007","author":[{"given":"Robert","family":"Pollack","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","unstructured":"P. Aczel. Simple overloading for type theories. Privately circulated notes, 1994."},{"key":"29_CR2","unstructured":"A. Bailey. The Machine-checked Literate Formalisation of Algebra in Type Theory. PhD thesis, Univ. of Manchester, 1998."},{"key":"29_CR3","unstructured":"G. Betarte. Dependent Record Types and Formal Abstract Reasoning. PhD thesis, Chalmers Univ. of Technology, 1998."},{"key":"29_CR4","doi-asserted-by":"crossref","unstructured":"G. Betarte and A. Tasistro. Extension of Martin-L\u00f6f\u2019s type theory with record types and subtyping. In G. Sambin and J. Smith, editors, Twenty Five Years of Constructive Type Theory. Oxford Univ. Press, 1998.","DOI":"10.1007\/BFb0097801"},{"key":"29_CR5","unstructured":"The Coq Project, 1999. http:\/\/pauillac.inria.fr\/coq\/ ."},{"key":"29_CR6","unstructured":"J. Courant. MC: A module calculus for Pure Type Systems. Technical Report 1217, CNRS Universit\u00e9 Paris Sud 8623: LRI, June 1999."},{"issue":"2","key":"29_CR7","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/0890-5401(91)90066-B","volume":"91","author":"N. G. Bruijn de","year":"1991","unstructured":"N. G. de Bruijn. Telescopic mappings in typed lambda calculus. Information and Computation, 91(2):189\u2013204, April 1991.","journal-title":"Information and Computation"},{"key":"29_CR8","unstructured":"Peter Dybjer. A general notion of simultaneous inductive-recursive definition in type theory. Journal of Symbolic Logic, 1997. To appear."},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In POPL\u201994. ACM Press, 1994.","DOI":"10.1145\/174675.176927"},{"key":"29_CR10","series-title":"Lect Notes Comput Sci","volume-title":"TYPES\u201998, Selected Papers","author":"F. Kamm\u00fcller","year":"1999","unstructured":"F. Kamm\u00fcller. Modular structures as dependent types in isabelle. In T. Altenkirch, W. Naraschewski, and B. Reus, editors, TYPES\u201998, Selected Papers, volume 1657 of LNCS. Springer-Verlag, 1999."},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"B. Lampson and R. Burstall. Pebble, a kernel language for modules and abstract data types. Information and Computation, 76(2\/3), 1988.","DOI":"10.1016\/0890-5401(88)90011-9"},{"key":"29_CR12","unstructured":"The LEGO Proof Assistant, 1999. http:\/\/www.dcs.ed.ac.uk\/home\/lego\/ ."},{"key":"29_CR13","doi-asserted-by":"crossref","unstructured":"X. Leroy. Manifest types, modules, and separate compilation. In POPL\u201994, New York, NY, USA, 1994. ACM Press.","DOI":"10.1145\/174675.176926"},{"key":"29_CR14","doi-asserted-by":"crossref","unstructured":"Z. Luo and S. Soloviev. Dependent coercions. In Category Theory in Computer Science, CTCS\u201999, Electronic Notes in Theoretical Computer Science. Elsevier, 1999.","DOI":"10.1016\/S1571-0661(05)80314-7"},{"key":"29_CR15","doi-asserted-by":"crossref","unstructured":"Z. Luo. Coercive subtyping. Journal of Logic and Computation, 9(1), 1999.","DOI":"10.1093\/logcom\/9.1.105"},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"D. MacQueen. Using dependent types to express modular structure. In POPL\u201986, 1986.","DOI":"10.1145\/512644.512670"},{"key":"29_CR17","unstructured":"Loic Pottier. Algebra with Coq. See User contributions in Coq release [Coq99], 1999."},{"key":"29_CR18","doi-asserted-by":"crossref","unstructured":"A. Saibi. Typing algorithm in type theory with inheritance. POPL\u201997, 1997.","DOI":"10.1145\/263699.263742"},{"key":"29_CR19","unstructured":"A. Tasistro. Substitution, Record Types and Subtyping in Type Theory, with Applications to the Theory of Programming. PhD thesis, Chalmers Univ. of Technology, May 1997."}],"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-44659-1_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T10:06:40Z","timestamp":1683972400000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44659-1_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678632","9783540446590"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-44659-1_29","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]}}}