{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:20:11Z","timestamp":1742617211069,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540613770"},{"type":"electronic","value":"9783540685074"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61377-3_30","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:36:18Z","timestamp":1330292178000},"page":"36-51","source":"Crossref","is-referenced-by-count":5,"title":["Congruence Types"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Herman","family":"Geuvers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"3_CR1","unstructured":"S. Abramsky, D. Gabbay, and T. Maibaum, editors. Handbook of Logic in Computer Science. Oxford Science Publications, 1992."},{"key":"3_CR2","first-page":"68","volume":"34","author":"R. Backhouse","year":"1988","unstructured":"R. Backhouse, P. Chisholm, and G. Malcolm. Do-it-yourself type theory (part I). BEATCS: Bulletin of the European Association for Theoretical Computer Science, 34:68\u2013110, 1988.","journal-title":"BEATCS: Bulletin of the European Association for Theoretical Computer Science"},{"key":"3_CR3","first-page":"205","volume":"35","author":"R. Backhouse","year":"1988","unstructured":"R. Backhouse, P. Chisholm, and G. Malcolm. Do-it-yourself type theory (part II). BEATCS; Bulletin of the European Association for Theoretical Computer Science, 35:205\u2013244, 1988.","journal-title":"BEATCS; Bulletin of the European Association for Theoretical Computer Science"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"F. Barbanera, M. Fernandez, and H. Geuvers. Modularity of strong normalisation and confluence in the algebraic \u03bb-cube. In Proceedings of LICS'94, pages 406\u2013415. IEEE Computer Society Press, 1994.","DOI":"10.1109\/LICS.1994.316049"},{"key":"3_CR5","unstructured":"H.P. Barendregt. Lambda calculi with types. In Abramsky et al. [1], pages 117\u2013309. Volume 2."},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"G. Barthe. Extensions of pure type systems. In Dezani-Ciancaglini and Plotkin [16], pages 16\u201331.","DOI":"10.1007\/BFb0014042"},{"key":"3_CR7","unstructured":"G. Barthe. Formalising algebra in type theory: fundamentals and applications to group theory. Manuscript. An earlier version appeared as technical report CSIR9508, University of Nijmegen, under the title \u2018Formalising mathematics in type theory: fundamentals and case studies', 1995."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"G. Barthe and H. Eibers. Towards lean proof checking. Manuscript, 1996.","DOI":"10.1007\/3-540-61697-7_5"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"G. Barthe and H. Geuvers. Modular properties of algebraic pure type systems. In G. Dowek, J. Heering, K. Meinke, and B. M\u00f6ller, editors, Proceedings of HOA '95, Lecture Notes in Computer Science. Springer-Verlag, 1996. To appear.","DOI":"10.1007\/3-540-61254-8_18"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"G. Barthe, M. Ruys, and H. Barendregt. A two-level approach towards lean proof-checking. In S. Berardi and M. Coppo, editors, Proceedings of TYPES'95, Lecture Notes in Computer Science. Springer-Verlag, 1996. To appear.","DOI":"10.1007\/3-540-61780-9_59"},{"key":"3_CR11","unstructured":"G. Betarte. A machine-assisted proof that the integers form an integral domain. Master's thesis, Department of Computer Science, Chalmers University, 1993."},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen. Combining algebra and higher-order types. In Proceedings of LICS'88, pages 82\u201390. IEEE Computer Society Press, 1988.","DOI":"10.1109\/LICS.1988.5103"},{"key":"3_CR13","volume-title":"Implementing Mathematics with the NuPrl Development System","author":"R.L. Constable","year":"1986","unstructured":"R.L. Constable, S.F. Alien, H.M. Bromley, W.R. Cleaveland, J.F. Cremer, R.W. Harper, D.J. Howe, T.B. Knoblock, N.P. Mendier, P. Panangaden, J.T. Sasaki, and S.F. Smith. Implementing Mathematics with the NuPrl Development System. Prentice-Hall, inc., Englewood Cliffs, New Jersey, first edition, 1986.","edition":"first edition"},{"key":"3_CR14","unstructured":"T. Coquand. Pattern matching in type theory. In B. Nordstr\u00f6m, editor, Informal proceedings of LF'92, pages 66\u201379, 1992. Available from http:\/\/www.dcs.ed.ac.uk\/lfcsinfo\/research\/types-bra\/proc\/index.html."},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Formal models and semantics. Handbook of Theoretical Computer Science, volume B, pages 243\u2013320. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"3_CR16","unstructured":"M. Dezani-Ciancaglini and G. Plotkin, editors. Proceedings of TLCA'95, volume 902 of Lecture Notes in Computer Science. Springer-Verlag, 1995."},{"key":"3_CR17","unstructured":"H. Geuvers. Logics and type systems. PhD thesis, University of Nijmegen, 1993."},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"H. Geuvers. A short and flexible proof of strong normalisation for the calculus of constructions. In P. Dybjer, B. Nordstrom, and J. Smith, editors, Proceedings of TYPES'94, volume 996 of Lecture Notes in Computer Science, pages 14\u201338. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60579-7_2"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"H. Geuvers and B. Werner. On the Church-Rosser property for expressive type systems and its consequence for their metatheoretic study. In Proceedings of LICS'94, pages 320\u2013329. IEEE Computer Society Press, 1994.","DOI":"10.1109\/LICS.1994.316057"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"M. Hofmann, A simple model for quotient types. In Dezani-Ciancaglini and Plotkin [16], pages 216\u2013234.","DOI":"10.1007\/BFb0014055"},{"key":"3_CR21","unstructured":"B. Jacobs. Categorical logic and type theory. 199-. Book. In preparation."},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"J-P. Jouannaud and M. Okada. Executable higher-order algebraic specification languages. In Proceedings of LICS'91, pages 350\u2013361. IEEE Computer Society Press, 1991.","DOI":"10.1109\/LICS.1991.151659"},{"key":"3_CR23","unstructured":"J-W. Klop. Term-rewriting systems. In Abramsky et al. [1], pages 1\u2013116. Volume 2."},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. Number 11 in International Series of Monographs on Computer Science. Oxford University Press, 1994.","DOI":"10.1093\/oso\/9780198538356.001.0001"},{"key":"3_CR25","unstructured":"B. Nordstr\u00f6m, K. Peterssoll, and J. Smith. Programming in Martin-Lof's Type Theory. An Introduction. Number 7 in International Series of Monographs on Computer Science. Oxford University Press, 1990."},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Inductive definitions in the system Coq. Rules and properties. In M. Bezem and J-F. Groote, editors, Proceedings of TLCA'93, volume 664 of Lecture Notes in Computer Science, pages 328\u2013345. Springer-Verlag, 1993.","DOI":"10.1007\/BFb0037116"},{"key":"3_CR27","unstructured":"M.J. Plasmeijer and M.C.J.D. van Eekelen. Clean 1.0 reference manual. Technical report, Department of Computer Science, University of Nijmegen, 1996. In preparation."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61377-3_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:18:48Z","timestamp":1742599128000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61377-3_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540613770","9783540685074"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-61377-3_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}