{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,26]],"date-time":"2026-03-26T05:28:42Z","timestamp":1774502922595,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540440390","type":"print"},{"value":"9783540456858","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_18","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T20:47:53Z","timestamp":1179607673000},"page":"263-280","source":"Crossref","is-referenced-by-count":14,"title":["Quotient Types: A Modular Approach"],"prefix":"10.1007","author":[{"given":"Aleksey","family":"Nogin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"18_CR1","unstructured":"Stuart F. Allen. A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Cornell University, 1987."},{"key":"18_CR2","unstructured":"Stuart F. Allen. A Non-type-theoretic Definition of Martin-L\u00f6f\u2019 s Types. In Proceedings of the Second Symposium on Logic in Computer Science, pages 215\u2013224. IEEE, June 1987."},{"key":"18_CR3","unstructured":"Roland Backhouse. A note of subtypes in Martin-L\u00f6f\u2019 s theory of types. Technical Report CSM-90, University of Essex, November 1984."},{"key":"18_CR4","unstructured":"Roland Backhouse. On the meaning and construction of the rules in Martin-L\u00f6f\u2019 s theory of types. In A. Avron, editor, Workshop on General Logic, Edinburgh, February 1987, number ECS-LFCS-88-52. Department of Computer Science, University of Edinburgh, May 1988."},{"key":"18_CR5","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/BF01887198","volume":"1","author":"R. C. Backhouse","year":"1989","unstructured":"Roland C. Backhouse, Paul Chisholm, Grant Malcolm, and Erik Saaman. Do-it-yourself type theory. Formal Aspects of Computing, 1:19\u201384, 1989.","journal-title":"Formal Aspects of Computing"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Ken Birman, Robert Constable, Mark Hayden, Jason J. Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, and Werner Vogels. The Horus and Ensemble projects: Accomplishments and limitations. In DARPA Information Survivability Conference and Exposition (DISCEX 2000), pages 149\u2013161. IEEE, 2000.","DOI":"10.1109\/DISCEX.2000.824975"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Robert L. Constable. Mathematics as programming. In Proceedings of the Workshop on Programming and Logics, Lectures Notes in Computer Science 164, pages 116\u2013128. Springer-Verlag, 1983.","DOI":"10.1007\/3-540-12896-4_359"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Robert L. Constable. Types in logic, mathematics, and programming. In S. R. Buss, editor, Handbook of Proof Theory, chapter X, pages 683\u2013786. Elsevier Science B.V., 1998.","DOI":"10.1016\/S0049-237X(98)80025-6"},{"key":"18_CR9","volume-title":"Implementing Mathematics with the NuPRL Development System","author":"R. L. Constable","year":"1986","unstructured":"Robert L. Constable, Stuart F. Allen, H.M. Bromley, W.R. Cleaveland, J.F. Cremer, R.W. Harper, Douglas J. Howe, T.B. Knoblock, N.P. Mendler, P. Panangaden, James T. Sasaki, and Scott F. Smith. Implementing Mathematics with the NuPRL Development System. Prentice-Hall, NJ, 1986."},{"key":"18_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"554","DOI":"10.1007\/3-540-44802-0_39","volume-title":"Computer Science Logic, Proceedings of the 10th Annual Conference of the EACSL","author":"P. Courtieu","year":"2001","unstructured":"Pierre Courtieu. Normalized types. In L. Fribourg, editor, Computer Science Logic, Proceedings of the 10th Annual Conference of the EACSL, volume 2142 of Lecture Notes in Computer Science, pages 554\u2013569. Springer-Verlag, 2001. http:\/\/link.springer-ny.com\/link\/service\/series\/0558\/tocs\/t2142.htm ."},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Jason J. Hickey. NuPRL-Light: An implementation framework for higer-order logics. In William McCune, editor, Proceedings of the 14th International Conference on Automated Deduction, volume 1249 of Lecture Notes on Artificial Intelligence, pages 395\u2013399, Berlin, July 13\u201317 1997. Springer. CADE\u201997. An extended version of the paper can be found at http:\/\/www.cs.caltech.edu\/~jyh\/papers\/cade14_nl\/default.html .","DOI":"10.1007\/3-540-63104-6_37"},{"key":"18_CR12","series-title":"PhD thesis","volume-title":"The MetaPRL Logical Programming Environment","author":"J. J. Hickey","year":"2001","unstructured":"Jason J. Hickey. The MetaPRL Logical Programming Environment. PhD thesis, Cornell University, Ithaca, NY, January 2001."},{"key":"18_CR13","unstructured":"Jason J. Hickey, Brian Aydemir, Yegor Bryukhov, Alexei Kopylov, Aleksey Nogin, and Xin Yu. A listing of MetaPRL theories. http:\/\/metaprl.org\/theories.pdf ."},{"key":"18_CR14","unstructured":"Jason J. Hickey, Aleksey Nogin, Alexei Kopylov, et al. MetaPRL home page. http:\/\/metaprl.org\/ ."},{"key":"18_CR15","unstructured":"Martin Hofmann. Extensional concepts in intensional Type theory. PhD thesis, University of Edinburgh, Laboratory for Foundations of Computer Science, July 1995."},{"key":"18_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/BFb0014055","volume-title":"Typed Lambda Calculus and Applications","author":"M. Hofmann","year":"1995","unstructured":"Martin Hofmann. A simple model for quotient types. In Typed Lambda Calculus and Applications, volume 902 of Lecture Notes in Computer Science, pages 216\u2013234, 1995."},{"key":"18_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/BFb0014309","volume-title":"Algebraic Methodology and Software Technology","author":"D. J. Howe","year":"1996","unstructured":"Douglas J. Howe. Semantic foundations for embedding HOL in NuPRL. In Martin Wirsing and Maurice Nivat, editors, Algebraic Methodology and Software Technology, volume 1101 of Lecture Notes in Computer Science, pages 85\u2013101. Springer-Verlag, Berlin, 1996."},{"key":"18_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"570","DOI":"10.1007\/3-540-44802-0_40","volume-title":"Computer Science Logic, Proceedings of the 10th Annual Conference of the EACSL","author":"A. Kopylov","year":"2001","unstructured":"Alexei Kopylov and Aleksey Nogin. Markov\u2019s principle for propositional type theory. In L. Fribourg, editor, Computer Science Logic, Proceedings of the 10th Annual Conference of the EACSL, volume 2142 of Lecture Notes in Computer Science, pages 570\u2013584. Springer-Verlag, 2001. http:\/\/link.springer-ny.com\/link\/service\/series\/0558\/tocs\/t2142.htm ."},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Xiaoming Liu, Christoph Kreitz, Robbert van Renesse, Jason J. Hickey, Mark Hayden, Kenneth Birman, and Robert Constable. Building reliable, high-performance communication systems from components. In 17 th ACM Symposium on Operating Systems Principles, December 1999.","DOI":"10.1145\/319151.319157"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Per Martin-L\u00f6f. Constructive mathematics and computer programming. In Proceedings of the Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153\u2013175, Amsterdam, 1982. North Holland.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"18_CR21","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1016\/S0049-237X(08)72018-4","volume-title":"Computer Programming and Formal Systems","author":"J. McCarthy","year":"1963","unstructured":"J. McCarthy. A basis for a mathematical theory of computation. In P. Braffort and D. Hirschberg, editors, Computer Programming and Formal Systems, pages 33\u201370. Amsterdam: North-Holland, 1963."},{"key":"18_CR22","unstructured":"Aleksey Nogin. Quotient types \u2014 A modular approach. Department of Computer Science http:\/\/cs-tr.cs.cornell.edu\/Dienst\/UI\/1.0\/Display\/ncstrl.cornell\/ TR2002-1869 TR2002-1869, Cornell University, April 2002. See also http:\/\/nogin.org\/papers\/quotients.html ."},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Aleksey Nogin and Jason Hickey. Sequent schema for derived rules. Accepted to TPHOLs 2002, 2002.","DOI":"10.1007\/3-540-45685-6_19"},{"key":"18_CR24","unstructured":"Bengt Nordstr\u00f6m and Kent Petersson. Types and specifications. In IFIP\u201993. Elsvier, 1983."},{"key":"18_CR25","volume-title":"Programming in Martin-L\u00f6f\u2019s Type Theory","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Bengt Nordstr\u00f6m, Kent Petersson, and Jan M. Smith. Programming in Martin-L\u00f6f\u2019s Type Theory. Oxford Sciences Publication, Oxford, 1990."},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Frank Pfenning and Rowan Davies. Judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4), August 2001.","DOI":"10.1017\/S0960129501003322"},{"key":"18_CR27","unstructured":"Simon Thompson. Type Theory and Functional Programming. Addison-Wesley, 1991."},{"key":"18_CR28","doi-asserted-by":"crossref","unstructured":"Anne Sjerp Troelstra. Metamathematical Investigation of Intuitionistic Mathematics, volume 344 of Lecture Notes in Mathematics. Springer-Verlag, 1973.","DOI":"10.1007\/BFb0066739"}],"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_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T13:31:22Z","timestamp":1737034282000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}