{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:18:00Z","timestamp":1763468280496,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":83,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,1,18]],"date-time":"2016-01-18T00:00:00Z","timestamp":1453075200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001866","name":"Fonds National de la Recherche Luxembourg","doi-asserted-by":"publisher","award":["FNR\/P14\/8149128"],"award-info":[{"award-number":["FNR\/P14\/8149128"]}],"id":[{"id":"10.13039\/501100001866","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,18]]},"DOI":"10.1145\/2854065.2854077","type":"proceedings-article","created":{"date-parts":[[2016,1,12]],"date-time":"2016-01-12T13:18:57Z","timestamp":1452604737000},"page":"130-141","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["A nominal exploration of intuitionism"],"prefix":"10.1145","author":[{"given":"Vincent","family":"Rahli","sequence":"first","affiliation":[{"name":"University of Luxembourg, Luxembourg"}]},{"given":"Mark","family":"Bickford","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}]}],"member":"320","published-online":{"date-parts":[[2016,1,18]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"IEEE Computer Society","author":"LICS","year":"2007","unstructured":"LICS 2007. IEEE Computer Society , 2007 . LICS 2007. IEEE Computer Society, 2007."},{"key":"e_1_3_2_1_2_1","unstructured":"The Agda wiki. http:\/\/wiki.portal.chalmers.se\/agda\/pmwi ki.php. The Agda wiki. http:\/\/wiki.portal.chalmers.se\/agda\/pmwi ki.php."},{"key":"e_1_3_2_1_3_1","volume-title":"An abstract semantics for atoms in Nuprl. Technical report","author":"Allen Stuart","year":"2006","unstructured":"Stuart Allen . An abstract semantics for atoms in Nuprl. Technical report , Cornell University , 2006 . Stuart Allen. An abstract semantics for atoms in Nuprl. Technical report, Cornell University, 2006."},{"key":"e_1_3_2_1_4_1","first-page":"221","volume-title":"LICS","author":"Allen Stuart F.","unstructured":"Stuart F. Allen . A non-type-theoretic definition of Martin-L\u00f6f\u2019s types . In LICS , pages 215\u2013 221 . IEEE Computer Society, 1987. Stuart F. Allen. A non-type-theoretic definition of Martin-L\u00f6f\u2019s types. In LICS, pages 215\u2013221. IEEE Computer Society, 1987."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.10.005"},{"key":"e_1_3_2_1_7_1","series-title":"LNCS","first-page":"44","volume-title":"ITP","author":"Anand Abhishek","year":"2014","unstructured":"Abhishek Anand and Vincent Rahli . Towards a formally verified proof assistant . In ITP 2014 , volume 8558 of LNCS , pages 27\u2013 44 . Springer, 2014. Abhishek Anand and Vincent Rahli. Towards a formally verified proof assistant. In ITP 2014, volume 8558 of LNCS, pages 27\u201344. Springer, 2014."},{"key":"e_1_3_2_1_8_1","volume-title":"Towards a formally verified proof assistant. Technical report","author":"Anand Abhishek","year":"2014","unstructured":"Abhishek Anand and Vincent Rahli . Towards a formally verified proof assistant. Technical report , Cornell University , 2014 . http:\/\/www.n uprl.org\/html\/Nuprl2Coq\/. Abhishek Anand and Vincent Rahli. Towards a formally verified proof assistant. Technical report, Cornell University, 2014. http:\/\/www.n uprl.org\/html\/Nuprl2Coq\/."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1102022660"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-68952-9"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005093"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/993954"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_7"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61667-9"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103704"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929529.1929536"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511565663"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.115"},{"key":"e_1_3_2_1_21_1","volume-title":"A dependent nominal type theory. Logical Methods in Computer Science, 8(1)","author":"Cheney James","year":"2012","unstructured":"James Cheney . A dependent nominal type theory. Logical Methods in Computer Science, 8(1) , 2012 . James Cheney. A dependent nominal type theory. Logical Methods in Computer Science, 8(1), 2012."},{"key":"e_1_3_2_1_22_1","series-title":"LNCS","first-page":"283","volume-title":"ICLP","author":"Cheney James","year":"2004","unstructured":"James Cheney and Christian Urban . alpha-prolog: A logic programming language with names, binding and a-equivalence . In ICLP 2004 , volume 3132 of LNCS , pages 269\u2013 283 . Springer, 2004. James Cheney and Christian Urban. alpha-prolog: A logic programming language with names, binding and a-equivalence. In ICLP 2004, volume 3132 of LNCS, pages 269\u2013283. Springer, 2004."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1387673.1387675"},{"key":"e_1_3_2_1_24_1","volume-title":"December","author":"Cohen Paul J.","year":"1963","unstructured":"Paul J. Cohen . The independence of the continuum hypothesis. the National Academy of Sciences of the United States of America, 50(6):1143\u20131148 , December 1963 . Paul J. Cohen. The independence of the continuum hypothesis. the National Academy of Sciences of the United States of America, 50(6):1143\u20131148, December 1963."},{"key":"e_1_3_2_1_25_1","volume-title":"January","author":"Cohen Paul J.","year":"1964","unstructured":"Paul J. Cohen . The independence of the continuum hypothesis ii. the National Academy of Sciences of the United States of America, 51(1):105\u2013110 , January 1964 . Paul J. Cohen. The independence of the continuum hypothesis ii. the National Academy of Sciences of the United States of America, 51(1):105\u2013110, January 1964."},{"key":"e_1_3_2_1_26_1","volume-title":"Implementing mathematics with the Nuprl proof development system","author":"Constable R.L.","year":"1986","unstructured":"R.L. Constable , S.F. Allen , H.M. Bromley , W.R. Cleaveland , J.F. Cremer , R.W. Harper , D.J. Howe , T.B. Knoblock , N.P. Mendler , P. Panangaden , J.T. Sasaki , and S.F. Smith . Implementing mathematics with the Nuprl proof development system . Prentice-Hall, Inc. , Upper Saddle River, NJ, USA, 1986 . R.L. Constable, S.F. Allen, H.M. Bromley, W.R. Cleaveland, J.F. Cremer, R.W. Harper, D.J. Howe, T.B. Knoblock, N.P. Mendler, P.Panangaden, J.T. Sasaki, and S.F. Smith. Implementing mathematics with the Nuprl proof development system. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1986."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2013.07.009"},{"key":"e_1_3_2_1_28_1","series-title":"LNCS","first-page":"77","volume-title":"Fundamentals of Computation Theory, Proceedings of the 1983 International","author":"Constable Robert L.","unstructured":"Robert L. Constable . Constructive mathematics as a programming logic I: some principles of theory . In Fundamentals of Computation Theory, Proceedings of the 1983 International , volume 158 of LNCS , pages 64\u2013 77 . Springer, 1983. Robert L. Constable. Constructive mathematics as a programming logic I: some principles of theory. In Fundamentals of Computation Theory, Proceedings of the 1983 International, volume 158 of LNCS, pages 64\u201377. Springer, 1983."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90085-8"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1839560.1839564"},{"key":"e_1_3_2_1_31_1","series-title":"Logic","first-page":"213","volume-title":"Epistemology versus Ontology","author":"Coquand Thierry","unstructured":"Thierry Coquand and Guilhem Jaber . A computational interpretation of forcing in type theory . In Epistemology versus Ontology , volume 27 of Logic , Epistemology, and the Unity of Science , pages 203\u2013 213 . Springer, 2012. Thierry Coquand and Guilhem Jaber. A computational interpretation of forcing in type theory. In Epistemology versus Ontology, volume 27 of Logic, Epistemology, and the Unity of Science, pages 203\u2013213. Springer, 2012."},{"key":"e_1_3_2_1_32_1","first-page":"66","volume-title":"Int\u2019l Conf. on Computer Logic","volume":"417","author":"Coquand Thierry","unstructured":"Thierry Coquand and Christine Paulin . Inductively defined types. In COLOG-88 , Int\u2019l Conf. on Computer Logic , volume 417 of LNCS, pages 50\u2013 66 . Springer, 1988. Thierry Coquand and Christine Paulin. Inductively defined types. In COLOG-88, Int\u2019l Conf. on Computer Logic, volume 417 of LNCS, pages 50\u201366. Springer, 1988."},{"key":"e_1_3_2_1_33_1","unstructured":"The Coq Proof Assistant. http:\/\/coq.inria.fr\/. The Coq Proof Assistant. http:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2013.09.009"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005362"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198505242.001.0001","volume-title":"Elements of Intuitionism","author":"Dummett Michael A. E.","year":"2000","unstructured":"Michael A. E. Dummett . Elements of Intuitionism . Clarendon Press , second edition, 2000 . Michael A. E. Dummett. Elements of Intuitionism. Clarendon Press, second edition, 2000."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/jsl.2014.82"},{"key":"e_1_3_2_1_39_1","volume-title":"The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation. TLCA\u20192015,","author":"Escard\u00b4o Mart\u00b4\u0131n","year":"2015","unstructured":"Mart\u00b4\u0131n Escard\u00b4o and Chuangjie Xu . The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation. TLCA\u20192015, available at http:\/\/www.cs.bham.ac.uk\/~mhe\/pap ers\/escardo-xu-inconsistency-continuity.pdf, 2015 . Mart\u00b4\u0131n Escard\u00b4o and Chuangjie Xu. The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation. TLCA\u20192015, available at http:\/\/www.cs.bham.ac.uk\/~mhe\/pap ers\/escardo-xu-inconsistency-continuity.pdf, 2015."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.25"},{"key":"e_1_3_2_1_41_1","volume-title":"Exhaustible sets in higher-type computation. Logical Methods in Computer Science, 4(3)","author":"Escard\u00b4o Mart\u00b4\u0131n H\u00f6tzel","year":"2008","unstructured":"Mart\u00b4\u0131n H\u00f6tzel Escard\u00b4o . Exhaustible sets in higher-type computation. Logical Methods in Computer Science, 4(3) , 2008 . Mart\u00b4\u0131n H\u00f6tzel Escard\u00b4o. Exhaustible sets in higher-type computation. Logical Methods in Computer Science, 4(3), 2008."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2013.09.010"},{"key":"e_1_3_2_1_43_1","series-title":"LIPIcs","first-page":"195","volume-title":"TLCA","author":"Fairweather Elliot","year":"2015","unstructured":"Elliot Fairweather , Maribel Fern\u00e1ndez , Nora Szasz , and Alvaro Tasistro . Dependent types for nominal terms with atom substitutions . In TLCA 2015 , volume 38 of LIPIcs , pages 180\u2013 195 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Elliot Fairweather, Maribel Fern\u00e1ndez, Nora Szasz, and Alvaro Tasistro. Dependent types for nominal terms with atom substitutions. In TLCA 2015, volume 38 of LIPIcs, pages 180\u2013195. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015."},{"key":"e_1_3_2_1_44_1","first-page":"224","volume-title":"LICS\u20191999 {58}","author":"Gabbay Murdoch","unstructured":"Murdoch Gabbay and Andrew M. Pitts . A new approach to abstract syntax involving binders . In LICS\u20191999 {58} , pages 214\u2013 224 . Murdoch Gabbay and Andrew M. Pitts. A new approach to abstract syntax involving binders. In LICS\u20191999 {58}, pages 214\u2013224."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273264"},{"key":"e_1_3_2_1_46_1","volume-title":"Cambridge University Press","author":"Girard Jean-Yves","year":"1989","unstructured":"Jean-Yves Girard , Paul Taylor , and Yves Lafont . Proofs and Types . Cambridge University Press , 1989 . Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and Types. Cambridge University Press, 1989."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80013-6"},{"key":"e_1_3_2_1_48_1","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"Gordon Michael J. C.","year":"1979","unstructured":"Michael J. C. Gordon , Robin Milner , and Christopher P. Wadsworth . Edinburgh LCF: A Mechanised Logic of Computation ., volume 78 of LNCS . Springer-Verlag , 1979 . Michael J. C. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation., volume 78 of LNCS. Springer-Verlag, 1979."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77371"},{"key":"e_1_3_2_1_51_1","unstructured":"Idris. http:\/\/www.idris-lang.org\/. Idris. http:\/\/www.idris-lang.org\/."},{"key":"e_1_3_2_1_52_1","first-page":"66","volume-title":"LICS\u20191999 {58}","author":"Jeffrey Alan","unstructured":"Alan Jeffrey and Julian Rathke . Towards a theory of bisimulation for local names . In LICS\u20191999 {58} , pages 56\u2013 66 . Alan Jeffrey and Julian Rathke. Towards a theory of bisimulation for local names. In LICS\u20191999 {58}, pages 56\u201366."},{"key":"e_1_3_2_1_53_1","volume-title":"The Foundations of Intuitionistic Mathematics, especially in relation to recursive functions","author":"Kleene S.C.","year":"1965","unstructured":"S.C. Kleene and R.E. Vesley . The Foundations of Intuitionistic Mathematics, especially in relation to recursive functions . North-Holland Publishing Company , 1965 . S.C. Kleene and R.E. Vesley. The Foundations of Intuitionistic Mathematics, especially in relation to recursive functions. North-Holland Publishing Company, 1965."},{"key":"e_1_3_2_1_54_1","volume-title":"Type classes for efficient exact real arithmetic in Coq. Logical Methods in Computer Science, 9(1)","author":"Krebbers Robbert","year":"2011","unstructured":"Robbert Krebbers and Bas Spitters . Type classes for efficient exact real arithmetic in Coq. Logical Methods in Computer Science, 9(1) , 2011 . Robbert Krebbers and Bas Spitters. Type classes for efficient exact real arithmetic in Coq. Logical Methods in Computer Science, 9(1), 2011."},{"key":"e_1_3_2_1_55_1","volume-title":"Masson","author":"Krivine Jean-Louis","year":"1993","unstructured":"Jean-Louis Krivine . Lambda-calculus, types and models. Ellis Horwood series in computers and their applications . Masson , 1993 . Jean-Louis Krivine. Lambda-calculus, types and models. Ellis Horwood series in computers and their applications. Masson, 1993."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70583-3_27"},{"key":"e_1_3_2_1_57_1","volume-title":"A type system for call-by-name exceptions. Logical Methods in Computer Science, 5(4)","author":"Lebresne Sylvain","year":"2009","unstructured":"Sylvain Lebresne . A type system for call-by-name exceptions. Logical Methods in Computer Science, 5(4) , 2009 . Sylvain Lebresne. A type system for call-by-name exceptions. Logical Methods in Computer Science, 5(4), 2009."},{"key":"e_1_3_2_1_58_1","volume-title":"IEEE Computer Society","author":"LICS","year":"1999","unstructured":"LICS 1999. IEEE Computer Society , 1999 . LICS 1999. IEEE Computer Society, 1999."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317775"},{"key":"e_1_3_2_1_60_1","series-title":"LIPIcs","first-page":"411","volume-title":"CSL","author":"L\u00f6sch Steffen","year":"2011","unstructured":"Steffen L\u00f6sch and Andrew M. Pitts . Relating two semantics of locally scoped names . In CSL 2011 , volume 12 of LIPIcs , pages 396\u2013 411 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011. Steffen L\u00f6sch and Andrew M. Pitts. Relating two semantics of locally scoped names. In CSL 2011, volume 12 of LIPIcs, pages 396\u2013411. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011."},{"key":"e_1_3_2_1_61_1","first-page":"173","volume-title":"Logic Colloquium \u201986","author":"Moore Gregory H.","unstructured":"Gregory H. Moore . The origins of forcing . In Logic Colloquium \u201986 , pages 143\u2013 173 . Elsevier Science Publishers B.V. (North-Holland), 1988. Gregory H. Moore. The origins of forcing. In Logic Colloquium \u201986, pages 143\u2013173. Elsevier Science Publishers B.V. (North-Holland), 1988."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1140640943"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.175187"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.04.003"},{"key":"e_1_3_2_1_65_1","series-title":"LNCS","first-page":"242","volume-title":"TACS","author":"Pitts Andrew M.","year":"2001","unstructured":"Andrew M. Pitts . Nominal logic: A first order theory of names and binding . In TACS 2001 , volume 2215 of LNCS , pages 219\u2013 242 . Springer, 2001. Andrew M. Pitts. Nominal logic: A first order theory of names and binding. In TACS 2001, volume 2215 of LNCS, pages 219\u2013242. Springer, 2001."},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706321"},{"key":"e_1_3_2_1_67_1","series-title":"LNCS","first-page":"255","volume-title":"MPC","author":"Andrew","year":"2000","unstructured":"Andrew M. Pitts and Murdoch Gabbay. A metalanguage for programming with bound names modulo renaming . In MPC 2000 , volume 1837 of LNCS , pages 230\u2013 255 . Springer, 2000. Andrew M. Pitts and Murdoch Gabbay. A metalanguage for programming with bound names modulo renaming. In MPC 2000, volume 1837 of LNCS, pages 230\u2013255. Springer, 2000."},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"crossref","unstructured":"Andrew M. Pitts and Ian D. B. Stark . Observable properties of higher order functions that dynamically create local names or what\u2019s new? In MFCS\u201993 volume 711 of LNCS pages 122\u2013 141 . Springer 1993. Andrew M. Pitts and Ian D. B. Stark. Observable properties of higher order functions that dynamically create local names or what\u2019s new? In MFCS\u201993 volume 711 of LNCS pages 122\u2013141. Springer 1993.","DOI":"10.1007\/3-540-57182-5_8"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.44"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863575"},{"key":"e_1_3_2_1_71_1","volume-title":"CCC","author":"Rahli Vincent","year":"2015","unstructured":"Vincent Rahli and Mark Bickford . Coq as a metatheory for Nuprl with bar induction . Presented at CCC 2015 , available at http:\/\/www.nup rl.org\/html\/Nuprl2Coq\/barind.pdf, 2015. Vincent Rahli and Mark Bickford. Coq as a metatheory for Nuprl with bar induction. Presented at CCC 2015, available at http:\/\/www.nup rl.org\/html\/Nuprl2Coq\/barind.pdf, 2015."},{"key":"e_1_3_2_1_72_1","volume-title":"A nominal exploration of intuitionism. Extended version avaible at http:\/\/www.nuprl.org\/html\/N uprl2Coq\/continuity-long.pdf","author":"Rahli Vincent","year":"2015","unstructured":"Vincent Rahli and Mark Bickford . A nominal exploration of intuitionism. Extended version avaible at http:\/\/www.nuprl.org\/html\/N uprl2Coq\/continuity-long.pdf , 2015 . Vincent Rahli and Mark Bickford. A nominal exploration of intuitionism. Extended version avaible at http:\/\/www.nuprl.org\/html\/N uprl2Coq\/continuity-long.pdf, 2015."},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_20"},{"issue":"12","key":"e_1_3_2_1_74_1","first-page":"2008","article-title":"Constructive set theory and brouwerian principles","volume":"11","author":"Rathjen Michael","year":"2005","unstructured":"Michael Rathjen . Constructive set theory and brouwerian principles . J. UCS , 11 ( 12 ): 2008 \u2013 2033 , 2005 . Michael Rathjen. Constructive set theory and brouwerian principles. J. UCS, 11(12):2008\u20132033, 2005.","journal-title":"J. UCS"},{"key":"e_1_3_2_1_75_1","volume-title":"Exceptions in dependent type theory. Presented at TYPES\u201914 ( http:\/\/www.pps.univ-paris-diderot.fr\/type s2014\/abstract-18.pdf)","author":"Sacchini Jorge Luis","year":"2014","unstructured":"Jorge Luis Sacchini . Exceptions in dependent type theory. Presented at TYPES\u201914 ( http:\/\/www.pps.univ-paris-diderot.fr\/type s2014\/abstract-18.pdf) , 2014 . Jorge Luis Sacchini. Exceptions in dependent type theory. Presented at TYPES\u201914 ( http:\/\/www.pps.univ-paris-diderot.fr\/type s2014\/abstract-18.pdf), 2014."},{"key":"e_1_3_2_1_77_1","series-title":"LNCS","first-page":"249","volume-title":"CSL","author":"Sch\u00f6pp Ulrich","year":"2004","unstructured":"Ulrich Sch\u00f6pp and Ian Stark . A dependent type theory with names and binding . In CSL 2004 , volume 3210 of LNCS , pages 235\u2013 249 . Springer, 2004. Ulrich Sch\u00f6pp and Ian Stark. A dependent type theory with names and binding. In CSL 2004, volume 3210 of LNCS, pages 235\u2013249. Springer, 2004."},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.040"},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/944746.944729"},{"key":"e_1_3_2_1_81_1","first-page":"1052","volume-title":"Handbook of Mathematical Logic","author":"Troelstra A.S.","unstructured":"A.S. Troelstra . Aspects of constructive mathematics . In Handbook of Mathematical Logic , pages 973\u2013 1052 . North-Holland Publishing Company, 1977. A.S. Troelstra. Aspects of constructive mathematics. In Handbook of Mathematical Logic, pages 973\u20131052. North-Holland Publishing Company, 1977."},{"key":"e_1_3_2_1_82_1","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Constructivism in Mathematics An Introduction","author":"Troelstra A.S.","year":"1988","unstructured":"A.S. Troelstra and D. van Dalen . Constructivism in Mathematics An Introduction , volume 121 of Studies in Logic and the Foundations of Mathematics . Elsevier , 1988 . A.S. Troelstra and D. van Dalen. Constructivism in Mathematics An Introduction, volume 121 of Studies in Logic and the Foundations of Mathematics. Elsevier, 1988."},{"key":"e_1_3_2_1_83_1","volume-title":"Institute for Advanced Study","author":"Foundations Program The Univalent","year":"2013","unstructured":"The Univalent Foundations Program . Homotopy Type Theory: Univalent Foundations of Mathematics. http:\/\/homotopytypetheory. org\/book , Institute for Advanced Study , 2013 . The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http:\/\/homotopytypetheory. org\/book, Institute for Advanced Study, 2013."},{"key":"e_1_3_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1182353892"},{"key":"e_1_3_2_1_85_1","series-title":"Synthese Library","first-page":"302","volume-title":"Reuniting the Antipodes Constructive and Nonstandard Views of the Continuum","author":"Veldman Wim","unstructured":"Wim Veldman . Understanding and using Brouwers continuity principle . In Reuniting the Antipodes Constructive and Nonstandard Views of the Continuum , volume 306 of Synthese Library , pages 285\u2013 302 . Springer Netherlands, 2001. Wim Veldman. Understanding and using Brouwers continuity principle. In Reuniting the Antipodes Constructive and Nonstandard Views of the Continuum, volume 306 of Synthese Library, pages 285\u2013302. Springer Netherlands, 2001."},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10699-004-3065-z"},{"key":"e_1_3_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/1577824.1577836"},{"key":"e_1_3_2_1_89_1","series-title":"LNCS","first-page":"249","volume-title":"TLCA","author":"Xu Chuangjie","year":"2013","unstructured":"Chuangjie Xu and Mart\u00b4\u0131n H\u00f6tzel Escard\u00b4o . A constructive model of uniform continuity . In TLCA 2013 , volume 7941 of LNCS , pages 236\u2013 249 . Springer, 2013. Chuangjie Xu and Mart\u00b4\u0131n H\u00f6tzel Escard\u00b4o. A constructive model of uniform continuity. In TLCA 2013, volume 7941 of LNCS, pages 236\u2013 249. Springer, 2013."}],"event":{"name":"CPP 2016: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"St. Petersburg FL USA","acronym":"CPP 2016"},"container-title":["Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2854065.2854077","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2854065.2854077","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:47Z","timestamp":1750225727000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2854065.2854077"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,18]]},"references-count":83,"alternative-id":["10.1145\/2854065.2854077","10.1145\/2854065"],"URL":"https:\/\/doi.org\/10.1145\/2854065.2854077","relation":{},"subject":[],"published":{"date-parts":[[2016,1,18]]},"assertion":[{"value":"2016-01-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}