{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:35:41Z","timestamp":1742913341209,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030171834"},{"type":"electronic","value":"9783030171841"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17184-1_16","type":"book-chapter","created":{"date-parts":[[2019,4,6]],"date-time":"2019-04-06T17:34:04Z","timestamp":1554572044000},"page":"440-466","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verifiable Certificates for Predicate Subtyping"],"prefix":"10.1007","author":[{"given":"Frederic","family":"Gilbert","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,4,6]]},"reference":[{"key":"16_CR1","unstructured":"Gilbert, F.: Extending higher-order logic with predicate subtyping: application to PVS. Ph.D. dissertation, Sorbonne Paris Cit\u00e9, Inria, CEA LIST (2018)"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Abel, A., Scherer, G.: On irrelevance and algorithmic equality in predicative type theory. arXiv preprint \n                      arXiv:1203.4716\n                      \n                     (2012)","DOI":"10.2168\/LMCS-8(1:29)2012"},{"issue":"2","key":"16_CR3","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H Barendregt","year":"1991","unstructured":"Barendregt, H.: Introduction to generalized type systems. J. Funct. Program. 1(2), 125\u2013154 (1991)","journal-title":"J. Funct. Program."},{"key":"16_CR4","volume-title":"Handbook of Logic in Computer Science","author":"H Barendregt","year":"1992","unstructured":"Barendregt, H.: Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. ii. Oxford University Press, Oxford (1992)"},{"key":"16_CR5","unstructured":"Barras, B., et al.: The Coq proof assistant reference manual: Version 6.1 (1997)"},{"issue":"06","key":"16_CR6","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1017\/S0956796899003573","volume":"9","author":"G Barthe","year":"1999","unstructured":"Barthe, G.: Type-checking injective pure type systems. J. Funct. Program. 9(06), 675\u2013698 (1999)","journal-title":"J. Funct. Program."},{"key":"16_CR7","unstructured":"Berardi, S.: Towards a mathematical analysis of the Coquand-Huet calculus of constructions and the other systems in Barendregt\u2019s cube. Technical report, Carnegie-Mellon University, USA and Universita di Torino, Italy (1988)"},{"key":"16_CR8","unstructured":"Bernardo, B.: An implicit calculus of constructions with dependent sums and decidable type inference. Ph.D. thesis, \u00c9cole polytechnique, October 2015"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Futatsugi, K., Goguen, J.A., Jouannaud, J.-P., Meseguer, J.: Principles of OBJ2. In: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 52\u201366. ACM (1985)","DOI":"10.1145\/318593.318610"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-60579-7_2","volume-title":"Types for Proofs and Programs","author":"H Geuvers","year":"1995","unstructured":"Geuvers, H.: A short and flexible proof of strong normalization for the calculus of constructions. In: Dybjer, P., Nordstr\u00f6m, B., Smith, J. (eds.) TYPES 1994. LNCS, vol. 996, pp. 14\u201338. Springer, Heidelberg (1995). \n                      https:\/\/doi.org\/10.1007\/3-540-60579-7_2"},{"issue":"02","key":"16_CR11","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H Geuvers","year":"1991","unstructured":"Geuvers, H., Nederhof, M.-J.: Modular proof of strong normalization for the calculus of constructions. J. Funct. Program. 1(02), 155\u2013189 (1991)","journal-title":"J. Funct. Program."},{"key":"16_CR12","unstructured":"Girard, J.-Y.: Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Ph.D. thesis, Universit\u00e9 Paris VII (1972)"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Kent, A.M., Kempe, D., Tobin-Hochstadt, S.: Occurrence typing modulo theories. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, vol. 51, pp. 296\u2013309. ACM (2016)","DOI":"10.1145\/2980983.2908091"},{"key":"16_CR14","unstructured":"Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theoret. Comput. Sci. 121(1), 279\u2013308 (1993)"},{"issue":"2","key":"16_CR15","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1145\/1667048.1667051","volume":"32","author":"K Knowles","year":"2010","unstructured":"Knowles, K., Flanagan, C.: Hybrid type checking. ACM Trans. Program. Lang. Syst. (TOPLAS) 32(2), 6 (2010)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"16_CR16","unstructured":"Luo, Z.: ECC, an extended calculus of constructions. In: Proceedings of Fourth Annual Symposium on Logic in Computer Science. LICS 1989, pp. 386\u2013395. IEEE (1989)"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). \n                      https:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"16_CR18","unstructured":"Owre, S., Shankar, N.: The formal semantics of PVS (1999)"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: ACM SIGPLAN Notices, vol. 43, pp. 159\u2013169. ACM (2008)","DOI":"10.1145\/1379022.1375602"},{"issue":"9","key":"16_CR20","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1109\/32.713327","volume":"24","author":"J Rushby","year":"1998","unstructured":"Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: predicate subtyping in PVS. IEEE Trans. Softw. Eng. 24(9), 709\u2013720 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"16_CR21","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1017\/S0956796812000044","volume":"22","author":"V Siles","year":"2012","unstructured":"Siles, V., Herbelin, H.: Pure type system conversion is always typable. J. Funct. Program. 22(2), 153\u2013180 (2012)","journal-title":"J. Funct. Program."},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-540-74464-1_16","volume-title":"Types for Proofs and Programs","author":"M Sozeau","year":"2007","unstructured":"Sozeau, M.: Subset coercions in Coq. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 237\u2013252. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-74464-1_16"},{"key":"16_CR23","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/BFb0064875","volume-title":"Logic Colloquium","author":"WW Tait","year":"1975","unstructured":"Tait, W.W.: A realizability interpretation of the theory of species. In: Parikh, R. (ed.) Logic Colloquium, vol. 453, pp. 240\u2013251. Springer, Heidelberg (1975). \n                      https:\/\/doi.org\/10.1007\/BFb0064875"},{"key":"16_CR24","unstructured":"Terlouw, J.: Een nadere bewijstheoretische analyse van GSTT\u2019s. Manuscript (in Dutch) (1989)"},{"key":"16_CR25","unstructured":"Terlouw, J.: Sterke normalisatie in C a la Tait. In: Notes of a Talk Held at the Intercity Seminar on Typed Lambda Calculus, Nijmegen, Netherlands (1989)"},{"issue":"1","key":"16_CR26","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/0168-0072(94)00040-A","volume":"73","author":"J Terlouw","year":"1995","unstructured":"Terlouw, J.: Strong normalization in type systems: a model theoretical approach. Ann. Pure Appl. Logic 73(1), 53\u201378 (1995)","journal-title":"Ann. Pure Appl. Logic"},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"604","DOI":"10.1007\/11814771_49","volume-title":"Automated Reasoning","author":"B Werner","year":"2006","unstructured":"Werner, B.: On the strength of proof-irrelevant type theories. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 604\u2013618. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11814771_49"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17184-1_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T09:22:44Z","timestamp":1558344164000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17184-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030171834","9783030171841"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17184-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"6 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"86","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"3,2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}}]}}