{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,8]],"date-time":"2025-01-08T05:31:46Z","timestamp":1736314306560,"version":"3.32.0"},"publisher-location":"Berlin\/Heidelberg","reference-count":15,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540565175"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0037103","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:21:36Z","timestamp":1138202496000},"page":"139-145","source":"Crossref","is-referenced-by-count":13,"title":["The undecidability of typability in the Lambda-Pi-calculus"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Dowek","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"10_CR1","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H. Barendregt","year":"1991","unstructured":"H. Barendregt, Introduction to Generalized Type Systems, Journal of Functional Programming 1, 2 (1991) 125\u2013154.","journal-title":"Journal of Functional Programming"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Th. Coquand, An Algorithm for Testing Conversion in Type Theory, Logical Frameworks, G. Huet and G. Plotkin (Eds.), Cambridge University Press (1991).","DOI":"10.1017\/CBO9780511569807.011"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"L. Damas, R. Milner, Principal Type-Scheme for Functional Programs, Proceedings of Principles of Programming Languages (1982).","DOI":"10.1145\/582153.582176"},{"issue":"12","key":"10_CR4","first-page":"951","volume":"312","author":"G. Dowek","year":"1991","unstructured":"G. Dowek, L'Ind\u00e9cidabilit\u00e9 du Filtrage du Troisi\u00e8me Ordre dans les Calculs avec Types D\u00e9pendants ou Constructeurs de Types (The Undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors), Comptes Rendus \u00e0 l'Acad\u00e9mie des Sciences I, 312, 12 (1991) 951\u2013956.","journal-title":"Comptes Rendus \u00e0 l'Acad\u00e9mie des Sciences I"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"G. Dowek, Third Order Matching is Decidable, Proceedings of Logic in Computer Science (1992) 2\u201310.","DOI":"10.1109\/LICS.1992.185514"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"H. Geuvers, The Church-Rosser Property for \u03b2\u03b7-reduction in Typed Lambda Calculi, Proceedings of Logic in Computer Science (1992) 453\u2013460.","DOI":"10.1109\/LICS.1992.185556"},{"key":"10_CR7","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W.D. Goldfarb","year":"1981","unstructured":"W.D. Goldfarb, The Undecidability of the Second-Order Unification Problem, Theoretical Computer Science 13 (1981) 225\u2013230.","journal-title":"Theoretical Computer Science"},{"key":"10_CR8","unstructured":"R. Harper, F. Honsell, G. Plotkin, A Framework for Defining Logics, Proceedings of Logic in Computer Science (1987) 194\u2013204."},{"key":"10_CR9","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","volume":"22","author":"G. Huet","year":"1973","unstructured":"G. Huet, The Undecidability of Unification in Third Order Logic, Information and Control 22 (1973) 257\u2013267.","journal-title":"Information and Control"},{"key":"10_CR10","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"G. Huet, A Unification Algorithm for Typed \u03bb-calculus, Theoretical Computer Science 1 (1975) 27\u201357.","journal-title":"Theoretical Computer Science"},{"key":"10_CR11","unstructured":"G. Huet, R\u00e9solution d'\u00c9quations dans les Langages d'Ordre 1, 2, ..., \u03c9, Th\u00e8se de Doctorat d'\u00c9tat, Universit\u00e9 de Paris VII (1976)."},{"key":"10_CR12","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G. Huet","year":"1978","unstructured":"G. Huet, B. Lang, Proving and Applying Program Transformations Expressed with Second Order Patterns, Acta Informatica 11 (1978) 31\u201355.","journal-title":"Acta Informatica"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"F. Pfenning, Logic Programming in the LF Logical Framework, Logical Frameworks, G. Huet and G. Plotkin (Eds.), Cambridge University Press (1991).","DOI":"10.1017\/CBO9780511569807.008"},{"key":"10_CR14","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1090\/S0002-9904-1946-08555-9","volume":"52","author":"E. L. Post","year":"1946","unstructured":"E. L. Post, A Variant of a Recursively Unsolvable Problem, Bulletin of American Mathematical Society 52 (1946) 264\u2013268.","journal-title":"Bulletin of American Mathematical Society"},{"key":"10_CR15","unstructured":"A. Salvesen, The Church-Rosser Theorem for Pure Type Systems with \u03b2\u03b7-reduction, Manuscript, University of Edinburgh (1991)."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0037103.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T11:50:29Z","timestamp":1736250629000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0037103"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540565175"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/bfb0037103","relation":{},"subject":[]}}