{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T14:10:05Z","timestamp":1737123005295,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":145,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540440444"},{"type":"electronic","value":"9783540456995"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45699-6_1","type":"book-chapter","created":{"date-parts":[[2007,5,21]],"date-time":"2007-05-21T21:00:01Z","timestamp":1179781201000},"page":"1-41","source":"Crossref","is-referenced-by-count":0,"title":["An Introduction to Dependent Type Theory"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Thierry","family":"Coquand","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"1_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44557-9_1","volume-title":"Proceedings of TYPES\u201999","author":"A. Abel","year":"2000","unstructured":"A. Abel. On relating type theories and set theories. In T. Coquand, P. Dybjer, B. Nordstr\u00f6m, and J. Smith, editors, Proceedings of TYPES\u201999, volume 1956 of Lecture Notes in Computer Science, pages 1\u201320. Springer-Verlag, 2000."},{"key":"1_CR2","unstructured":"A. Abel. Termination checking with types. Technical Report 0201, Institut fur Informatik, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, 2002."},{"issue":"1","key":"1_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0956796801004191","volume":"12","author":"A. Abel","year":"2002","unstructured":"A. Abel and T. Altenkirch. A predicative analysis of structural recursion. Journal of Functional Programming, 12(1):1\u201341, January 2002.","journal-title":"Journal of Functional Programming"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"P. Aczel. The Type Theoretic Interpretation of Constructive Set Theory. In A. MacIntyre, A. Pacholski, and J. Paris, editors, Proceedings of Logic Colloqium 77, Studies in Logic and the Foundations of Mathematics, pages 55\u201366. North-Holland, 1978.","DOI":"10.1016\/S0049-237X(08)71989-X"},{"key":"1_CR5","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/S0049-237X(08)71252-7","volume-title":"Proceedings of the Kleene Symposium","author":"P. Aczel","year":"1980","unstructured":"P. Aczel. Frege structures and the notions of proposition, truth and set. In J. Barwise, H. J. Keisler, and K. Kunen, editors, Proceedings of the Kleene Symposium, volume 101 of Studies in Logic and the Foundations of Mathematics, pages 31\u201359. North-Holland, Amsterdam, 1980."},{"key":"1_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-48167-2_1","volume-title":"Proceedings of TYPES\u201998","author":"P. Aczel","year":"1999","unstructured":"P. Aczel. On Relating Type Theories and Set Theories. In T. Altenkirch, W. Naraschewski, and B. Reus, editors, Proceedings of TYPES\u201998, volume 1657 of Lecture Notes in Computer Science, pages 1\u201318. Springer-Verlag, 1999."},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"T. Altenkirch and C. McBride. Generic programming within dependently typed programming. In J. Gibbons and J. Jeuring, editors, Proceedings of WCGP\u201902. Kluwer Academic Publishers, 2002.","DOI":"10.1007\/978-0-387-35672-3_1"},{"key":"1_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/BFb0053541","volume-title":"Proceedings of FOSSACS\u201998","author":"R. Amadio","year":"1998","unstructured":"R. Amadio and S. Coupet-Grimal. Analysis of a guard condition in type theory. In M. Nivat, editor, Proceedings of FOSSACS\u201998, volume 1378 of Lecture Notes in Computer Science, pages 48\u201362. Springer-Verlag, 1998."},{"issue":"4","key":"1_CR9","doi-asserted-by":"crossref","first-page":"575","DOI":"10.1145\/155183.155231","volume":"15","author":"R. M. Amadio","year":"1993","unstructured":"R. M. Amadio and L. Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575\u2013631, September 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR10","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Proceedings of CSL\u201994","author":"D. Aspinall","year":"1994","unstructured":"D. Aspinall. Subtyping with singleton types. In L. Pacholski and J. Tiuryn, editors, Proceedings of CSL\u201994, volume 933 of Lecture Notes in Computer Science, pages 1\u201315. Springer-Verlag, 1994."},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"P. Audebaud. Partial Objects in the Calculus of Constructions. In Proceedings of LICS\u201991, pages 86\u201395. IEEE Computer Society Press, 1991.","DOI":"10.1109\/LICS.1991.151633"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"L. Augustsson. Cayenne: A language with dependent types. In Proceedings of ICFP\u201998, pages 239\u2013250. ACM Press, 1998.","DOI":"10.1145\/289423.289451"},{"key":"1_CR13","unstructured":"L. Augustsson and M. Carlsson. An exercise in dependent types: A well-typed interpreter. In Informal Proceedings of DTP\u201999, 1999."},{"key":"1_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1007\/10704973_2","volume-title":"Proceedings of AFP\u201998","author":"R. Backhouse","year":"1999","unstructured":"R. Backhouse, P. Jansson, J. Jeuring, and L. Meertens. Generic programming\u2014 an introduction. In S. D. Swierstra, P. R. Henriques, and J. N. Oliveira, editors, Proceedings of AFP\u201998, volume 1608 of Lecture Notes in Computer Science, pages 28\u2013115. Springer-Verlag, 1999."},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"S. van Bakel, L. Liquori, S. Ronchi della Rocca, and P. Urzyczyn. Comparing cubes of typed and type assignment systems. Annals of Pure and Applied Logic, 86(3):267\u2013303, July 1997.","DOI":"10.1016\/S0168-0072(96)00036-X"},{"issue":"2","key":"1_CR16","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H. Barendregt","year":"1991","unstructured":"H. Barendregt. Introduction to Generalised Type Systems. Journal of Functional Programming, 1(2):125\u2013154, April 1991.","journal-title":"Journal of Functional Programming"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"H. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, pages 117\u2013309. Oxford Science Publications, 1992. Volume 2.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"H. Barendregt and H. Geuvers. Proof assistants using dependent type systems. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 18, pages 1149\u20131238. Elsevier Publishing, 2001.","DOI":"10.1016\/B978-044450813-3\/50020-5"},{"key":"1_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/BFb0055781","volume-title":"Proceedings of MFCS\u201998","author":"G. Barthe","year":"1998","unstructured":"G. Barthe. The semi-full closure of Pure Type Systems. In L. Brim, J. Gruska, and J. Zlatuska, editors, Proceedings of MFCS\u201998, volume 1450 of Lecture Notes in Computer Science, pages 316\u2013325. Springer-Verlag, 1998."},{"issue":"6","key":"1_CR20","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1017\/S0956796899003573","volume":"9","author":"G. Barthe","year":"1999","unstructured":"G. Barthe. Type-Checking Injective Pure Type Systems. Journal of Functional Programming, 9(6):675\u2013698, 1999.","journal-title":"Journal of Functional Programming"},{"key":"1_CR21","unstructured":"G. Barthe and T. Coquand. On the equational theory of non-normalizing pure type systems. Journal of Functional Programming, 200x. To appear."},{"key":"1_CR22","unstructured":"G. Barthe, M. J. Frade, E. Gim\u00e9nez, L. Pinto, and T. Uustalu. Type-based termination of recursive definitions. Mathematical Structures in Computer Science, 2002. To appear."},{"issue":"5","key":"1_CR23","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1017\/S0956796800003750","volume":"10","author":"G. Barthe","year":"2000","unstructured":"G. Barthe and M.H. S\u00f8rensen. Domain-free pure type systems. Journal of Functional Programming, 10(5):417\u2013452, September 2000.","journal-title":"Journal of Functional Programming"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"D. Basin and S. Matthews. Logical Frameworks. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume 9. Kluwer Academic Publishers, 2002.","DOI":"10.1007\/978-94-017-0464-9_2"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"L.S. van Benthem Jutting. Typing in pure type systems. Information and Computation, 105(1):30\u201341, July 1993.","DOI":"10.1006\/inco.1993.1038"},{"key":"1_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/3-540-58085-9_71","volume-title":"Proceedings of TYPES\u201993","author":"L.S. Benthem Jutting van","year":"1994","unstructured":"L.S. van Benthem Jutting, J. McKinna, and R. Pollack. Checking algorithms for pure type systems. In H. Barendregt and T. Nipkow, editors, Proceedings of TYPES\u201993, volume 806 of Lecture Notes in Computer Science, pages 19\u201361. Springer-Verlag, 1994."},{"key":"1_CR27","unstructured":"G. Betarte. Dependent Record Types and Algebraic Structures in Type Theory. PhD thesis, Department of Computer Science, Chalmers Tekniska H\u00f6gskola, 1998."},{"key":"1_CR28","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 University Press, 1998.","DOI":"10.1007\/BFb0097801"},{"key":"1_CR29","unstructured":"R. Bird. Introduction to Functional Programming using Haskell. Prenctice Hall, 2 edition, 1998."},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"F. Blanqui, J.-P. Jouannaud, and M. Okada. Inductive Data Type Systems. Theoretical Computer Science, 272(1\/2):41\u201368, February 2002.","DOI":"10.1016\/S0304-3975(00)00347-9"},{"key":"1_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/3-540-63166-6_15","volume-title":"Proceedings of CAV\u201997","author":"D. Bolignano","year":"1997","unstructured":"D. Bolignano. Towards a mechanization of cryptographic protocol verification. In O. Grumberg, editor, Proceedings of CAV\u201997, volume 1254 of Lecture Notes in Computer Science, pages 131\u2013142. Springer-Verlag, 1997."},{"issue":"4","key":"1_CR32","doi-asserted-by":"crossref","first-page":"309","DOI":"10.3233\/FI-1998-33401","volume":"33","author":"M. Brandt","year":"1998","unstructured":"M. Brandt and F. Henglein. Coinductive axiomatization of recursive type equality and subtyping. Fundamenta Informaticae, 33(4):309\u2013338, April 1998.","journal-title":"Fundamenta Informaticae"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"W. Buchholz, S. Feferman, W. Pohlers, and W. Sieg. Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Results, volume 897 of Lectures Notes in Mathematics. Springer-Verlag, 1981.","DOI":"10.1007\/BFb0091894"},{"key":"1_CR34","unstructured":"L. Cardelli. A polymorphic lambda-calculus with Type:Type. Technical Report 10, SRC, May 1986."},{"key":"1_CR35","unstructured":"L. Cardelli. Phase distinctions in type theory. Unpublished Mansucript, January 1988."},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"L. Cardelli. Structural subtyping and the notion of power type. In Proceedings of POPL\u201988, pages 70\u201379. ACM Press, 1988.","DOI":"10.1145\/73560.73566"},{"key":"1_CR37","unstructured":"C. Coquand. Agda. See http:\/\/www.cs.chalmers.se\/~catarina\/agda ."},{"key":"1_CR38","unstructured":"C. Coquand. Computation in Type Theory. PhD thesis, Department of Computing Science, Chalmers University of Technology, 1996."},{"key":"1_CR39","unstructured":"T. Coquand. Metamathematical Investigations of a Calculus of Constructions. In P. Odifreddi, editor, Logic and Computer Science, pages 91\u2013122. Academic Press, 1990."},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"T. Coquand. An algorithm for testing conversion in type theory. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 255\u2013279. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.011"},{"key":"1_CR41","unstructured":"T. Coquand. Pattern matching with dependent types. In B. Nordstr\u00f6m, editor, Informal proceedings of Logical Frameworks\u201992, pages 66\u201379, 1992."},{"issue":"1\u20133","key":"1_CR42","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/0167-6423(95)00021-6","volume":"26","author":"T. Coquand","year":"1996","unstructured":"T. Coquand. An algorithm for type-checking dependent types. Science of Computer Programming, 26(1\u20133):167\u2013177, May 1996.","journal-title":"Science of Computer Programming"},{"key":"1_CR43","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1007\/3-540-58715-2_114","volume-title":"Proceedings of FSTTCS\u201994","author":"T. Coquand","year":"1994","unstructured":"T. Coquand and P. Dybjer. Inductive definitions and type theory: an introduction (preliminary version). In P.S. Thiagarajan, editor, Proceedings of FSTTCS\u201994, volume 880 of Lecture Notes in Computer Science, pages 60\u201376. Springer-Verlag, 1994."},{"issue":"1","key":"1_CR44","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1017\/S0956796800000952","volume":"4","author":"T. Coquand","year":"1994","unstructured":"T. Coquand and H. Herbelin. A-translation and looping combinators in pure type systems. Journal of Functional Programming, 4(1):77\u201388, January 1994.","journal-title":"Journal of Functional Programming"},{"key":"1_CR45","doi-asserted-by":"crossref","unstructured":"T. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, 76(2\/3):95\u2013120, February\/March 1988.","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"1_CR46","series-title":"Lect Notes Comput Sci","first-page":"50","volume-title":"Proceedings of COLOG\u201988","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and C. Paulin. Inductively defined types. In P. Martin-L\u00f6f and G. Mints, editors, Proceedings of COLOG\u201988, volume 417 of Lecture Notes in Computer Science, pages 50\u201366. Springer-Verlag, 1988."},{"key":"1_CR47","unstructured":"T. Coquand, R. Pollack, and M. Takeyama. Modules as Dependently Typed Records. Manuscript, 2002."},{"key":"1_CR48","unstructured":"J. Courant. Un calcul de modules pour les syst\u00e8mes de types purs. PhD thesis, Ecole Normale Sup\u00e9rieure de Lyon, 1998."},{"key":"1_CR49","doi-asserted-by":"crossref","unstructured":"G. Cousineau and M. Mauny. The functional approach to programming. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139173018"},{"key":"1_CR50","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Proceedings of TIC\u201900","author":"K. Crary","year":"2001","unstructured":"K. Crary. Sound and complete elimination of singleton kinds. In R. Harper, editor, Proceedings of TIC\u201900, volume 2071 of Lecture Notes in Computer Science, pages 1\u201326. Springer-Verlag, 2001."},{"key":"1_CR51","doi-asserted-by":"crossref","unstructured":"K. Crary and S. Weirich. Resource bound certification. In Proceedings of POPL\u201900, pages 184\u2013198. ACM Press, 2000.","DOI":"10.1145\/325694.325716"},{"key":"1_CR52","doi-asserted-by":"crossref","unstructured":"P. Dybjer. Inductive sets and families in Martin-L\u00f6f\u2019s type theory and their set-theoretic semantics. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 280\u2013306. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.012"},{"key":"1_CR53","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BF01211308","volume":"6","author":"P. Dybjer","year":"1994","unstructured":"P. Dybjer. Inductive families. Formal Aspects of Computing, 6:440\u2013465, 1994.","journal-title":"Formal Aspects of Computing"},{"issue":"1\u20132","key":"1_CR54","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/S0304-3975(96)00145-4","volume":"176","author":"P. Dybjer","year":"1997","unstructured":"P. Dybjer. Representing inductively defined sets by well-orderings in Martin-L\u00f6f\u2019s type theory. Theoretical Computer Science, 176(1\u20132):329\u2013335, April 1997.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"1_CR55","doi-asserted-by":"crossref","first-page":"525","DOI":"10.2307\/2586554","volume":"65","author":"P. Dybjer","year":"2000","unstructured":"P. Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2):525\u2013549, June 2000.","journal-title":"Journal of Symbolic Logic"},{"key":"1_CR56","unstructured":"H. Geuvers. Logics and type systems. PhD thesis, University of Nijmegen, 1993."},{"key":"1_CR57","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/3-540-45413-6_16","volume-title":"Proceedings of TLCA\u201901","author":"H. Geuvers","year":"2001","unstructured":"H. Geuvers. Induction is not derivable in second order dependent type theory. In S. Abramsky, editor, Proceedings of TLCA\u201901, Lecture Notes in Computer Science, pages 166\u2013181. Springer-Verlag, 2001."},{"issue":"2","key":"1_CR58","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"H. Geuvers and M.J. Nederhof. A modular proof of strong normalisation for the Calculus of Constructions. Journal of Functional Programming, 1(2):155\u2013189, April 1991.","journal-title":"Journal of Functional Programming"},{"key":"1_CR59","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"439","DOI":"10.1007\/3-540-48168-0_31","volume-title":"Proceedings of CSL\u201999","author":"H. Geuvers","year":"1999","unstructured":"H. Geuvers, E. Poll, and J. Zwanenburg. Safe proof checking in type theory with Y. In J. Flum and M. Rodr\u00edguez-Artalejo, editors, Proceedings of CSL\u201999, volume 1683 of Lecture Notes in Computer Science, pages 439\u2013452. Springer-Verlag, 1999."},{"key":"1_CR60","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\u201994, pages 320\u2013329. IEEE Computer Society Press, 1994.","DOI":"10.1109\/LICS.1994.316057"},{"key":"1_CR61","doi-asserted-by":"crossref","unstructured":"J. Giesl, C. Walther, and J. Brauburger. Termination analysis for functional programs. In W. Bibel and P. Schmitt, editors, Automated Deduction-A Basis for Applications, volume 3 of Applied Logic Series, pages 135\u2013164. Kluwer Academic Publishers, 1998.","DOI":"10.1007\/978-94-017-0437-3_6"},{"key":"1_CR62","unstructured":"E. Gim\u00e9nez. Un calcul de constructions infinies et son application \u00e0 la v\u00e9rification de syst\u00e8mes communicants. PhD thesis, Ecole Normale Superieure de Lyon, 1996."},{"key":"1_CR63","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/BFb0055070","volume-title":"Proceedings of ICALP\u201998","author":"E. Gim\u00e9nez","year":"1998","unstructured":"E. Gim\u00e9nez. Structural recursive definitions in Type Theory. In K.G. Larsen, S. Skyum, and G. Winskel, editors, Proceedings of ICALP\u201998, volume 1443 of Lecture Notes in Computer Science, pages 397\u2013408. Springer-Verlag, 1998."},{"key":"1_CR64","unstructured":"J-Y. Girard. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Th\u00e8se d\u2019Etat, Universit\u00e9 Paris 7, 1972."},{"key":"1_CR65","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Number 7 in Tracts in Theoretical Computer Science. Cambridge University Press, 1989."},{"key":"1_CR66","doi-asserted-by":"crossref","unstructured":"B. Gr\u00e9goire and X. Leroy. A compiled implementation of strong reduction. In Proceedings of ICFP\u201902. ACM Press, 2002.","DOI":"10.1145\/581478.581501"},{"key":"1_CR67","doi-asserted-by":"crossref","unstructured":"B. Grobauer. Cost recurrences for DML programs. In Proceedings of ICFP\u201901, pages 253\u2013264. ACM Press, September 2001.","DOI":"10.1145\/507663.507666"},{"key":"1_CR68","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/3-540-44622-2_21","volume-title":"Proceedings of CSL\u201900","author":"P. Hancock","year":"2000","unstructured":"P. Hancock and A. Setzer. Interactive programs in dependent type theory. In P. Clote and H. Schwichtenberg, editors, Proceedings of CSL\u201900, volume 1862 of Lecture Notes in Computer Science, pages 317\u2013331. Springer-Verlag, 2000."},{"issue":"1","key":"1_CR69","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143\u2013184, January 1993.","journal-title":"Journal of the ACM"},{"key":"1_CR70","doi-asserted-by":"crossref","unstructured":"R. Harper, J. C. Mitchell, and E. Moggi. Higher-order modules and the phase distinction. In Proceedings of POPL\u201990, pages 341\u2013354. ACM Press, 1990.","DOI":"10.1145\/96709.96744"},{"issue":"2","key":"1_CR71","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1145\/169701.169696","volume":"15","author":"R. Harper","year":"1993","unstructured":"R. Harper and J.C. Mitchell. On the type structure of Standard ML. ACM Transactions on Programming Languages and Systems, 15(2):211\u2013252, April 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR72","doi-asserted-by":"crossref","unstructured":"R. Hinze. A new approach to generic functional programming. In Proceedings of POPL\u201900, pages 119\u2013132. ACM Press, 2000.","DOI":"10.1145\/325694.325709"},{"key":"1_CR73","unstructured":"J. G. Hook and D. J. Howe. Impredicative strong existential equivalent to type:type. Technical Report TR86-760, Cornell University, Computer Science Department, June 1986."},{"key":"1_CR74","doi-asserted-by":"crossref","unstructured":"J. Hughes, L. Pareto, and A. Sabry. Proving the correctness of reactive systems using sized types. In Proceedings of POPL\u201996, pages 410\u2013423. ACM Press, 1996.","DOI":"10.1145\/237721.240882"},{"key":"1_CR75","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1007\/BFb0014058","volume-title":"Proceedings of TLCA\u2019 95","author":"A. Hurkens","year":"1995","unstructured":"A. Hurkens. A Simplification of Girard\u2019s Paradox. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of TLCA\u2019 95, volume 902 of Lecture Notes in Computer Science, pages 266\u2013278. Springer-Verlag, 1995."},{"key":"1_CR76","doi-asserted-by":"crossref","unstructured":"P. Jansson and J. Jeuring. PolyP\u2014a polytypic programming language extension. In Proceedings of POPL\u201997, pages 470\u2013482. ACM Press, 1997.","DOI":"10.1145\/263699.263763"},{"key":"1_CR77","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/3-540-45931-6_14","volume-title":"Proceedings of FOSSACS 2002","author":"S. Jha","year":"2002","unstructured":"S. Jha, J. Palsberg, and T. Zhao. Efficient type matching. In M. Nielsen and U. Engberg, editors, Proceedings of FOSSACS 2002, volume 2303 of Lecture Notes in Computer Science, pages 187\u2013204. Springer-Verlag, 2002."},{"key":"1_CR78","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1007\/3-540-46425-5_15","volume-title":"Proceedings of ESOP\u201900","author":"M. P. Jones","year":"2000","unstructured":"M. P. Jones. Type classes with functional dependencies. In G. Smolka, editor, Proceedings of ESOP\u201900, volume 1782 of Lecture Notes in Computer Science, pages 230\u2013244, 2000."},{"issue":"2","key":"1_CR79","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1016\/S0304-3975(96)00161-2","volume":"173","author":"J.-P. Jouannaud","year":"1997","unstructured":"J.-P. Jouannaud and M. Okada. Abstract data type systems. Theoretical Computer Science, 173(2):349\u2013391, February 1997.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"1_CR80","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1017\/S0960129500000657","volume":"5","author":"D. Kozen","year":"1995","unstructured":"D. Kozen, J. Palsberg, and M. Schwartzback. Efficient recursive subtyping. Mathematical Structures in Computer Science, 5(1):113\u2013125, March 1995.","journal-title":"Mathematical Structures in Computer Science"},{"key":"1_CR81","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):278\u2013346, February\/March 1988.","DOI":"10.1016\/0890-5401(88)90011-9"},{"key":"1_CR82","doi-asserted-by":"crossref","unstructured":"C.-S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. In Proceedings of POPL\u201901, pages 81\u201392. ACM Press, 2001.","DOI":"10.1145\/373243.360210"},{"issue":"3","key":"1_CR83","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1017\/S0956796800003683","volume":"10","author":"X. Leroy","year":"2000","unstructured":"X. Leroy. A modular module system. Journal of Functional Programming, 10(3):269\u2013303, May 2000.","journal-title":"Journal of Functional Programming"},{"issue":"2","key":"1_CR84","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1017\/S0960129500001298","volume":"1","author":"G. Longo","year":"1991","unstructured":"G. Longo and E. Moggi. Constructive natural deduction and its \u2018w-set\u2019 interpretation. Mathematical Structures in Computer Science, 1(2):215\u2013254, July 1991.","journal-title":"Mathematical Structures in Computer Science"},{"key":"1_CR85","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"},{"issue":"1","key":"1_CR86","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1093\/logcom\/9.1.105","volume":"9","author":"Z. Luo","year":"1999","unstructured":"Z. Luo. Coercive subtyping. Journal of Logic and Computation, 9(1):105\u2013130, February 1999.","journal-title":"Journal of Logic and Computation"},{"key":"1_CR87","doi-asserted-by":"crossref","unstructured":"D. MacQueen. Using dependent types to express modular structure. In Proceedings of POPL\u201986, pages 277\u2013286. ACM Press, 1986.","DOI":"10.1145\/512644.512670"},{"key":"1_CR88","unstructured":"L. Magnusson. The implementation of ALF: a proof editor based on Martin-L\u00f6f\u2019s monomorphic type theory with explicit substitution. PhD thesis, Department of Computer Science, Chalmers University, 1994."},{"key":"1_CR89","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/S0049-237X(08)70847-4","volume-title":"Proceedings 2nd Scandinavian Logic Symposium","author":"P. Martin-L\u00f6f","year":"1971","unstructured":"P. Martin-L\u00f6f. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In J. E. Fenstad, editor, Proceedings 2nd Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics, pages 179\u2013216. North-Holland, Amsterdam, 1971."},{"key":"1_CR90","unstructured":"P. Martin-L\u00f6f. A theory of types. Technical Report, Stockholm University, February 1971."},{"key":"1_CR91","unstructured":"P. Martin-L\u00f6f. An intuitionistic theory of types. Unpublished Manuscript, 1972."},{"key":"1_CR92","unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory, volume 1 of Studies in Proof Theory. Bibliopolis, Naples, 1984."},{"key":"1_CR93","unstructured":"P. Martin-L\u00f6f. Constructive mathematics and computer programming. In C. A. R. Hoare and J. C. Shepherdson, editors, Mathematical Logic and Programming Languages, pages 167\u2013184. Prentice-Hall, 1985."},{"key":"1_CR94","unstructured":"C. McBride. Dependently typed functional programs and their proofs. PhD thesis, University of Edinburgh, 2000."},{"key":"1_CR95","doi-asserted-by":"crossref","unstructured":"C. McBride. Faking It (Simulating Dependent Types in Haskell). Journal of Functional Programming, 2002. To appear.","DOI":"10.1017\/S0956796802004355"},{"key":"1_CR96","unstructured":"N. P. Mendler. Inductive types and type constraints in second-order lambda calculus. In Proceedings of LICS\u201987, pages 30\u201336. IEEE Computer Society Press, 1987."},{"issue":"1\u20132","key":"1_CR97","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0168-0072(91)90069-X","volume":"51","author":"N. P. Mendler","year":"1991","unstructured":"N. P. Mendler. Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic, 51(1\u20132):159\u2013172, March 1991.","journal-title":"Annals of Pure and Applied Logic"},{"key":"1_CR98","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348\u2013375, 1978.","journal-title":"Journal of Computer and System Sciences"},{"key":"1_CR99","unstructured":"R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. The MIT Press, 1991."},{"key":"1_CR100","doi-asserted-by":"crossref","unstructured":"R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). The MIT Press, 1997.","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"1_CR101","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"344","DOI":"10.1007\/3-540-45413-6_27","volume-title":"Proceedings of TLCA\u201901","author":"A. Miquel","year":"2001","unstructured":"A. Miquel. The implicit calculus of constructions. In S. Abramsky, editor, Proceedings of TLCA\u201901, volume 2044 of Lecture Notes in Computer Science, pages 344\u2013359. Springer-Verlag, 2001."},{"key":"1_CR102","unstructured":"A. Miquel. Le Calcul des Constructions implicite: syntaxe et s\u00e9mantique. PhD thesis, Universit\u00e9 Paris 11, 2001."},{"issue":"3","key":"1_CR103","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1145\/44501.45065","volume":"10","author":"J. C. Mitchell","year":"1988","unstructured":"J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. ACM Transactions on Programming Languages and Systems, 10(3):470\u2013502, July 1988.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR104","doi-asserted-by":"crossref","unstructured":"G. C. Necula. Proof-carrying code. In Proceedings of POPL\u201997, pages 106\u2013119. ACM Press, 1997.","DOI":"10.1145\/263699.263712"},{"key":"1_CR105","doi-asserted-by":"crossref","unstructured":"G. C. Necula and P. Lee. Efficient representation and validation of logical proofs. In Proceedings of LICS\u201998, pages 93\u2013104, 1998.","DOI":"10.1109\/LICS.1998.705646"},{"key":"1_CR106","unstructured":"R. Nederpelt, H. Geuvers, and R. de Vrijer, editors. Selected Papers on Automath, volume 133 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1994."},{"key":"1_CR107","doi-asserted-by":"crossref","unstructured":"M. Neubauer, P. Thiemann, M. Gasbichler, and M. Sperber. Functional logic overloading. In Proceedings of POPL\u201902, pages 233\u2013244. ACM Press, 2002.","DOI":"10.1145\/565816.503294"},{"issue":"3","key":"1_CR108","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1007\/BF01941137","volume":"28","author":"B. Nordstr\u00f6m","year":"1988","unstructured":"B. Nordstr\u00f6m. Terminating general recursion. BIT, 28(3):605\u2013619, 1988.","journal-title":"BIT"},{"key":"1_CR109","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J. Smith. Programming in Martin-L\u00f6f\u2019s Type Theory. An Introduction. Number 7 in International Series of Monographs on Computer Science. Oxford University Press, 1990."},{"key":"1_CR110","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1006\/inco.2001.3090","volume":"171","author":"J. Palsberg","year":"2001","unstructured":"J. Palsberg and T. Zhao. Efficient and flexible matching of recursive types. Information and Computation, 171:364\u2013387, November 2001.","journal-title":"Information and Computation"},{"key":"1_CR111","unstructured":"L. Pareto. Types for crash prevention. PhD thesis, Department of Computing, Chalmers Tekniska H\u00f6gskola, 2000."},{"key":"1_CR112","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"Proceedings of TLCA\u2019 93","author":"C. Paulin-Mohring","year":"1993","unstructured":"C. Paulin-Mohring. Inductive definitions in the system Coq. Rules and properties. In M. Bezem and J.F. Groote, editors, Proceedings of TLCA\u2019 93, volume 664 of Lecture Notes in Computer Science, pages 328\u2013345. Springer-Verlag, 1993."},{"key":"1_CR113","unstructured":"C. Paulin-Mohring. D\u00e9finitions Inductives en Theorie des Types d\u2019Ordre Superieur. Habilitation \u00e0 diriger les recherches, Universit\u00e9 Claude Bernard Lyon I, 1996."},{"key":"1_CR114","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. ML for the Working Programmer. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511811326"},{"key":"1_CR115","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"61\/2","author":"L.C. Paulson","year":"1998","unstructured":"L.C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6(1\/2):85\u2013128, 1998.","journal-title":"Journal of Computer Security"},{"key":"1_CR116","unstructured":"S. Peyton Jones and E. Meijer. Henk: a typed intermediate language. Appeared as Technical Report BCCS-97-03, Computer Science Department, Boston College, 1997."},{"key":"1_CR117","unstructured":"H. Pfeifer and H. Rue\u00df. Polytypic abstraction in type theory. In R. Backhouse and T. Sheard, editors, Informal Proceedings of WGP\u201998. Department of Computing Science, Chalmers University, June 1998."},{"key":"1_CR118","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/3-540-48256-3_5","volume-title":"Proceedings of TPHOLs\u201999","author":"H. Pfeifer","year":"1999","unstructured":"H. Pfeifer and H. Rue\u00df. Polytypic proof construction. In Y. Bertot, G. Dowek, H. Hirshowitz, C. Paulin, and L. Th\u00e9ry, editors, Proceedings of TPHOLs\u201999, volume 1690 of Lecture Notes in Computer Science, pages 55\u201372. Springer-Verlag, 1999."},{"key":"1_CR119","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Elf: a meta-language for deductive systems. In A. Bundy, editor, Proceedings of CADE-12, volume 814 of Lecture Notes in Artificial Intelligence, pages 811\u2013815. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_66"},{"key":"1_CR120","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Logical Frameworks. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 17, pages 1063\u20131147. Elsevier Publishing, 2001.","DOI":"10.1016\/B978-044450813-3\/50019-9"},{"key":"1_CR121","series-title":"Lect Notes Comput Sci","first-page":"209","volume-title":"Proceedings of MFPS\u201989","author":"F. Pfenning","year":"1989","unstructured":"F. Pfenning and C. Paulin. Inductively Defined Types in the Calculus of Constructions. In M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Proceedings of MFPS\u201989, volume 442 of Lecture Notes in Computer Science, pages 209\u2013228. Springer-Verlag, 1989."},{"key":"1_CR122","unstructured":"R. Pollack. Typechecking in pure type systems. In B. Nordstr\u00f6m, editor, Informal proceedings of Logical Frameworks\u201992, pages 271\u2013288, 1992."},{"key":"1_CR123","unstructured":"R. Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1994."},{"key":"1_CR124","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"462","DOI":"10.1007\/3-540-44659-1_29","volume-title":"Proceedings of TPHOLs\u201900","author":"R. Pollack","year":"2000","unstructured":"R. Pollack. Dependently typed records for representing mathematical structures. In M. Aagard and J. Harrison, editors, Proceedings of TPHOLs\u201900, volume 1869 of Lecture Notes in Computer Science, pages 462\u2013479. Springer-Verlag, 2000."},{"key":"1_CR125","unstructured":"M. B. Reinhold. Typechecking is undecidable\u2019 TYPE\u2019 is a type. Technical Report MIT\/LCS\/TR-458, Massachusetts Institute of Technology, December 1989."},{"key":"1_CR126","unstructured":"D. R\u00e9my. Using, Understanding, and Unraveling the OCaml Language\u2014From Practice to Theory and vice versa. This volume."},{"key":"1_CR127","unstructured":"J. W. Roorda. Pure Type Systems for Functional Programming. Master\u2019s thesis, Department of Computer Science, University of Utrecht, 2000."},{"key":"1_CR128","unstructured":"C. Russo. Types For Modules. PhD thesis, University of Edinburgh, 1998."},{"key":"1_CR129","doi-asserted-by":"crossref","unstructured":"A. Salvesen and J. Smith. The Strength of the Subset Type in Martin-L\u00f6f\u2019s Type Theory. In Proceedings of LICS\u201988, pages 384\u2013391. IEEE Computer Society Press, 1988.","DOI":"10.1109\/LICS.1988.5135"},{"key":"1_CR130","unstructured":"D. Scott. Constructive validity. In M. Laudet, D. Lacombe, L. Nolin, and M. Sch\u00fctzenberger, editors, Proceedings of Symposium on Automatic Demonstration, volume 125 of Lecture Notes in Mathematics, pages 237\u2013275. Springer-Verlag, 1970."},{"key":"1_CR131","doi-asserted-by":"crossref","unstructured":"P. Severi. Type Inference for Pure Type Systems. Information and Computation, 143(1):1\u201323, May 1998.","DOI":"10.1006\/inco.1998.2708"},{"key":"1_CR132","doi-asserted-by":"crossref","unstructured":"Z. Shao, B. Saha, V. Trifonov, and N. Papaspyrou. A type system for certified binaries. In Proceedings of POPL\u201902, pages 217\u2013232. ACM Press, 2002.","DOI":"10.1145\/565816.503293"},{"key":"1_CR133","unstructured":"M. H. S\u00f8rensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Available as DIKU Rapport 98\/14, 1998."},{"key":"1_CR134","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/3-540-61780-9_74","volume-title":"Proceedings of TYPES\u201995","author":"M. Stefanova","year":"1996","unstructured":"M. Stefanova and H. Geuvers. A simple set-theoretic semantics for the Calculus of Constructions. In S. Berardi and M. Coppo, editors, Proceedings of TYPES\u201995, volume 1158 of Lecture Notes in Computer Science, pages 249\u2013264. Springer-Verlag, 1996."},{"key":"1_CR135","doi-asserted-by":"crossref","unstructured":"C. A. Stone and R. Harper. Deciding Type Equivalence with Singleton Kinds. In Proceedings of POPL\u201900, pages 214\u2013227. ACM Press, 2000.","DOI":"10.1145\/325694.325724"},{"key":"1_CR136","unstructured":"M. D. G. Swaen. Weak and strong sum elimination in intuitionistic type theory. PhD thesis, Faculty of Mathematics and Computer Science, University of Amsterdam, 1989."},{"key":"1_CR137","doi-asserted-by":"crossref","unstructured":"W. W. Tait. Constructive reasoning. In Proceedings of the Third International Congress in Logic, Methodology and Philosophy of Science, pages 185\u2013199. North-Holland Publishing, 1968.","DOI":"10.1016\/S0049-237X(08)71195-9"},{"key":"1_CR138","unstructured":"S. Thompson. Haskell. The Craft of Functional Programming. Addison-Wesley, 1996."},{"key":"1_CR139","doi-asserted-by":"crossref","unstructured":"D. Walker. A Type System for Expressive Security Policies. In Proceedings of POPL\u201900, pages 254\u2013267. ACM Press, 2000.","DOI":"10.1145\/325694.325728"},{"key":"1_CR140","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"530","DOI":"10.1007\/BFb0014566","volume-title":"Proceedings of TACS\u201997","author":"B. Werner","year":"1997","unstructured":"B. Werner. Sets in Types, Types in Sets. In M. Abadi and T. Ito, editors, Proceedings of TACS\u201997, volume 1281 of Lecture Notes in Computer Science, pages 530\u2013546. Springer-Verlag, 1997."},{"key":"1_CR141","unstructured":"H. Xi. Dependent types in practical programming. PhD thesis, Department of Computer Science, Carnegie-Mellon University, 1998."},{"key":"1_CR142","doi-asserted-by":"crossref","unstructured":"H. Xi. Dead Code Elimination through Dependent Types. In G. Gupta, editor, Proceedings of PADL\u201999, volume 1551, pages 228\u2013242. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-49201-1_16"},{"key":"1_CR143","doi-asserted-by":"crossref","unstructured":"H. Xi and R. Harper. A Dependently Typed Assembly Language. In Proceedings of ICFP\u201901, pages 169\u2013180. ACM Press, 2001.","DOI":"10.1145\/507656.507657"},{"key":"1_CR144","doi-asserted-by":"crossref","unstructured":"H. Xi and F. Pfenning. Eliminating array bound checking through dependent types. In Proceedings of PLDI\u201998, pages 249\u2013257. ACM Press, 1998.","DOI":"10.1145\/277652.277732"},{"key":"1_CR145","doi-asserted-by":"crossref","unstructured":"H. Xi and F. Pfenning. Dependent types in practical programming. In Proceedings of POPL\u201999, pages 214\u2013227. ACM Press, 1999.","DOI":"10.1145\/292540.292560"}],"container-title":["Lecture Notes in Computer Science","Applied Semantics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45699-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T14:45:34Z","timestamp":1737038734000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45699-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440444","9783540456995"],"references-count":145,"URL":"https:\/\/doi.org\/10.1007\/3-540-45699-6_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}