{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,24]],"date-time":"2025-07-24T11:38:11Z","timestamp":1753357091509,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,10,8]],"date-time":"2013-10-08T00:00:00Z","timestamp":1381190400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,10,8]]},"DOI":"10.1145\/2501988.2502028","type":"proceedings-article","created":{"date-parts":[[2013,10,17]],"date-time":"2013-10-17T12:23:54Z","timestamp":1382012634000},"page":"363-372","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Crowd-scale interactive formal reasoning and analytics"],"prefix":"10.1145","author":[{"given":"Ethan","family":"Fast","sequence":"first","affiliation":[{"name":"Stanford University, Palo Alto, USA"}]},{"given":"Colleen","family":"Lee","sequence":"additional","affiliation":[{"name":"Stanford University, Palo Alto, USA"}]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[{"name":"Stanford University, Palo Alto, USA"}]},{"given":"Michael S.","family":"Bernstein","sequence":"additional","affiliation":[{"name":"Stanford University, Palo Alto, USA"}]},{"given":"Daphne","family":"Koller","sequence":"additional","affiliation":[{"name":"Stanford University, Palo Alto, USA"}]},{"given":"Eric","family":"Smith","sequence":"additional","affiliation":[{"name":"Kestrel Institute, Palo Alto, USA"}]}],"member":"320","published-online":{"date-parts":[[2013,10,8]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Coursera support documentation. http:\/\/support.coursera.org.  Coursera support documentation. http:\/\/support.coursera.org."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1745-3992.1998.tb00631.x"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1745-3984.1997.tb00512.x"},{"key":"e_1_3_2_1_4_1","volume-title":"Proc. ENTCS 2000","author":"Burstall R.","year":"2000","unstructured":"Burstall , R. Proveeasy : Helping people learn to do proofs . In Proc. ENTCS 2000 ( 2000 ), 16--32. Burstall, R. Proveeasy: Helping people learn to do proofs. In Proc. ENTCS 2000 (2000), 16--32."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0360-1315(03)00030-7"},{"key":"e_1_3_2_1_6_1","first-page":"15","article-title":"Maude as a metalanguage","volume":"1998","author":"Clavel M.","year":"1998","unstructured":"Clavel , M. , Dur\u00e1n , F. , Eker , S. , Lincoln , P. , Mart-Oliet , N. , Meseguer , J. , and Quesada , J . Maude as a metalanguage . In Proc. WRLA 1998 15 ( 1998 ). Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart-Oliet, N., Meseguer, J., and Quesada, J. Maude as a metalanguage. In Proc. WRLA 1998 15 (1998).","journal-title":"Proc. WRLA"},{"key":"e_1_3_2_1_7_1","volume-title":"Proc. UMUAI 1994","author":"Corbett A.","year":"1994","unstructured":"Corbett , A. , and Anderson , J . Knowledge tracing: Modeling the acquisition of procedural knowledge . In Proc. UMUAI 1994 ( 1994 ), 253--278. Corbett, A., and Anderson, J. Knowledge tracing: Modeling the acquisition of procedural knowledge. In Proc. UMUAI 1994 (1994), 253--278."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/365024.365111"},{"key":"e_1_3_2_1_9_1","first-page":"3","article-title":"Personalized versus collective instructor feedback in the online courseroom: Does type of feedback affect student satisfaction, academic performance and perceived connectedness with the instructor?","volume":"7","author":"Gallien T.","year":"2008","unstructured":"Gallien , T. , and Oomen-Early , J . Personalized versus collective instructor feedback in the online courseroom: Does type of feedback affect student satisfaction, academic performance and perceived connectedness with the instructor? International Journal on E-Learning 7 , 3 ( 2008 ), 463--476. Gallien, T., and Oomen-Early, J. Personalized versus collective instructor feedback in the online courseroom: Does type of feedback affect student satisfaction, academic performance and perceived connectedness with the instructor? International Journal on E-Learning 7, 3 (2008), 463--476.","journal-title":"International Journal on E-Learning"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/5254.889104"},{"key":"e_1_3_2_1_11_1","first-page":"153","article-title":"Expanding the model-tracing architecture: A 3rd generation intelligent tutor for algebra symbolization","author":"Heffernan N. T.","year":"2008","unstructured":"Heffernan , N. T. , Koedinger , K. R. , and Razzaq , L . Expanding the model-tracing architecture: A 3rd generation intelligent tutor for algebra symbolization . Int. J. Artif. Intell. Ed. ( 2008 ), 153 -- 178 . Heffernan, N. T., Koedinger, K. R., and Razzaq, L. Expanding the model-tracing architecture: A 3rd generation intelligent tutor for algebra symbolization. Int. J. Artif. Intell. Ed. (2008), 153--178.","journal-title":"Int. J. Artif. Intell. Ed. ("},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICALT.2008.224"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2441776.2441847"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622776.1622787"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588534"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1207\/s15516709cog1804_1"},{"key":"e_1_3_2_1_17_1","volume-title":"Peer and self assessment in massive online design classes. ACM TOCHI","author":"Kulkarni C.","year":"2013","unstructured":"Kulkarni , C. , Pang , K. , Le , H. , Chia , D. , Papadopoulos , K. , Cheng , J. , Koller , D. , and Klemmer , S . Peer and self assessment in massive online design classes. ACM TOCHI ( 2013 ). Kulkarni, C., Pang, K., Le, H., Chia, D., Papadopoulos, K., Cheng, J., Koller, D., and Klemmer, S. Peer and self assessment in massive online design classes. ACM TOCHI (2013)."},{"key":"e_1_3_2_1_18_1","volume-title":"Proc. UITP","author":"Lapets A.","year":"2012","unstructured":"Lapets , A. , Skowyra , R. , Bassem , C. , Kfoury , A. , and Bestavros , A . Towards an infrastructure for integrated accessible formal reasoning environments . In Proc. UITP 2012 . Lapets, A., Skowyra, R., Bassem, C., Kfoury, A., and Bestavros, A. Towards an infrastructure for integrated accessible formal reasoning environments. In Proc. UITP 2012."},{"key":"e_1_3_2_1_19_1","first-page":"81","article-title":"Rewriting logic: Roadmap and bibliography","author":"Mart-Oliet N.","year":"2001","unstructured":"Mart-Oliet , N. , and Meseguer , J . Rewriting logic: Roadmap and bibliography . J. Log. Algebr. Program. 81 ( 2001 ). Mart-Oliet, N., and Meseguer, J. Rewriting logic: Roadmap and bibliography. J. Log. Algebr. Program. 81 (2001).","journal-title":"J. Log. Algebr. Program."},{"key":"e_1_3_2_1_20_1","author":"Nielsen","year":"1993","unstructured":"Nielsen , J. Usability Engineering. Morgan Kaufmann , 1993 . Nielsen, J. Usability Engineering. Morgan Kaufmann, 1993.","journal-title":"J. Usability Engineering. Morgan Kaufmann"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_1_22_1","unstructured":"Pappano L. Massive open online courses are multiplying at a rapid pace. http:\/\/www.nytimes.com\/2012\/11\/04\/education\/edlife\/massive-open-online-courses-are-multiplying-at-a-rapid-pace.html.  Pappano L. Massive open online courses are multiplying at a rapid pace. http:\/\/www.nytimes.com\/2012\/11\/04\/education\/edlife\/massive-open-online-courses-are-multiplying-at-a-rapid-pace.html."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/645891.671440"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00248324"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13437-1_110"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/872757.872770"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/648226.749301"},{"key":"e_1_3_2_1_28_1","first-page":"29","article-title":"Student use of an interactive theorem prover","author":"Suppes P","year":"1984","unstructured":"Suppes , P . Student use of an interactive theorem prover . Contemporary Mathematics 29 ( 1984 ). Suppes, P. Student use of an interactive theorem prover. Contemporary Mathematics 29 (1984).","journal-title":"Contemporary Mathematics"},{"key":"e_1_3_2_1_29_1","first-page":"176","article-title":"Trust-based peer assessment for virtual learning systems","volume":"2010","author":"Tosic M.","year":"2010","unstructured":"Tosic , M. , and Nejkovic , V . Trust-based peer assessment for virtual learning systems . In Proc. SocInfo 2010 ( 2010 ), 176 -- 191 . Tosic, M., and Nejkovic, V. Trust-based peer assessment for virtual learning systems. In Proc. SocInfo 2010 (2010), 176--191.","journal-title":"Proc. SocInfo"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1080\/00461520.2011.611369"},{"key":"e_1_3_2_1_31_1","volume-title":"CEUR Workshop Proceedings","author":"Windsteiger W.","year":"2012","unstructured":"Windsteiger , W. Theorema 2. 0 : A graphical user interface for a mathematical assistant system . CEUR Workshop Proceedings ( 2012 ), 73--81. Windsteiger, W. Theorema 2.0: A graphical user interface for a mathematical assistant system. CEUR Workshop Proceedings (2012), 73--81."}],"event":{"name":"UIST'13: The 26th Annual ACM Symposium on User Interface Software and Technology","sponsor":["SIGGRAPH ACM Special Interest Group on Computer Graphics and Interactive Techniques","SIGCHI ACM Special Interest Group on Computer-Human Interaction"],"location":"St. Andrews Scotland, United Kingdom","acronym":"UIST'13"},"container-title":["Proceedings of the 26th annual ACM symposium on User interface software and technology"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2501988.2502028","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2501988.2502028","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:46Z","timestamp":1750231726000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2501988.2502028"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,10,8]]},"references-count":31,"alternative-id":["10.1145\/2501988.2502028","10.1145\/2501988"],"URL":"https:\/\/doi.org\/10.1145\/2501988.2502028","relation":{},"subject":[],"published":{"date-parts":[[2013,10,8]]},"assertion":[{"value":"2013-10-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}