{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T04:10:45Z","timestamp":1772511045745,"version":"3.50.1"},"reference-count":24,"publisher":"Informa UK Limited","issue":"2","license":[{"start":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T00:00:00Z","timestamp":1648944000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"funder":[{"name":"ALEXANDRIA","award":["GA 742178"],"award-info":[{"award-number":["GA 742178"]}]}],"content-domain":{"domain":["www.tandfonline.com"],"crossmark-restriction":true},"short-container-title":["Experimental Mathematics"],"published-print":{"date-parts":[[2022,4,3]]},"DOI":"10.1080\/10586458.2022.2062073","type":"journal-article","created":{"date-parts":[[2022,4,25]],"date-time":"2022-04-25T14:34:07Z","timestamp":1650897247000},"page":"364-382","update-policy":"https:\/\/doi.org\/10.1080\/tandf_crossmark_01","source":"Crossref","is-referenced-by-count":8,"title":["Simple Type Theory is not too Simple: Grothendieck\u2019s Schemes Without Dependent Types"],"prefix":"10.1080","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1694-9467","authenticated-orcid":false,"given":"Anthony","family":"Bordg","sequence":"first","affiliation":[{"name":"University of Cambridge, Cambridge, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0288-4279","authenticated-orcid":false,"given":"Lawrence","family":"Paulson","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9886-9542","authenticated-orcid":false,"given":"Wenda","family":"Li","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, UK"}]}],"member":"301","published-online":{"date-parts":[[2022,4,25]]},"reference":[{"key":"CIT0001","doi-asserted-by":"publisher","DOI":"10.1007\/11812289_4"},{"key":"CIT0002","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9284-7"},{"key":"CIT0003","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09537-9"},{"key":"CIT0004","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-014-0181-1"},{"key":"CIT0005","unstructured":"Bordg, A., Paulson, L., Li, W. (2021). Grothendieck\u2019s schemes in algebraic geometry. Archive of Formal Proofs, March 2021. Available at https:\/\/isa-afp.org\/entries\/Grothendieck_Schemes.html, Formal proof development."},{"key":"CIT0006","doi-asserted-by":"publisher","DOI":"10.1080\/10586458.2021.1983489"},{"key":"CIT0007","unstructured":"Chicli, L. I. (2003). Sur la Formalisation des Math\u00e9matiques dans le Calcul des Constructions inductives. PhD thesis. Universit\u00e9 C\u00f4te d\u2019Azur. 2003NICE4088."},{"key":"CIT0008","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"CIT0009","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual. Available at http:\/\/coq.inria.fr."},{"key":"CIT0010","unstructured":"Coquand, T., Huet, G. (1986). The calculus of constructions. PhD thesis. INRIA."},{"key":"CIT0011","first-page":"50","volume-title":"International Conference on Computer Logic","author":"Coquand T.","year":"1988"},{"key":"CIT0012","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"CIT0013","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_12"},{"key":"CIT0014","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"CIT0015","doi-asserted-by":"publisher","DOI":"10.1007\/BF02684778"},{"key":"CIT0016","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3849-0"},{"key":"CIT0017","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_21"},{"key":"CIT0018","unstructured":"Kobayashi, H., Chen, L., Murao, H. (2004). Groups, rings and modules. Archive of Formal Proofs, May 2004. Available at https:\/\/isa-afp.org\/entries\/Group-Ring-Module.html, Formal proof development."},{"key":"CIT0019","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9464-6"},{"key":"CIT0020","volume-title":"Algebra. Graduate Texts in Mathematics","author":"Lang S.","year":"2002"},{"key":"CIT0021","unstructured":"Lee, H. (2014). Vector spaces. Archive of Formal Proofs. Available at https:\/\/isa-afp.org\/entries\/VectorSpace.html, Formal proof development."},{"key":"CIT0022","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"CIT0023","unstructured":"The Stacks Project Authors. (2018). Stacks Project. Available at https:\/\/stacks.math.columbia.edu."},{"key":"CIT0024","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028402"}],"container-title":["Experimental Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.tandfonline.com\/doi\/pdf\/10.1080\/10586458.2022.2062073","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,8]],"date-time":"2022-08-08T16:10:32Z","timestamp":1659975032000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.tandfonline.com\/doi\/full\/10.1080\/10586458.2022.2062073"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,3]]},"references-count":24,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,4,3]]}},"alternative-id":["10.1080\/10586458.2022.2062073"],"URL":"https:\/\/doi.org\/10.1080\/10586458.2022.2062073","relation":{},"ISSN":["1058-6458","1944-950X"],"issn-type":[{"value":"1058-6458","type":"print"},{"value":"1944-950X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,3]]},"assertion":[{"value":"The publishing and review policy for this title is described in its Aims & Scope.","order":1,"name":"peerreview_statement","label":"Peer Review Statement"},{"value":"http:\/\/www.tandfonline.com\/action\/journalInformation?show=aimsScope&journalCode=uexm20","URL":"http:\/\/www.tandfonline.com\/action\/journalInformation?show=aimsScope&journalCode=uexm20","order":2,"name":"aims_and_scope_url","label":"Aim & Scope"},{"value":"2022-04-25","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}