{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T23:26:24Z","timestamp":1744068384259,"version":"3.28.0"},"reference-count":12,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/lics.2000.855752","type":"proceedings-article","created":{"date-parts":[[2002,11,7]],"date-time":"2002-11-07T17:04:51Z","timestamp":1036688691000},"page":"18-29","source":"Crossref","is-referenced-by-count":6,"title":["A model for impredicative type systems, universes, intersection types and subtyping"],"prefix":"10.1109","author":[{"given":"A.","family":"Miquel","sequence":"first","affiliation":[]}],"member":"263","reference":[{"key":"ref4","first-page":"453","article-title":"The Church-Rosser property for ?n-reduction in typed lambda calculi","author":"geuvers","year":"0","journal-title":"Proceedings of the seventh annual symposium on Logic in Computer Science"},{"key":"ref3","doi-asserted-by":"crossref","first-page":"87","DOI":"10.3233\/FI-1993-191-205","article-title":"Type inference: some results, some problems","volume":"19","author":"giannini","year":"1993","journal-title":"Fundamenta Informaticae"},{"journal-title":"M\ufffdmoire de DEA","year":"1998","author":"miquel","key":"ref10"},{"journal-title":"Proofs and Types","year":"1989","author":"girard","key":"ref6"},{"journal-title":"Habilitation \ufffd diriger des recherches","year":"1996","author":"paulin-mohring","key":"ref11"},{"key":"ref5","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","article-title":"A modular proof of Strong Normalization for the Calculus of Constructions","volume":"1","author":"geuvers","year":"1991","journal-title":"Journal of Functional Programming"},{"journal-title":"Une th\ufffdorie des Constructions Inductives","year":"1994","author":"werner","key":"ref12"},{"journal-title":"Th\ufffdorie des ensembles","year":"1998","author":"krivine","key":"ref8"},{"journal-title":"Locus Solus","year":"1999","author":"girard","key":"ref7"},{"journal-title":"The Coq Proof Assistant Reference Manual - Version V6 1","year":"1997","author":"barras","key":"ref2"},{"key":"ref9","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538356.001.0001","author":"luo","year":"1994","journal-title":"Computation and Reasoning A Type Theory for Computer Science"},{"journal-title":"Constructions Inductive Types and Strong Normalization","year":"1993","author":"altenkirch","key":"ref1"}],"event":{"name":"Fifteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2000)","acronym":"LICS-00","location":"Santa Barbara, CA, USA"},"container-title":["Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332)"],"original-title":[],"link":[{"URL":"https:\/\/linproxy.fan.workers.dev:443\/http\/xplorestaging.ieee.org\/ielx5\/6908\/18575\/00855752.pdf?arnumber=855752","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,7]],"date-time":"2024-01-07T11:27:58Z","timestamp":1704626878000},"score":1,"resource":{"primary":{"URL":"https:\/\/linproxy.fan.workers.dev:443\/http\/ieeexplore.ieee.org\/document\/855752\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":12,"URL":"https:\/\/linproxy.fan.workers.dev:443\/https\/doi.org\/10.1109\/lics.2000.855752","relation":{},"subject":[]}}