{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:11Z","timestamp":1761611171259},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540590484"},{"type":"electronic","value":"9783540491781"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0014042","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:50:31Z","timestamp":1132732231000},"page":"16-31","source":"Crossref","is-referenced-by-count":6,"title":["Extensions of pure type systems"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"2_CR1","unstructured":"H. Barendregt. Typed \u03bb-calculi, Handbook of logic in computer science, Abramsky and al eds, OUP 1992."},{"key":"2_CR2","unstructured":"G. Barthe. Towards a mathematical vernacular, submitted."},{"key":"2_CR3","unstructured":"G. Barthe. Formalizing mathematics in type theory: fundamentals and case studies, submitted."},{"key":"2_CR4","unstructured":"G. Barthe. An introduction to quotient and congruence types, manuscript, University of Nijmegen, November 1994."},{"key":"2_CR5","unstructured":"R. Constable and al. Implementing Mathematics with the NuPrl Proof Development System, Prenctice Hall, 1986."},{"key":"2_CR6","unstructured":"T. Coquand. A new paradox in type theory, in the proceedings of the 9th Congress of Logic, Methodology and Philosophy of Science."},{"key":"2_CR7","unstructured":"H. Geuvers. Logics and type systems, Ph.D thesis, University of Nijmegen, 1993."},{"key":"2_CR8","unstructured":"H. Geuvers. A short and flexible proof of strong normalisation for the Calculus of Constructions, submitted."},{"key":"2_CR9","unstructured":"M. Hofmann. Extensional concepts in intensional type theory, Ph.D thesis, University of Edinburgh, forthcoming."},{"key":"2_CR10","unstructured":"M. Hofmann. A simple model for quotient types, in these proceedings."},{"key":"2_CR11","unstructured":"B. Jacobs. Categorical Logic and Type Theory, in preparation."},{"key":"2_CR12","unstructured":"B. Jacobs. Quotients in simple Type Theory, submitted."},{"key":"2_CR13","unstructured":"J. Lambek and P.J. Scott. Introduction to higher-order categorical logic, CUP, 1986."},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Z. Luo. Computation and reasoning: a type theory for computer science, OUP, 1994.","DOI":"10.1093\/oso\/9780198538356.001.0001"},{"key":"2_CR15","unstructured":"N. Mendler. Quotient types via coequalisers in Martin-Lof's type theory, in the informal proceedings of the workshop on logical frameworks, Antibes, May 1990."},{"key":"2_CR16","unstructured":"R. Nederpelt and al (eds). Selected Papers on Automath, North-Holland, 1994."},{"key":"2_CR17","unstructured":"B. Nordstrom, K. Petersson and J. Smith. Programming in Martin-Lof's type theory, OUP, 1990."},{"key":"2_CR18","unstructured":"E. Poll and P. Severi. PTS with definitions, in proceedings of LFCS'94, LNCS 813."},{"key":"2_CR19","unstructured":"G. Pottinger. Definite descriptions and excluded middle in the theory of constructions, TYPES mailing list, November 1989."},{"key":"2_CR20","unstructured":"A. Salvesen and J. Smith. The strength of the subset type in Martin-Lof's type theory, proceedings of LICS'88, 1988."},{"key":"2_CR21","volume-title":"Strong normalisation in type systems: a model-theoretical approach","author":"J. Terlouw","year":"1993","unstructured":"J. Terlouw. Strong normalisation in type systems: a model-theoretical approach, Dirk van Dalen Festschrift, Utrecht, 1993."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014042","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,1]],"date-time":"2024-02-01T02:12:43Z","timestamp":1706753563000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014042"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540590484","9783540491781"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/bfb0014042","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}