{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:14Z","timestamp":1775790794265,"version":"3.50.1"},"reference-count":102,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2019,4,24]],"date-time":"2019-04-24T00:00:00Z","timestamp":1556064000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Eric and Wendy Schmidt Postdoctoral Award program for Women in Mathematical and Computing Sciences"},{"DOI":"10.13039\/501100001866","name":"Fonds National de la Recherche Luxembourg","doi-asserted-by":"crossref","award":["FNR\/P14\/814912"],"award-info":[{"award-number":["FNR\/P14\/814912"]}],"id":[{"id":"10.13039\/501100001866","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Weizmann Institute of Science -- National Postdoctoral Award program for Advancing Women in Science"},{"name":"Fulbright Post-doctoral Scholar program"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2019,4,30]]},"abstract":"<jats:p>Powerful yet effective induction principles play an important role in computing, being a paramount component of programming languages, automated reasoning, and program verification systems. The Bar Induction (BI) principle is a fundamental concept of intuitionism, which is equivalent to the standard principle of transfinite induction. In this work, we investigate the compatibility of several variants of BI with Constructive Type Theory (CTT), a dependent type theory in the spirit of Martin-L\u00f6f\u2019s extensional theory. We first show that CTT is compatible with a BI principle for sequences of numbers. Then, we establish the compatibility of CTT with a more general BI principle for sequences of name-free closed terms. The formalization of the latter principle within the theory involved enriching CTT\u2019s term syntax with a limit constructor and showing that consistency is preserved. Furthermore, we provide novel insights regarding BI, such as the non-truncated version of BI on monotone bars being intuitionistically false. These enhancements are carried out formally using the Nuprl proof assistant that implements CTT and the formalization of CTT within the Coq proof assistant presented in previous works.<\/jats:p>","DOI":"10.1145\/3305261","type":"journal-article","created":{"date-parts":[[2019,4,26]],"date-time":"2019-04-26T12:23:24Z","timestamp":1556281404000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Bar Induction is Compatible with Constructive Type Theory"],"prefix":"10.1145","volume":"66","author":[{"given":"Vincent","family":"Rahli","sequence":"first","affiliation":[{"name":"SnT, University of Luxembourg, Luxembourg"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Bickford","sequence":"additional","affiliation":[{"name":"Cornell University, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Liron","family":"Cohen","sequence":"additional","affiliation":[{"name":"Cornell University, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert L.","family":"Constable","sequence":"additional","affiliation":[{"name":"Cornell University, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,4,24]]},"reference":[{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"e_1_2_1_3_1","volume-title":"Retrieved","author":"Wiki Agda","year":"2018","unstructured":"Agda Wiki . 2018 . Agda . Retrieved February 13, 2019 from http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php. Agda Wiki. 2018. Agda. Retrieved February 13, 2019 from http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php."},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 2nd Annual IEEE Symposium on Logic in Computer Science (LICS\u201987)","author":"Allen Stuart F.","year":"1987","unstructured":"Stuart F. Allen . 1987 . A non-type-theoretic definition of Martin-L\u00f6f\u2019s types . In Proceedings of the 2nd Annual IEEE Symposium on Logic in Computer Science (LICS\u201987) . IEEE, Los Alamitos, CA, 215--221. Stuart F. Allen. 1987. A non-type-theoretic definition of Martin-L\u00f6f\u2019s types. In Proceedings of the 2nd Annual IEEE Symposium on Logic in Computer Science (LICS\u201987). IEEE, Los Alamitos, CA, 215--221."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.10.005"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Thorsten Altenkirch Neil Ghani Peter Hancock Conor McBride and Peter Morris. 2015. Indexed Container. J. Funct. Program. 25 (2015).  Thorsten Altenkirch Neil Ghani Peter Hancock Conor McBride and Peter Morris. 2015. Indexed Container. J. Funct. Program. 25 (2015).","DOI":"10.1017\/S095679681500009X"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the TYPES 2014 Conference.","author":"Anand Abhishek","year":"2014","unstructured":"Abhishek Anand , Mark Bickford , Robert L. Constable , and Vincent Rahli . 2014 . A type theory with partial equivalence relations as types . In Proceedings of the TYPES 2014 Conference. Abhishek Anand, Mark Bickford, Robert L. Constable, and Vincent Rahli. 2014. A type theory with partial equivalence relations as types. In Proceedings of the TYPES 2014 Conference."},{"key":"e_1_2_1_10_1","series-title":"Lecture Notes in Computer Science","volume-title":"Interactive Theorem Proving","author":"Anand Abhishek","unstructured":"Abhishek Anand and Vincent Rahli . 2014. Towards a formally verified proof assistant . In Interactive Theorem Proving . Lecture Notes in Computer Science , Vol. 8558 . Springer , 27--44. Abhishek Anand and Vincent Rahli. 2014. Towards a formally verified proof assistant. In Interactive Theorem Proving. Lecture Notes in Computer Science, Vol. 8558. Springer, 27--44."},{"key":"e_1_2_1_11_1","unstructured":"Mark van Atten. 2004. On Brouwer. Cengage Learning.  Mark van Atten. 2004. On Brouwer. Cengage Learning."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1182353892"},{"key":"e_1_2_1_13_1","volume-title":"Foundations of Constructive Mathematics","author":"Beeson Michael J.","unstructured":"Michael J. Beeson . 1985. Foundations of Constructive Mathematics . Springer . Michael J. Beeson. 1985. Foundations of Constructive Mathematics. Springer."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586854"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11494645_3"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200410038"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005093"},{"key":"e_1_2_1_18_1","volume-title":"Interactive Theorem Proving and Program Development","author":"Bertot Yves","unstructured":"Yves Bertot and Pierre Casteran . 2004. Interactive Theorem Proving and Program Development . Springer-Verlag . http:\/\/www.labri.fr\/perso\/casteran\/CoqArt. Yves Bertot and Pierre Casteran. 2004. Interactive Theorem Proving and Program Development. Springer-Verlag. http:\/\/www.labri.fr\/perso\/casteran\/CoqArt."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01620763"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_7"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the TYPES 2014 Conference. http:\/\/nuprl.org\/KB\/show.php?ID&equals;723","author":"Bickford Mark","year":"2014","unstructured":"Mark Bickford and Robert Constable . 2014 . Inductive construction in Nuprl type theory using bar induction . In Proceedings of the TYPES 2014 Conference. http:\/\/nuprl.org\/KB\/show.php?ID&equals;723 . Mark Bickford and Robert Constable. 2014. Inductive construction in Nuprl type theory using bar induction. In Proceedings of the TYPES 2014 Conference. http:\/\/nuprl.org\/KB\/show.php?ID&equals;723."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005066"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934511"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929529.1929536"},{"key":"e_1_2_1_26_1","volume-title":"One Hundred Years of Intuitionism","author":"Bridges Douglas","unstructured":"Douglas Bridges . 2008. A reverse look at Brouwer\u2019s fan theorem . In One Hundred Years of Intuitionism , M. van Atten, P. Boldini, M. Bourdeau, and G. Heinzmann (Eds.). Birkh\u00e4user , 316--325. Douglas Bridges. 2008. A reverse look at Brouwer\u2019s fan theorem. In One Hundred Years of Intuitionism, M. van Atten, P. Boldini, M. Bourdeau, and G. Heinzmann (Eds.). Birkh\u00e4user, 316--325."},{"key":"e_1_2_1_27_1","volume-title":"Varieties of Constructive Mathematics","author":"Bridges Douglas","unstructured":"Douglas Bridges and Fred Richman . 1987. Varieties of Constructive Mathematics . Cambridge University Press . http:\/\/books.google.com\/books?id&equals;oN5nsPkXhhsC. Douglas Bridges and Fred Richman. 1987. Varieties of Constructive Mathematics. Cambridge University Press. http:\/\/books.google.com\/books?id&equals;oN5nsPkXhhsC."},{"key":"e_1_2_1_28_1","volume-title":"Brouwer\u2019s Cambridge Lectures on Intuitionism","author":"Brouwer L. E. J.","unstructured":"L. E. J. Brouwer . 1981. Brouwer\u2019s Cambridge Lectures on Intuitionism . Cambridge University Press . L. E. J. Brouwer. 1981. Brouwer\u2019s Cambridge Lectures on Intuitionism. Cambridge University Press."},{"key":"e_1_2_1_29_1","volume-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic","author":"Brouwer L. E. J.","year":"1879","unstructured":"L. E. J. Brouwer . 1927. On the domains of definition of functions . In From Frege to G\u00f6del: A Source Book in Mathematical Logic , 1879 --1931. Harvard University Press , Cambridge, MA , 446--463. L. E. J. Brouwer. 1927. On the domains of definition of functions. In From Frege to G\u00f6del: A Source Book in Mathematical Logic, 1879--1931. Harvard University Press, Cambridge, MA, 446--463."},{"key":"e_1_2_1_30_1","first-page":"3","article-title":"Historical background, principles and methods of intuitionism","volume":"49","author":"Brouwer L. E. J.","year":"1952","unstructured":"L. E. J. Brouwer . 1952 . Historical background, principles and methods of intuitionism . South African Journal of Science 49 , 3 -- 4 (1952), 139--146. http:\/\/reference.sabinet.co.za\/webx\/access\/journal_archive\/00382353\/3884.pdf. L. E. J. Brouwer. 1952. Historical background, principles and methods of intuitionism. South African Journal of Science 49, 3--4 (1952), 139--146. http:\/\/reference.sabinet.co.za\/webx\/access\/journal_archive\/00382353\/3884.pdf.","journal-title":"South African Journal of Science"},{"key":"e_1_2_1_31_1","unstructured":"Venanzio Capretta. 2004. A polymorphic representation of induction-recursion. www.cs.ru.nl\/venanzio\/publications\/induction_recursion.ps.  Venanzio Capretta. 2004. A polymorphic representation of induction-recursion. www.cs.ru.nl\/venanzio\/publications\/induction_recursion.ps."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.50.6.1143"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.51.1.105"},{"key":"e_1_2_1_34_1","series-title":"Lecture Notes in Computer Science","volume-title":"Fundamentals of Computation Theory","author":"Constable Robert L.","unstructured":"Robert L. Constable . 1983. Constructive mathematics as a programming logic I: Some principles of theory . In Fundamentals of Computation Theory . Lecture Notes in Computer Science , Vol. 158 . Springer , 64--77. Robert L. Constable. 1983. Constructive mathematics as a programming logic I: Some principles of theory. In Fundamentals of Computation Theory. Lecture Notes in Computer Science, Vol. 158. Springer, 64--77."},{"key":"e_1_2_1_35_1","unstructured":"R. L. Constable S. F. Allen M. Bromley R. Cleaveland J. F. Cremer R. W. Harper etal 1986. Implementing Mathematics With the Nuprl Proof Development System. Prentice Hall Upper Saddle River NJ.   R. L. Constable S. F. Allen M. Bromley R. Cleaveland J. F. Cremer R. W. Harper et al. 1986. Implementing Mathematics With the Nuprl Proof Development System. Prentice Hall Upper Saddle River NJ."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90085-8"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD\u201916)","author":"Coquand Thierry","year":"2016","unstructured":"Thierry Coquand and Bassel Mannaa . 2016 . The independence of Markov\u2019s principle in type theory . In Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD\u201916) . Thierry Coquand and Bassel Mannaa. 2016. The independence of Markov\u2019s principle in type theory. In Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD\u201916)."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005130"},{"key":"e_1_2_1_39_1","volume-title":"Retrieved","year":"2019","unstructured":"Coq. n.d. The Coq Proof Assistant . Retrieved February 13, 2019 from http:\/\/coq.inria.fr\/. Coq. n.d. The Coq Proof Assistant. Retrieved February 13, 2019 from http:\/\/coq.inria.fr\/."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.2307\/2272124"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(84)90035-6"},{"key":"e_1_2_1_43_1","volume-title":"Elements of Intuitionism","author":"Dummett Michael A. E.","unstructured":"Michael A. E. Dummett . 2000. Elements of Intuitionism ( 2 nd ed.). Clarendon Press . Michael A. E. Dummett. 2000. Elements of Intuitionism (2nd ed.). Clarendon Press.","edition":"2"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(02)00096-9"},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications (TLCA\u201915)","author":"Mart\u00edn","unstructured":"Mart\u00edn H. Escard\u00f3 and Chuangjie Xu. 2015. The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation . In Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications (TLCA\u201915) . 153--164. Mart\u00edn H. Escard\u00f3 and Chuangjie Xu. 2015. The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation. In Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications (TLCA\u201915). 153--164."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1017\/jsl.2014.82"},{"key":"e_1_2_1_47_1","volume-title":"Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation. 653--669","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan (Newman) Wu , Jieung Kim , Vilhelm Sj\u00f6berg , 2016 . CertiKOS: An extensible architecture for building certified concurrent OS kernels . In Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation. 653--669 . https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, et al. 2016. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation. 653--669. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu."},{"key":"e_1_2_1_49_1","first-page":"107","article-title":"Functional interpretation of bar induction by bar recursion","volume":"20","author":"Howard William A.","year":"1968","unstructured":"William A. Howard . 1968 . Functional interpretation of bar induction by bar recursion . Compositio Mathematica 20 (1968), 107 -- 124 . http:\/\/eudml.org\/doc\/88970 William A. Howard. 1968. Functional interpretation of bar induction by bar recursion. Compositio Mathematica 20 (1968), 107--124. http:\/\/eudml.org\/doc\/88970","journal-title":"Compositio Mathematica"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.2307\/2270450"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77371"},{"key":"e_1_2_1_52_1","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics","author":"Howe Douglas J.","unstructured":"Douglas J. Howe . 1996. Importing mathematics from HOL into Nuprl . In Theorem Proving in Higher Order Logics . Lecture Notes in Computer Science , Vol. 1125 . Springer , 267--282. Douglas J. Howe. 1996. Importing mathematics from HOL into Nuprl. In Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, Vol. 1125. Springer, 267--282."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151641"},{"key":"e_1_2_1_54_1","series-title":"Lecture Notes in Computer Science","volume-title":"Algebraic Methodology and Software Technology","author":"Howe Douglas J.","unstructured":"Douglas J. Howe . 1996. Semantic foundations for embedding HOL in Nuprl . In Algebraic Methodology and Software Technology . Lecture Notes in Computer Science , Vol. 1101 . Springer , 85--101. Douglas J. Howe. 1996. Semantic foundations for embedding HOL in Nuprl. In Algebraic Methodology and Software Technology. Lecture Notes in Computer Science, Vol. 1101. Springer, 85--101."},{"key":"e_1_2_1_55_1","volume-title":"Counterexamples in intuitionistic analysis using Kripke\u2019s schema. Mathematical Logic Quarterly 15, 1618","author":"Hull Richard G.","year":"1969","unstructured":"Richard G. Hull . 1969. Counterexamples in intuitionistic analysis using Kripke\u2019s schema. Mathematical Logic Quarterly 15, 1618 ( 1969 ), 241--246. Richard G. Hull. 1969. Counterexamples in intuitionistic analysis using Kripke\u2019s schema. Mathematical Logic Quarterly 15, 1618 (1969), 241--246."},{"key":"e_1_2_1_56_1","volume-title":"n.d. Overview. Retrieved","year":"2019","unstructured":"Idris. n.d. Overview. Retrieved February 19, 2019 from http:\/\/www.idris-lang.org\/. Idris. n.d. Overview. Retrieved February 19, 2019 from http:\/\/www.idris-lang.org\/."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19900360307"},{"key":"e_1_2_1_58_1","volume-title":"Reverse mathematics in Bishop\u2019s constructive mathematics. Philosophia Scienti\u00e6 CS6","author":"Ishihara Hajime","year":"2006","unstructured":"Hajime Ishihara . 2006. Reverse mathematics in Bishop\u2019s constructive mathematics. Philosophia Scienti\u00e6 CS6 ( 2006 ), 43--59. Hajime Ishihara. 2006. Reverse mathematics in Bishop\u2019s constructive mathematics. Philosophia Scienti\u00e6 CS6 (2006), 43--59."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1153858649"},{"key":"e_1_2_1_60_1","volume-title":"Vesley","author":"Kleene Stephen C.","year":"1965","unstructured":"Stephen C. Kleene and Richard E . Vesley . 1965 . The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions. North-Holland Publishing Company . Stephen C. Kleene and Richard E. Vesley. 1965. The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions. North-Holland Publishing Company."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_63_1","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Science Logic","author":"Kopylov Alexei","unstructured":"Alexei Kopylov and Aleksey Nogin . 2001. Markov\u2019s principle for propositional type theory . In Computer Science Logic . Lecture Notes in Computer Science , Vol. 2142 . Springer , 570--584. Alexei Kopylov and Aleksey Nogin. 2001. Markov\u2019s principle for propositional type theory. In Computer Science Logic. Lecture Notes in Computer Science, Vol. 2142. Springer, 570--584."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.2307\/2964012"},{"key":"e_1_2_1_65_1","first-page":"222","article-title":"Lawless sequences of natural numbers","volume":"20","author":"Kreisel Georg","year":"1968","unstructured":"Georg Kreisel . 1968 . Lawless sequences of natural numbers . Compositio Mathematica 20 (1968), 222 -- 248 . http:\/\/eudml.org\/doc\/88982 Georg Kreisel. 1968. Lawless sequences of natural numbers. Compositio Mathematica 20 (1968), 222--248. http:\/\/eudml.org\/doc\/88982","journal-title":"Compositio Mathematica"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.2307\/2964110"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(70)90001-X"},{"key":"e_1_2_1_68_1","volume-title":"Formal Systems and Recursive Functions. Studies in Logic and the Foundations of Mathematics","author":"Kripke Saul A.","unstructured":"Saul A. Kripke . 1965. Semantical analysis of intuitionistic logic I . In Formal Systems and Recursive Functions. Studies in Logic and the Foundations of Mathematics , Vol. 40 . Elsevier , 92--130. Saul A. Kripke. 1965. Semantical analysis of intuitionistic logic I. In Formal Systems and Recursive Functions. Studies in Logic and the Foundations of Mathematics, Vol. 40. Elsevier, 92--130."},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_1_70_1","volume-title":"Proceedings of the 6th International Congress for Logic, Methodology, and Philosophy of Science. 153--175","year":"1982","unstructured":"Martin-L\u00f6f. 1982 . Constructive mathematics and computer programming . In Proceedings of the 6th International Congress for Logic, Methodology, and Philosophy of Science. 153--175 . Martin-L\u00f6f. 1982. Constructive mathematics and computer programming. In Proceedings of the 6th International Congress for Logic, Methodology, and Philosophy of Science. 153--175."},{"key":"e_1_2_1_71_1","unstructured":"Per Martin-L\u00f6f. 1984. Intuitionistic Type Theory. Number 1 in Studies in Proof Theory Lecture Notes. Bibliopolis Napoli Italy.  Per Martin-L\u00f6f. 1984. Intuitionistic Type Theory. Number 1 in Studies in Proof Theory Lecture Notes. Bibliopolis Napoli Italy."},{"key":"e_1_2_1_73_1","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction\u2014CADE-25","author":"de Moura Leonardo Mendon\u00e7a","unstructured":"Leonardo Mendon\u00e7a de Moura , Soonho Kong , Jeremy Avigad , Floris van Doorn , and Jakob von Raumer . 2015. The lean theorem prover (system description) . In Automated Deduction\u2014CADE-25 . Lecture Notes in Computer Science , Vol. 9195 . Springer , 378--388. Leonardo Mendon\u00e7a de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The lean theorem prover (system description). In Automated Deduction\u2014CADE-25. Lecture Notes in Computer Science, Vol. 9195. Springer, 378--388."},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71193-5"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70747-X"},{"key":"e_1_2_1_76_1","first-page":"280","article-title":"Notes towards an axiomatization of intuitionistic analysis","volume":"9","author":"Myhill John","year":"1967","unstructured":"John Myhill . 1967 . Notes towards an axiomatization of intuitionistic analysis . Logique et Analyse 9 (1967), 280 -- 297 . John Myhill. 1967. Notes towards an axiomatization of intuitionistic analysis. Logique et Analyse 9 (1967), 280--297.","journal-title":"Logique et Analyse"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.05.041"},{"key":"e_1_2_1_78_1","volume-title":"Smith","author":"Nordstr\u00f6m Bengt","year":"1990","unstructured":"Bengt Nordstr\u00f6m , Kent Petersson , and Jan M . Smith . 1990 . Programming in Martin-L\u00f6f\u2019s Type Theory: An Introduction. Clarendon Press , New York, NY. Bengt Nordstr\u00f6m, Kent Petersson, and Jan M. Smith. 1990. Programming in Martin-L\u00f6f\u2019s Type Theory: An Introduction. Clarendon Press, New York, NY."},{"key":"e_1_2_1_79_1","volume-title":"Retrieved","year":"2019","unstructured":"Github. 2019 . Nuprl in Coq . Retrieved February 19, 2019 from https:\/\/github.com\/vrahli\/NuprlInCoq. Github. 2019. Nuprl in Coq. Retrieved February 19, 2019 from https:\/\/github.com\/vrahli\/NuprlInCoq."},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/11780342_44"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.201100106"},{"key":"e_1_2_1_82_1","series-title":"Lecture Notes in Computer Science","volume-title":"Typed Lambda Calculi and Applications","author":"Paulin-Mohring Christine","unstructured":"Christine Paulin-Mohring . 1993. Inductive definitions in the system Coq rules and properties . In Typed Lambda Calculi and Applications . Lecture Notes in Computer Science , Vol. 664 . Springer , 328--345. Christine Paulin-Mohring. 1993. Inductive definitions in the system Coq rules and properties. In Typed Lambda Calculi and Applications. Lecture Notes in Computer Science, Vol. 664. Springer, 328--345."},{"key":"e_1_2_1_83_1","series-title":"Lecture Notes in Computer Science","volume-title":"Theoretical Aspects of Computer Software","author":"Pitts Andrew M.","unstructured":"Andrew M. Pitts . 2001. Nominal logic: A first order theory of names and binding . In Theoretical Aspects of Computer Software . Lecture Notes in Computer Science , Vol. 2215 . Springer , 219--242. Andrew M. Pitts. 2001. Nominal logic: A first order theory of names and binding. In Theoretical Aspects of Computer Software. Lecture Notes in Computer Science, Vol. 2215. Springer, 219--242."},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-42432-3_3"},{"key":"e_1_2_1_86_1","volume-title":"Retrieved","author":"Rahli Vincent","year":"2015","unstructured":"Vincent Rahli and Mark Bickford . 2015 . A Nominal Exploration of Intuitionism. Extended version of CPP 2016 paper . Retrieved February 19, 2019 from http:\/\/www.nuprl.org\/html\/Nuprl2Coq\/continuity-long.pdf. Vincent Rahli and Mark Bickford. 2015. A Nominal Exploration of Intuitionism. Extended version of CPP 2016 paper. Retrieved February 19, 2019 from http:\/\/www.nuprl.org\/html\/Nuprl2Coq\/continuity-long.pdf."},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854077"},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000172"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_20"},{"key":"e_1_2_1_90_1","volume-title":"Proceedings of the 2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS\u201917)","author":"Rahli Vincent","unstructured":"Vincent Rahli , Mark Bickford , and Robert L. Constable . 2017. Bar induction: The good, the bad, and the ugly . In Proceedings of the 2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS\u201917) . IEEE, Los Alamitos, CA, 1--12. Extended version available at https:\/\/vrahli.github.io\/articles\/bar-induction-lics-long.pdf. Vincent Rahli, Mark Bickford, and Robert L. Constable. 2017. Bar induction: The good, the bad, and the ugly. In Proceedings of the 2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS\u201917). IEEE, Los Alamitos, CA, 1--12. Extended version available at https:\/\/vrahli.github.io\/articles\/bar-induction-lics-long.pdf."},{"key":"e_1_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200510030"},{"key":"e_1_2_1_92_1","first-page":"2008","article-title":"Constructive set theory and Brouwerian principles","volume":"11","author":"Rathjen Michael","year":"2005","unstructured":"Michael Rathjen . 2005 . Constructive set theory and Brouwerian principles . Journal of Universal Computer Science 11 , 12 (2005), 2008 -- 2033 . Michael Rathjen. 2005. Constructive set theory and Brouwerian principles. Journal of Universal Computer Science 11, 12 (2005), 2008--2033.","journal-title":"Journal of Universal Computer Science"},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.2307\/2274713"},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273126"},{"key":"e_1_2_1_95_1","volume-title":"Subsystems of Second Order Arithmetic","author":"Simpson Stephen G.","unstructured":"Stephen G. Simpson . 2006. Subsystems of Second Order Arithmetic ( 2 nd ed.). Cambridge University Press . Stephen G. Simpson. 2006. Subsystems of Second Order Arithmetic (2nd ed.). Cambridge University Press.","edition":"2"},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.1090\/pspum\/005\/0154801"},{"key":"e_1_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(77)90060-9"},{"key":"e_1_2_1_99_1","volume-title":"Choice Sequences: A","author":"Troelstra A. S.","year":"1977","unstructured":"A. S. Troelstra . 1977 . Choice Sequences: A Chapter of Intuitionistic Mathematics. Clarendon Press . A. S. Troelstra. 1977. Choice Sequences: A Chapter of Intuitionistic Mathematics. Clarendon Press."},{"key":"e_1_2_1_100_1","volume-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis","author":"Troelstra A. S.","unstructured":"A. S. Troelstra . 1973. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis . Springer , New York, NY . A. S. Troelstra. 1973. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Springer, New York, NY."},{"key":"e_1_2_1_101_1","doi-asserted-by":"publisher","DOI":"10.4064\/fm-82-4-307-322"},{"key":"e_1_2_1_102_1","volume-title":"Troelstra and Dirk van Dalen","author":"Anne","year":"1988","unstructured":"Anne S. Troelstra and Dirk van Dalen . 1988 . Constructivism in Mathematics An Introduction. Studies in Logic and the Foundations of Mathematics, Vol. 121 . Elsevier . Anne S. Troelstra and Dirk van Dalen. 1988. Constructivism in Mathematics An Introduction. Studies in Logic and the Foundations of Mathematics, Vol. 121. Elsevier."},{"key":"e_1_2_1_103_1","unstructured":"2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Univalent Foundations Program. http:\/\/homotopytypetheory.org\/book.  2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Univalent Foundations Program. http:\/\/homotopytypetheory.org\/book."},{"key":"e_1_2_1_104_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-014-0384-9"},{"key":"e_1_2_1_105_1","volume-title":"Brouwer\u2019s real thesis on bars. Philosophia Scienti\u00e6 CS6","author":"Veldman Wim","year":"2006","unstructured":"Wim Veldman . 2006. Brouwer\u2019s real thesis on bars. Philosophia Scienti\u00e6 CS6 ( 2006 ), 21--42. Wim Veldman. 2006. Brouwer\u2019s real thesis on bars. Philosophia Scienti\u00e6 CS6 (2006), 21--42."},{"key":"e_1_2_1_106_1","volume-title":"One Hundred Years of Intuitionism","author":"Veldman Wim","unstructured":"Wim Veldman . 2008. Some applications of Brouwer\u2019s thesis on bars . In One Hundred Years of Intuitionism , M. van Atten, P. Boldini, M. Bourdeau, and G. Heinzmann (Eds.). Birkh\u00e4user , 326--340. Wim Veldman. 2008. Some applications of Brouwer\u2019s thesis on bars. In One Hundred Years of Intuitionism, M. van Atten, P. Boldini, M. Bourdeau, and G. Heinzmann (Eds.). Birkh\u00e4user, 326--340."},{"key":"e_1_2_1_107_1","volume-title":"Reuniting the Antipodes\u2014Constructive and Nonstandard Views of the Continuum","author":"Veldman Wim","unstructured":"Wim Veldman . 2001. Understanding and using Brouwer\u2019s continuity principle . In Reuniting the Antipodes\u2014Constructive and Nonstandard Views of the Continuum . Synthese Library, Vol . 306. Springer Netherlands , 285--302. Wim Veldman. 2001. Understanding and using Brouwer\u2019s continuity principle. In Reuniting the Antipodes\u2014Constructive and Nonstandard Views of the Continuum. Synthese Library, Vol. 306. Springer Netherlands, 285--302."},{"key":"e_1_2_1_108_1","doi-asserted-by":"publisher","DOI":"10.1112\/jlms\/s2-47.2.193"},{"key":"e_1_2_1_109_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)00047-6"},{"key":"e_1_2_1_110_1","series-title":"Lecture Notes in Computer Science","volume-title":"Interactive Theorem Proving","author":"Vytiniotis Dimitrios","unstructured":"Dimitrios Vytiniotis , Thierry Coquand , and David Wahlstedt . 2012. Stop when you are almost-full\u2014Adventures in constructive termination . In Interactive Theorem Proving . Lecture Notes in Computer Science , Vol. 7406 . Springer , 250--265. Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt. 2012. Stop when you are almost-full\u2014Adventures in constructive termination. In Interactive Theorem Proving. Lecture Notes in Computer Science, Vol. 7406. Springer, 250--265."},{"key":"e_1_2_1_111_1","series-title":"Lecture Notes in Computer Science","volume-title":"Typed Lambda Calculi and Applications","author":"Xu Chuangjie","unstructured":"Chuangjie Xu and Mart\u00edn H\u00f6tzel Escard\u00f3 . 2013. A constructive model of uniform continuity . In Typed Lambda Calculi and Applications . Lecture Notes in Computer Science , Vol. 7941 . Springer , 236--249. Chuangjie Xu and Mart\u00edn H\u00f6tzel Escard\u00f3. 2013. A constructive model of uniform continuity. In Typed Lambda Calculi and Applications. Lecture Notes in Computer Science, Vol. 7941. Springer, 236--249."}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3305261","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3305261","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:09Z","timestamp":1750208289000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3305261"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4,24]]},"references-count":102,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,4,30]]}},"alternative-id":["10.1145\/3305261"],"URL":"https:\/\/doi.org\/10.1145\/3305261","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,4,24]]},"assertion":[{"value":"2018-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-04-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}