{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T05:44:22Z","timestamp":1742967862880,"version":"3.40.3"},"publisher-location":"Cham","reference-count":111,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031345173"},{"type":"electronic","value":"9783031345180"}],"license":[{"start":{"date-parts":[[2023,10,11]],"date-time":"2023-10-11T00:00:00Z","timestamp":1696982400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,10,11]],"date-time":"2023-10-11T00:00:00Z","timestamp":1696982400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-34518-0_8","type":"book-chapter","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:01:57Z","timestamp":1714410117000},"page":"175-202","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Some Remarks About Dependent Type Theory"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,10,11]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Peter Aczel. On Relating Type Theories and Set Theories. In T. Altenkirch, B. Reus, and W. Naraschewski, editors, Types for Proofs and Programs, pages 33\u201346. Springer, 1998.","DOI":"10.1007\/3-540-48167-2_1"},{"issue":"4","key":"8_CR2","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1017\/S0960129501003309","volume":"11","author":"Peter Aczel","year":"2001","unstructured":"Peter Aczel. The Russell-Prawitz modality. Math. Struct. Comput. Sci., 11(4):541\u2013554, 2001.","journal-title":"Math. Struct. Comput. Sci."},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"M. Algehed and J.-Ph. Bernardy. Simple noninterference from parametricity. Proc. ACM Program. Lang., 3(ICFP):89:1\u201389:22, 2019.","DOI":"10.1145\/3341693"},{"key":"8_CR4","unstructured":"L. Augustsson, Th. Coquand, and B. Nordstr\u00f6m. Another logical framework. In Annual Workshop on Logical Frameworks, 1990, 1990."},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"S. Awodey, J. Frey, and S. Speight. Impredicative encodings of (higher) inductive types. In Anuj Dawar and Erich Gr\u00e4del, editors, Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 76\u201385. ACM, 2018.","DOI":"10.1145\/3209108.3209130"},{"issue":"2","key":"8_CR6","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"Henk Barendregt","year":"1991","unstructured":"Henk Barendregt. Introduction to Generalized Type Systems. J. Funct. Program., 1(2):125\u2013154, 1991.","journal-title":"J. Funct. Program."},{"issue":"2","key":"8_CR7","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1017\/S0956796803004726","volume":"16","author":"G Barthe","year":"2006","unstructured":"G. Barthe and Th. Coquand. Remarks on the equational theory of non-normalizing pure type systems. J. Funct. Program., 16(2):137\u2013155, 2006.","journal-title":"J. Funct. Program."},{"key":"8_CR8","unstructured":"S. Berardi. Type Dependence and Constructive Mathematics. PhD thesis, University of Torino, 1989. PhD thesis."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"J.-Ph. Bernardy, P. Jansson, and R. Paterson. Parametricity and dependent types. In Paul Hudak and Stephanie Weirich, editors, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 345\u2013356. ACM, 2010.","DOI":"10.1145\/1863543.1863592"},{"key":"8_CR10","volume-title":"Foundations of Constructive Analysis","author":"Errett Bishop","year":"1967","unstructured":"Errett Bishop. Foundations of Constructive Analysis. McGraw-Hill, New York, 1967."},{"key":"8_CR11","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0304-3975(85)90135-5","volume":"39","author":"Corrado B\u00f6hm","year":"1985","unstructured":"Corrado B\u00f6hm and Alessandro Berarducci. Automatic synthesis of typed lambda-programs on term algebras. Theor. Comput. Sci., 39:135\u2013154, 1985.","journal-title":"Theor. Comput. Sci."},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Sylvie Boldo and Guillaume Melquiond. Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system. Amsterdam: Elsevier\/ISTE Press, 2017.","DOI":"10.1016\/B978-1-78548-112-3.50002-3"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"K. Buzzard, J. Commelin, and P. Massot. Formalising perfectoid spaces. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 299\u2013312. ACM, 2020.","DOI":"10.1145\/3372885.3373830"},{"issue":"2","key":"8_CR14","doi-asserted-by":"publisher","first-page":"346","DOI":"10.2307\/1968337","volume":"33","author":"Alonzo Church","year":"1932","unstructured":"Alonzo Church. A set of postulates for the foundation of logic. Ann. of Math. (2), 33(2):346\u2013366, 1932.","journal-title":"Ann. of Math. (2)"},{"issue":"4","key":"8_CR15","doi-asserted-by":"publisher","first-page":"839","DOI":"10.2307\/1968702","volume":"34","author":"Alonzo Church","year":"1933","unstructured":"Alonzo Church. A set of postulates for the foundation of logic. Ann. of Math. (2), 34(4):839\u2013864, 1933.","journal-title":"Ann. of Math. (2)"},{"key":"8_CR16","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"Alonzo Church","year":"1940","unstructured":"Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56\u201368, 1940.","journal-title":"Journal of Symbolic Logic"},{"key":"8_CR17","volume-title":"The calculi of Lambda-Conversion, volume 6","author":"Alonzo Church","year":"1941","unstructured":"Alonzo Church. The calculi of Lambda-Conversion, volume 6. Princeton University Press, Princeton, NJ, 1941."},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Jesper Cockx, Dominique Devriese, and Frank Piessens. Pattern matching without K. In Johan Jeuring and Manuel M. T. Chakravarty, editors, Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014, pages 257\u2013268. ACM, 2014.","DOI":"10.1145\/2628136.2628139"},{"key":"8_CR19","unstructured":"Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, Todd B. Knoblock, N. P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. Implementing mathematics with the Nuprl proof development system. Prentice Hall, 1986."},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Robert L. Constable and N. P. Mendler. Recursive definitions in type theory. In Rohit Parikh, editor, Logics of Programs, Conference, Brooklyn College, New York, NY, USA, June 17-19, 1985, Proceedings, volume 193 of Lecture Notes in Computer Science, pages 61\u201378. Springer, 1985.","DOI":"10.1007\/3-540-15648-8_5"},{"key":"8_CR21","unstructured":"Th. Coquand. Une th\u00e9orie des constructions. Phd thesis, Universit\u00e9 Paris VII, 1985."},{"key":"8_CR22","unstructured":"Th. Coquand. An Analysis of Girard\u2019s Paradox. In Proceedings of the Symposium on Logic in Computer Science (LICS \u201986), Cambridge, Massachusetts, USA, June 16-18, 1986, pages 227\u2013236. IEEE Computer Society, 1986."},{"key":"8_CR23","unstructured":"Th. Coquand. Pattern matching with dependent types. In Annual Workshop on Logical Frameworks, 1992, 1992."},{"issue":"1","key":"8_CR24","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/BF01995104","volume":"32","author":"Th Coquand","year":"1992","unstructured":"Th. Coquand. The Paradox of Trees in Type Theory. BIT, 32(1):10\u201314, 1992.","journal-title":"BIT"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Th. Coquand. A new paradox in type theory. In Logic, methodology and philosophy of science IX. Proceedings of the ninth international congress of logic, methodology and philosophy of science, Uppsala, Sweden, August 7-14, 1991, pages 555\u2013570. Amsterdam: North-Holland, 1994.","DOI":"10.1016\/S0049-237X(06)80062-5"},{"key":"8_CR26","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1016\/j.tcs.2019.01.015","volume":"777","author":"Th Coquand","year":"2019","unstructured":"Th. Coquand. Canonicity and normalization for dependent type theory. Theor. Comput. Sci., 777:184\u2013191, 2019.","journal-title":"Theor. Comput. Sci."},{"key":"8_CR27","unstructured":"Th. Coquand. Reduction free normalisation for a proof irrelevant type of propositions. CoRR, abs\/2103.04287, 2021."},{"issue":"1","key":"8_CR28","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1017\/S0956796800000952","volume":"4","author":"Th Coquand","year":"1994","unstructured":"Th. Coquand and H. Herbelin. A-translation and looping combinators in pure type systems. J. Funct. Program., 4(1):77\u201388, 1994.","journal-title":"J. Funct. Program."},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Th. Coquand and G. P. Huet. Constructions: A higher order proof system for mechanizing mathematics. In Bruno Buchberger, editor, EUROCAL \u201985, European Conference on Computer Algebra, Linz, Austria, April 1-3, 1985, Proceedings Volume 1: Invited Lectures, volume 203 of Lecture Notes in Computer Science, pages 151\u2013184. Springer, 1985.","DOI":"10.1007\/3-540-15983-5_13"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Th. Coquand and G\u00e9rard P. Huet. The Calculus of Constructions. Inf. Comput., 76:95\u2013120, 1988.","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Th. Coquand and Ch. Paulin. Inductively defined types. In Per Martin-L\u00f6f and Grigori Mints, editors, COLOG-88, pages 50\u201366, Berlin, Heidelberg, 1990. Springer Berlin Heidelberg.","DOI":"10.1007\/3-540-52335-9_47"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"N. G. de Bruijn. The mathematical language AUTOMATH, its usage, and some of its extensions. Sympos. Automatic Demonstrat., Versailles\/France, 1968, Lect. Notes Math. 125, 29-61 (1970)., 1970.","DOI":"10.1007\/BFb0060623"},{"key":"8_CR33","volume-title":"Automath a language for mathematics. Seminaire de mathematiques superieures - ete 1971. No. 52","author":"N G de Bruijn","year":"1973","unstructured":"N. G. de Bruijn. Automath a language for mathematics. Seminaire de mathematiques superieures - ete 1971. No. 52. Montreal: Les Presses de l\u2019Universite de Montreal, 1973."},{"key":"8_CR34","unstructured":"N. G. de Bruijn. A survey of the project Automath. In To H. B. Curry: Essays on combinatory logic, lambda calculus and formalism, Academic Press, 606 p., Seldin, J. P. and Hindley, J. R, eds., 1980."},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Th. Ehrhard. A categorical semantics of constructions. In Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS \u201988), Edinburgh, Scotland, UK, July 5-8, 1988, pages 264\u2013273. IEEE Computer Society, 1988.","DOI":"10.1109\/LICS.1988.5125"},{"issue":"1","key":"8_CR36","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/322358.322370","volume":"30","author":"Steven Fortune","year":"1983","unstructured":"Steven Fortune, Daniel Leivant, and Michael O\u2019Donnell. The expressiveness of simple and second-order type structures. J. ACM, 30(1):151\u2013185, 1983.","journal-title":"J. ACM"},{"key":"8_CR37","unstructured":"G. Frege. Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Nebert, 1879."},{"issue":"6","key":"8_CR38","doi-asserted-by":"publisher","first-page":"771","DOI":"10.1017\/S0960129502003766","volume":"12","author":"Daniel Fridlender","year":"2002","unstructured":"Daniel Fridlender. A proof-irrelevant model of Martin-L\u00f6f\u2019s logical framework. Math. Struct. Comput. Sci., 12(6):771\u2013795, 2002.","journal-title":"Math. Struct. Comput. Sci."},{"key":"8_CR39","unstructured":"R. O. Gandy. On axiomatic systems in mathematics and theories in physics. PhD thesis, 1952. PhD thesis."},{"key":"8_CR40","unstructured":"Herman Geuvers. Conservativity between logics and typed lambda calculi. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, International Workshop TYPES\u201993, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers, volume 806 of Lecture Notes in Computer Science, pages 79\u2013107. Springer, 1993."},{"key":"8_CR41","doi-asserted-by":"crossref","unstructured":"Herman Geuvers. Induction is not derivable in second order dependent type theory. In Samson Abramsky, editor, Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Krakow, Poland, May 2-5, 2001, Proceedings, volume 2044 of Lecture Notes in Computer Science, pages 166\u2013181. Springer, 2001.","DOI":"10.1007\/3-540-45413-6_16"},{"key":"8_CR42","doi-asserted-by":"crossref","unstructured":"Herman Geuvers and Benjamin Werner. On the Church-Rosser Property for Expressive Type Systems and its Consequences for their Metatheoretic Study. In Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS \u201994), Paris, France, July 4-7, 1994, pages 320\u2013329. IEEE Computer Society, 1994.","DOI":"10.1109\/LICS.1994.316057"},{"key":"8_CR43","doi-asserted-by":"crossref","unstructured":"J.-Y. Girard. Une extension de l\u2019interpr\u00e9tation de G\u00f6del \u00e0 l\u2019analyse, et son application \u00e0 l\u2019\u00e9limination des coupures dans l\u2019analyse et la th\u00e9orie des types.(An extension of G\u00f6del\u2019s interpretation to analysis and its application to cut elimination in analysis and type theory). Proc. 2nd Scandinav. Logic Sympos. 1970, Studies Logic Foundations Math. 63, 63-92 (1971)., 1971.","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"8_CR44","unstructured":"J.-Y. Girard. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur, 1972. Th\u00e8se de Doctorat d\u2019Etat."},{"key":"8_CR45","doi-asserted-by":"crossref","unstructured":"J.-Y. Girard. The system $${\\mathcal F}$$ of variable types, fifteen years later. Theor. Comput. Sci., 45:159\u2013192, 1986.","DOI":"10.1016\/0304-3975(86)90044-7"},{"key":"8_CR46","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1111\/j.1746-8361.1958.tb01464.x","volume":"12","author":"Kurt G\u00f6del","year":"1958","unstructured":"Kurt G\u00f6del. \u00dcber eine bisher noch nicht ben\u00fctzte Erweiterung des finiten Standpunktes. Dialectica, 12:280\u2013287, 1958.","journal-title":"Dialectica"},{"key":"8_CR47","first-page":"1382","volume":"55","author":"G Gonthier","year":"2008","unstructured":"G. Gonthier. The Four-Color Theorem. Notices Amer. Math. Soc., 55:1382\u20131393, 2008.","journal-title":"Notices Amer. Math. Soc."},{"key":"8_CR48","doi-asserted-by":"crossref","unstructured":"G. Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, Fran\u00e7ois Garillot, St\u00e9phane Le Roux, Assia Mahboubi, Russell O\u2019Connor, Sidi Ould Biha, et al. A machine-checked proof of the odd order theorem. In International Conference on Interactive Theorem Proving, pages 163\u2013179. Springer, 2013.","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"8_CR49","doi-asserted-by":"crossref","unstructured":"Michael J. C. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF, volume 78 of Lecture Notes in Computer Science. Springer, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"8_CR50","unstructured":"Peter Hancock. Ordinals and Interactive Programs. PhD thesis, University of Edinburgh, 2000."},{"key":"8_CR51","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/BF01206605","volume":"95","author":"D Hilbert","year":"1926","unstructured":"D. Hilbert. \u00dcber das unendliche. Mathematische Annalen, 95:161\u2013190, 1926.","journal-title":"Mathematische Annalen"},{"key":"8_CR52","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/BF02940602","volume":"6","author":"D Hilbert","year":"1928","unstructured":"D. Hilbert. Die Grundlagen der Mathematik. Abhandlungen aus dem Seminar der Hamburgischen Universit\u00e4t, 6:65\u201385, 1928.","journal-title":"Abhandlungen aus dem Seminar der Hamburgischen Universit\u00e4t"},{"key":"8_CR53","unstructured":"William A. Howard. The formulae-as-types notion of construction. In J. Hindley and J. Seldin, editors, To H.B. Curry: Essays on Combinatory Logic,$$\\lambda $$-calculus and Formalism, pages 479\u2013490. Academic Press, 1980."},{"key":"8_CR54","unstructured":"D. J. Howe. The Computational Behaviour of Girard\u2019s Paradox. In Proceedings of the Symposium on Logic in Computer Science (LICS \u201987), Ithaca, New York, USA, June 22-25, 1987, pages 205\u2013214. IEEE Computer Society, 1987."},{"key":"8_CR55","unstructured":"G\u00e9rard P. Huet. A Mechanization of Type Theory. In Nils J. Nilsson, editor, Proceedings of the 3rd International Joint Conference on Artificial Intelligence. Stanford, CA, USA, August 20-23, 1973, pages 139\u2013146. William Kaufmann, 1973."},{"issue":"4","key":"8_CR56","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G\u00e9rard P Huet","year":"1980","unstructured":"G\u00e9rard P. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems: Abstract properties and applications to term rewriting systems. J. ACM, 27(4):797\u2013821, 1980.","journal-title":"J. ACM"},{"key":"8_CR57","doi-asserted-by":"crossref","unstructured":"A. J. C. Hurkens. A simplification of Girard\u2019s paradox. In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors, Typed Lambda Calculi and Applications, pages 266\u2013278, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg.","DOI":"10.1007\/BFb0014058"},{"key":"8_CR58","unstructured":"L. S. Jutting. The development of a text in AUT-QE. In P. Braffort et L. Michel, editor, Symposium d\u2019Orsday sur la manipulation des symboles et l\u2019utilisation d\u2019APL, 1973."},{"key":"8_CR59","doi-asserted-by":"crossref","unstructured":"G. Kreisel. Church\u2019s thesis: A kind of reducibility axiom for constructive mathematics. In Intuitionism and Proof Theory (Proc. Conf., Buffalo, N.Y., 1968), pages 121\u2013150. North-Holland, Amsterdam, 1970.","DOI":"10.1016\/S0049-237X(08)70746-8"},{"key":"8_CR60","unstructured":"J.-L. Krivine. Un algorithme non typable dans le syst\u00e8me F. (An algorithm not typable in the system F). C. R. Acad. Sci., Paris, S\u00e9r. I, 304:123\u2013126, 1987."},{"key":"8_CR61","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BF01110627","volume":"103","author":"J Lambek","year":"1968","unstructured":"J. Lambek. A fixpoint theorem for complete categories. Math. Z., 103:151\u2013161, 1968.","journal-title":"Math. Z."},{"issue":"2","key":"8_CR62","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/363744.363749","volume":"8","author":"Peter J Landin","year":"1965","unstructured":"Peter J. Landin. Correspondence between ALGOL 60 and Church\u2019s Lambda-notation: part I. Commun. ACM, 8(2):89\u2013101, 1965.","journal-title":"Commun. ACM"},{"key":"8_CR63","unstructured":"The Caml Language. A History of Caml, 2005."},{"key":"8_CR64","doi-asserted-by":"crossref","unstructured":"X. Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, pages 42\u201354, 2006.","DOI":"10.1145\/1111037.1111042"},{"key":"8_CR65","doi-asserted-by":"crossref","unstructured":"Paul Lorenzen. Einf\u00fchrung in die operative Logik und Mathematik, volume 78 of Grundlehren Math. Wiss. Springer, 1955.","DOI":"10.1007\/978-3-662-01539-1"},{"key":"8_CR66","unstructured":"P. Martin-L\u00f6f. A Theory of Types. Rep., Dep. Math., Univ. Stockh., 1971."},{"key":"8_CR67","unstructured":"P. Martin-L\u00f6f. On the strength of intuitionistic reasoning. Rep., Dep. Math., Univ. Stockh., 1971."},{"key":"8_CR68","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f. An intuitionistic theory of types: Predicative part. In H. E. Rose and J. Sheperdson, editors, Studies in Logic and the Foundations of Mathematics, volume 80, pages 73\u2013118. Elsevier, 1975.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"8_CR69","unstructured":"P. Martin-L\u00f6f. Syntax and Semantics of Mathematical Language. Notes written by P. Hancock, Rep., Dep. Math., Univ. Stockh., 1975."},{"key":"8_CR70","unstructured":"P. Martin-L\u00f6f. Constructive mathematics and computer programming. Rep., Dep. Math., Univ. Stockh., 1979."},{"key":"8_CR71","doi-asserted-by":"crossref","unstructured":"Per Martin-L\u00f6f. Hauptsatz for the theory of species. Proc. 2nd Scandinav. Logic Sympos. 1970, Studies Logic Foundations Math. 63, 217-233, 1971.","DOI":"10.1016\/S0049-237X(08)70848-6"},{"key":"8_CR72","unstructured":"Per Martin-L\u00f6f. Intuitionistic Type Theory, volume 1 of Studies in Proof Theory. Lecture Notes. Bibliopolis, Naples, 1984. Notes by Giovanni Sambin."},{"key":"8_CR73","volume-title":"A construction of the provable wellorderings of the theory of species. In Logic, meaning and computation. Essays in memory of Alonzo Church, pages 343\u2013351","author":"Per Martin-L\u00f6f","year":"2001","unstructured":"Per Martin-L\u00f6f. A construction of the provable wellorderings of the theory of species. In Logic, meaning and computation. Essays in memory of Alonzo Church, pages 343\u2013351. Dordrecht: Kluwer Academic Publishers, 2001."},{"key":"8_CR74","doi-asserted-by":"crossref","unstructured":"A. R. Meyer and M. B. Reinhold. \u201cType\u201d Is Not A Type. In Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, USA, January 1986, pages 287\u2013295. ACM Press, 1986.","DOI":"10.1145\/512644.512671"},{"key":"8_CR75","unstructured":"A. Miquel. Le Calcul des Constructions Implicite: Syntaxe et S\u00e9mantique. PhD thesis, Universit\u00e9 Paris VII, 2001. PhD thesis."},{"key":"8_CR76","doi-asserted-by":"crossref","unstructured":"A. Miquel. Lamda-Z: Zermelo\u2019s Set Theory as a PTS with 4 Sorts. In Jean-Christophe Filli\u00e2tre, Christine Paulin-Mohring, and Benjamin Werner, editors, Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, volume 3839 of Lecture Notes in Computer Science, pages 232\u2013251. Springer, 2004.","DOI":"10.1007\/11617990_15"},{"key":"8_CR77","doi-asserted-by":"crossref","unstructured":"J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. In Mary S. Van Deusen, Zvi Galil, and Brian K. Reid, editors, Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, New Orleans, Louisiana, USA, January 1985, pages 37\u201351. ACM Press, 1985.","DOI":"10.1145\/318593.318606"},{"key":"8_CR78","doi-asserted-by":"crossref","unstructured":"Rob Nederpelt and Herman Geuvers. Type Theory and Formal Proof: An Introduction. Cambridge University Press, USA, 1st edition, 2014.","DOI":"10.1017\/CBO9781139567725"},{"issue":"3","key":"8_CR79","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":"8_CR80","unstructured":"B. Nordstr\u00f6m and K. Petersson. Types and specifications. In R. E. A. Mason, editor, Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983, pages 915\u2013920. North-Holland\/IFIP, 1983."},{"key":"8_CR81","unstructured":"Christine Paulin-Mohring. Algorithm development in the calculus of constructions. In Proceedings of the First Annual IEEE Symposium on Logic in Computer Science, pages 84\u201391. IEEE Computer Society, 1986."},{"key":"8_CR82","doi-asserted-by":"crossref","unstructured":"P.-M. P\u00e9drot and N. Tabareau. Failure is not an option - an exceptional type theory. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, pages 245\u2013271, 2018.","DOI":"10.1007\/978-3-319-89884-1_9"},{"key":"8_CR83","doi-asserted-by":"crossref","unstructured":"F. Pfenning and Ch. Paulin-Mohring. Inductively defined types in the calculus of constructions. In Mathematical Foundations of Programming Semantics, 5th International Conference, Tulane University, New Orleans, Louisiana, USA, March 29\u2013April 1, 1989, Proceedings, volume 442 of Lecture Notes in Computer Science, pages 209\u2013228. Springer, 1989.","DOI":"10.1007\/BFb0040259"},{"key":"8_CR84","doi-asserted-by":"crossref","unstructured":"Frank Pfenning. Unification and anti-unification in the calculus of constructions. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS \u201991), Amsterdam, The Netherlands, July 15-18, 1991, pages 74\u201385. IEEE Computer Society, 1991.","DOI":"10.1109\/LICS.1991.151632"},{"key":"8_CR85","first-page":"815","volume":"13","author":"Henri Poincar\u00e9","year":"1905","unstructured":"Henri Poincar\u00e9. Les math\u00e9matiques et la logique. Revue de m\u00e9taphysique et de morale, 13:815\u2013835, 1905.","journal-title":"Revue de m\u00e9taphysique et de morale"},{"issue":"24","key":"8_CR86","first-page":"1","volume":"12","author":"Henri Poincar\u00e9","year":"1912","unstructured":"Henri Poincar\u00e9. La logique de l\u2019infini. Scientia (Rivista di Scienza), 12(24):1\u201311, 1912.","journal-title":"Scientia (Rivista di Scienza)"},{"key":"8_CR87","volume-title":"Epistemology versus Ontology. Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-L\u00f6f","author":"Michael Rathjen","year":"2012","unstructured":"Michael Rathjen. Constructive Zermelo\u2013Fraenkel Set Theory, Power Set, and the Calculus of Constructions. In P. Dybjer, S. Lindstr\u00f6m, E. Palmgren, and B. G. Sundholm, editors, Epistemology versus Ontology. Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-L\u00f6f. Springer Netherlands, Dordrecht, 2012."},{"key":"8_CR88","unstructured":"J. C. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983, pages 513\u2013523. North-Holland\/IFIP, 1983."},{"key":"8_CR89","unstructured":"John C. Reynolds. Towards a theory of type structure. In Bernard Robinet, editor, Programming Symposium, Proceedings Colloque sur la Programmation, Paris, France, April 9-11, 1974, volume 19 of Lecture Notes in Computer Science, pages 408\u2013423. Springer, 1974."},{"key":"8_CR90","doi-asserted-by":"crossref","unstructured":"John C. Reynolds. Polymorphism is not set-theoretic. In Gilles Kahn, David B. MacQueen, and Gordon D. Plotkin, editors, Semantics of Data Types, International Symposium, Sophia-Antipolis, France, June 27-29, 1984, Proceedings, volume 173 of Lecture Notes in Computer Science, pages 145\u2013156. Springer, 1984.","DOI":"10.1007\/3-540-13346-1_7"},{"issue":"1","key":"8_CR91","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1993.1037","volume":"105","author":"John C Reynolds","year":"1993","unstructured":"John C. Reynolds and Gordon D. Plotkin. On functors expressible in the polymorphic typed lambda calculus. Inf. Comput., 105(1):1\u201329, 1993.","journal-title":"Inf. Comput."},{"key":"8_CR92","unstructured":"Bertrand Russell. The Principles of Mathematics. W. W. Norton & Company, Berlin, 2 edition, 1903."},{"issue":"3","key":"8_CR93","doi-asserted-by":"publisher","first-page":"222","DOI":"10.2307\/2369948","volume":"30","author":"Bertrand Russell","year":"1908","unstructured":"Bertrand Russell. Mathematical logic as based on the theory of types. American Journal of Mathematics, 30(3):222\u2013262, 1908.","journal-title":"American Journal of Mathematics"},{"key":"8_CR94","first-page":"488","volume":"39","author":"Bertrand Russell","year":"1911","unstructured":"Bertrand Russell. Sur les axiomes de l\u2019infini et du transfini. Bulletin de la Socit\u0301\u00e9 Math\u00e9matique de France, 39:488\u2013501, 1911.","journal-title":"Bulletin de la Socit\u0301\u00e9 Math\u00e9matique de France"},{"key":"8_CR95","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BFb0060636","volume-title":"Symposium on Automatic Demonstration","author":"DS Scott","year":"1970","unstructured":"D.S. Scott. Constructive validity. In M. Laudet, D. Lacombe, L. Nolin, and M. Sch\u00fctzenberger, editors, Symposium on Automatic Demonstration, pages 237\u2013275. Springer Berlin Heidelberg, 1970."},{"key":"8_CR96","doi-asserted-by":"crossref","unstructured":"Morten Heine S\u00f8rensen and Pawe\u0142 Urzyczyn. Lectures on the Curry-Howard isomorphism, volume 149. Amsterdam: Elsevier, 2006.","DOI":"10.1016\/S0049-237X(06)80005-4"},{"key":"8_CR97","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0433-6","volume-title":"Semantics of Type Theory","author":"Thomas Streicher","year":"1991","unstructured":"Thomas Streicher. Semantics of Type Theory. Progress in Theoretical Computer Science. Birkhaeuser Boston, Inc., 1991."},{"key":"8_CR98","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796817000053","volume":"27","author":"Aaron Stump","year":"2017","unstructured":"Aaron Stump. The calculus of dependent lambda eliminations. J. Funct. Program., 27:e14, 2017.","journal-title":"J. Funct. Program."},{"key":"8_CR99","doi-asserted-by":"crossref","unstructured":"N. Tabareau, E. Tanter, and M. Sozeau. The marriage of univalence and parametricity. J. ACM, 68(1):5:1\u20135:44, 2021.","DOI":"10.1145\/3429979"},{"key":"8_CR100","doi-asserted-by":"crossref","unstructured":"W. W. Tait. Intensional interpretations of functionals of finite type. I. J. Symb. Log., 32:198\u2013212, 1967.","DOI":"10.2307\/2271658"},{"key":"8_CR101","doi-asserted-by":"crossref","unstructured":"G. Takeuti. On the fundamental conjecture of GLC. I, II. J. Math. Soc. Japan, 7:249\u2013275, 394\u2013408, 1955.","DOI":"10.2969\/jmsj\/00740394"},{"key":"8_CR102","unstructured":"Uemura, T.: Cubical assemblies and the independence of the propositional resizing. 24th international conference on types for proofs and programs. TYPES 2018, Braga, Portugal, p. 20, June 18\u201321, 2019"},{"key":"8_CR103","unstructured":"L.S. van Benthem Jutting. Checking Landau\u2019 \u201cGrundlagen\u201d in the AUTOMATH system. PhD thesis, University of Eindhoven, 1977."},{"key":"8_CR104","unstructured":"L.S. van Benthem Jutting. Normalization in Coquand\u2019s system, 1986. Internal Report."},{"key":"8_CR105","unstructured":"Jean van Heijenoort, editor. From Frege to G\u00f6del. A source book in mathematical logic, 1879\u20131931. Reprint of the 3rd printing of the 1967 original. Cambridge, MA: Harvard University Press, reprint of the 3rd printing of the 1967 original edition, 2002."},{"key":"8_CR106","unstructured":"V. Voevodsky. The equivalence axiom and univalent models of type theory. Notes from a talk at CMU, 2010."},{"key":"8_CR107","doi-asserted-by":"publisher","first-page":"1278","DOI":"10.1017\/S0960129514000577","volume":"25","author":"Vladimir Voevodsky","year":"2015","unstructured":"Vladimir Voevodsky. An experimental library of formalized mathematics based on the univalent foundations. Math. Structures Comput. Sci, 25:1278\u20131294, 2015.","journal-title":"Math. Structures Comput. Sci"},{"key":"8_CR108","doi-asserted-by":"crossref","unstructured":"Jan von Plato. The great formal machinery works. Princeton University Press, Princeton, NJ, 2017. Theories of deduction and computation at the origins of the digital age.","DOI":"10.23943\/princeton\/9780691174174.001.0001"},{"issue":"2","key":"8_CR109","doi-asserted-by":"publisher","first-page":"608","DOI":"10.2307\/2274873","volume":"54","author":"S S Wainer","year":"1989","unstructured":"S. S. Wainer. Slow growing versus fast growing. J. Symb. Log., 54(2):608\u2013614, 1989.","journal-title":"J. Symb. Log."},{"key":"8_CR110","volume-title":"Principia Mathematica; 2nd ed","author":"A N Whitehead","year":"1927","unstructured":"A. N. Whitehead and B. A. W. Russell. Principia Mathematica; 2nd ed. Cambridge Univ. Press, Cambridge, 1927."},{"key":"8_CR111","unstructured":"G. C. Wraith. A note on categorical datatypes. In D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts, and A. Poign\u00e9, editors, Category Theory and Computer Science, pages 118\u2013127, Berlin, Heidelberg, 1989. Springer Berlin Heidelberg."}],"container-title":["The French School of Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-34518-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,17]],"date-time":"2024-11-17T07:43:12Z","timestamp":1731829392000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-34518-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,11]]},"ISBN":["9783031345173","9783031345180"],"references-count":111,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-34518-0_8","relation":{},"subject":[],"published":{"date-parts":[[2023,10,11]]},"assertion":[{"value":"11 October 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}