{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T07:38:09Z","timestamp":1790840289329,"version":"4.1.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030336356","type":"print"},{"value":"9783030336363","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-33636-3_7","type":"book-chapter","created":{"date-parts":[[2019,10,19]],"date-time":"2019-10-19T14:02:20Z","timestamp":1571493740000},"page":"155-196","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Setoid Type Theory\u2014A Syntactic Translation"],"prefix":"10.1007","author":[{"given":"Thorsten","family":"Altenkirch","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Simon","family":"Boulier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ambrus","family":"Kaposi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nicolas","family":"Tabareau","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,10,20]]},"reference":[{"key":"7_CR1","unstructured":"Altenkirch, T.: Extensional equality in intensional type theory. In: 14th Symposium on Logic in Computer Science, pp. 412\u2013420 (1999)"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Altenkirch, T., Kaposi, A.: Type theory in type theory using quotient inductive types. In: Bodik, R., Majumdar, R. (eds.) Proceedings of POPL 2016, St. Petersburg, FL, USA, January 2016, pp. 18\u201329. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837638","DOI":"10.1145\/2837614.2837638"},{"key":"7_CR3","doi-asserted-by":"publisher","unstructured":"Altenkirch, T., Kaposi, A.: Towards a cubical type theory without an interval. In: Uustalu, T. (ed.) TYPES 2015. Leibniz International Proceedings in Informatics (LIPIcs), vol. 69, pp. 3:1\u20133:27. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2018). https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2015.3","DOI":"10.4230\/LIPIcs.TYPES.2015.3"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., Mcbride, C., Swierstra, W.: Observational equality, now! In: PLPV 2007: Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification, pp. 57\u201358. ACM (2007)","DOI":"10.1145\/1292597.1292608"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-94821-8_2","volume-title":"Interactive Theorem Proving","author":"A Anand","year":"2018","unstructured":"Anand, A., Boulier, S., Cohen, C., Sozeau, M., Tabareau, N.: Towards certified meta-programming with typed Template-Coq. In: Avigad, J., Mahboubi, A. (eds.) ITP 2018. LNCS, vol. 10895, pp. 20\u201339. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94821-8_2"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Atkey, R., Ghani, N., Johann, P.: A relationally parametric model of dependent type theory. In: Jagannathan, S., Sewell, P. (eds.) Proceedings of POPL 2014, San Diego, CA, USA, 20\u201321 January 2014, pp. 503\u2013516. ACM (2014)","DOI":"10.1145\/2578855.2535852"},{"issue":"02","key":"7_CR7","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1017\/S0956796812000056","volume":"22","author":"JP Bernardy","year":"2012","unstructured":"Bernardy, J.P., Jansson, P., Paterson, R.: Proofs for free \u2013 parametricity for dependent types. J. Funct. Program. 22(02), 107\u2013152 (2012). https:\/\/doi.org\/10.1017\/S0956796812000056","journal-title":"J. Funct. Program."},{"key":"7_CR8","unstructured":"Bezem, M., Coquand, T., Huber, S.: A model of type theory in cubical sets. In: 19th International Conference on Types for Proofs and Programs (TYPES 2013), vol. 26, pp. 107\u2013128 (2014)"},{"key":"7_CR9","unstructured":"Boulier, S.: Extending type theory with syntactic models. Ph.D. thesis, \u00c9cole des Mines de Nantes (2018)"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Boulier, S., P\u00e9drot, P.M., Tabareau, N.: The next 700 syntactical models of type theory. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp. 182\u2013194. ACM, New York (2017). https:\/\/doi.org\/10.1145\/3018610.3018620","DOI":"10.1145\/3018610.3018620"},{"key":"7_CR11","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0168-0072(86)90053-9","volume":"32","author":"J Cartmell","year":"1986","unstructured":"Cartmell, J.: Generalised algebraic theories and contextual categories. Ann. Pure Appl. Logic 32, 209\u2013243 (1986)","journal-title":"Ann. Pure Appl. Logic"},{"key":"7_CR12","unstructured":"Cohen, C., Coquand, T., Huber, S., M\u00f6rtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom. In: Uustalu, T. (ed.) TYPES 2015. Leibniz International Proceedings in Informatics (LIPIcs), vol. 69, pp. 5:1\u20135:34. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2018)"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/3-540-61780-9_66","volume-title":"Types for Proofs and Programs","author":"P Dybjer","year":"1996","unstructured":"Dybjer, P.: Internal type theory. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 120\u2013134. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61780-9_66"},{"issue":"POPL","key":"7_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3290316","volume":"3","author":"Ga\u00ebtan Gilbert","year":"2019","unstructured":"Gilbert, G., Cockx, J., Sozeau, M., Tabareau, N.: Definitional proof-irrelevance without K. In: Proceedings of POPL 2019, Lisbon, Portugal, January 2019","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"7_CR15","unstructured":"Herbelin, H.: Syntactic investigations into cubical type theory. In: Esp\u00edrito Santo, J., Pinto, L. (eds.) TYPES 2018. University of Minho (2018)"},{"key":"7_CR16","first-page":"153","volume-title":"Lecture Notes in Computer Science","author":"Martin Hofmann","year":"1996","unstructured":"Hofmann, M.: Conservativity of equality reflection over intensional type theory. In: TYPES 1995, pp. 153\u2013164 (1995)"},{"key":"7_CR17","unstructured":"Hofmann, M.: Extensional concepts in intensional type theory. Thesis, University of Edinburgh, Department of Computer Science (1995)"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: Syntax and semantics of dependent types. In: Semantics and Logics of Computation, pp. 79\u2013130. Cambridge University Press (1997)","DOI":"10.1017\/CBO9780511526619.004"},{"key":"7_CR19","unstructured":"Hofmann, M., Streicher, T.: The groupoid interpretation of type theory. In: In Venice Festschrift, pp. 83\u2013111. Oxford University Press (1996)"},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"Jaber, G., Lewertowski, G., P\u00e9drot, P., Sozeau, M., Tabareau, N.: The definitional side of the forcing. In: Grohe, M., Koskinen, E., Shankar, N. (eds.) Proceedings of LICS 2016, New York, NY, USA, 5\u20138 July 2016, pp. 367\u2013376. ACM (2016). https:\/\/doi.org\/10.1145\/2933575.2935320","DOI":"10.1145\/2933575.2935320"},{"key":"7_CR21","unstructured":"Kaposi, A.: The setoid model formalized in Agda, May 2019. https:\/\/bitbucket.org\/akaposi\/setoid\/src\/master\/agda"},{"issue":"POPL","key":"7_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3290315","volume":"3","author":"Ambrus Kaposi","year":"2019","unstructured":"Kaposi, A., Kov\u00e1cs, A., Altenkirch, T.: Constructing quotient inductive-inductive types. Proc. ACM Program. Lang. 3(POPL), 2:1\u20132:24 (2019). https:\/\/doi.org\/10.1145\/3290315","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"7_CR23","unstructured":"Martin-L\u00f6f, P.: Intuitionistic type theory, Studies in Proof Theory, vol. 1. Bibliopolis (1984)"},{"key":"7_CR24","unstructured":"Matthieu Sozeau, N.T.: Univalence for free (2013). http:\/\/hal.inria.fr\/hal-00786589\/en"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-45842-5_13","volume-title":"Types for Proofs and Programs","author":"C McBride","year":"2002","unstructured":"McBride, C.: Elimination with a motive. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 197\u2013216. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45842-5_13"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/11541868_18","volume-title":"Theorem Proving in Higher Order Logics","author":"N Oury","year":"2005","unstructured":"Oury, N.: Extensionality in the calculus of constructions. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 278\u2013293. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11541868_18"},{"key":"7_CR27","unstructured":"Program, T.U.F.: Homotopy type theory: univalent foundations of mathematics. Technical report, Institute for Advanced Study (2013)"},{"key":"7_CR28","doi-asserted-by":"publisher","unstructured":"Sterling, J., Angiuli, C., Gratzer, D.: Cubical syntax for reflection-free extensional equality. In: Geuvers, H. (ed.) Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), vol. 131 (2019). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.32","DOI":"10.4230\/LIPIcs.FSCD.2019.32"},{"key":"7_CR29","unstructured":"Streicher, T.: Investigations into intensional type theory. Habilitation thesis (1993)"},{"key":"7_CR30","doi-asserted-by":"publisher","unstructured":"Tabareau, N., Tanter, \u00c9., Sozeau, M.: Equivalences for free. In: ICFP 2018 - International Conference on Functional Programming, Saint-Louis, United States, September 2018. https:\/\/doi.org\/10.1145\/3234615","DOI":"10.1145\/3234615"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-41582-1_10","volume-title":"Implementation and Application of Functional Languages","author":"P Walt van der","year":"2013","unstructured":"van der Walt, P., Swierstra, W.: Engineering proof by reflection in agda. In: Hinze, R. (ed.) IFL 2012. LNCS, vol. 8241, pp. 157\u2013173. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41582-1_10"},{"key":"7_CR32","unstructured":"Winterhalter, T., Sozeau, M., Tabareau, N.: Using reflection to eliminate reflection. In: Santo, J.E., Pinto, L. (eds.) 24th International Conference on Types for Proofs and Programs, TYPES 2018. University of Minho (2018)"}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-33636-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,2]],"date-time":"2022-10-02T05:09:19Z","timestamp":1664687359000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-33636-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030336356","9783030336363"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-33636-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"20 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"MPC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Mathematics of Program Construction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","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":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mpc2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.nott.ac.uk\/~pszgmh\/mpc19.html","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 (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"68% - 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 (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}