{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,12]],"date-time":"2024-04-12T00:30:09Z","timestamp":1712881809863},"reference-count":19,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.400.7","type":"journal-article","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T11:52:49Z","timestamp":1712231569000},"page":"96-119","source":"Crossref","is-referenced-by-count":0,"title":["Waterproof: Educational Software for Learning How to Write Mathematical Proofs"],"prefix":"10.4204","volume":"400","author":[{"given":"Jelle","family":"Wemmenhove","sequence":"first","affiliation":[]},{"given":"Dick","family":"Arends","sequence":"additional","affiliation":[]},{"given":"Thijs","family":"Beurskens","sequence":"additional","affiliation":[]},{"given":"Maitreyee","family":"Bhaid","sequence":"additional","affiliation":[]},{"given":"Sean","family":"McCarren","sequence":"additional","affiliation":[]},{"given":"Jan","family":"Moraal","sequence":"additional","affiliation":[]},{"given":"Diego","family":"Rivera Garrido","sequence":"additional","affiliation":[]},{"given":"David","family":"Tuin","sequence":"additional","affiliation":[]},{"given":"Malcolm","family":"Vassallo","sequence":"additional","affiliation":[]},{"given":"Pieter","family":"Wils","sequence":"additional","affiliation":[]},{"given":"Jim","family":"Portegies","sequence":"additional","affiliation":[]}],"member":"2720","published-online":{"date-parts":[[2024,4,6]]},"reference":[{"key":"mizar","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-319-20615-8_17","article-title":"Mizar: State-of-the-art and Beyond","volume-title":"Intelligent Computer Mathematics","author":"Bancerek","year":"2015"},{"key":"hott-lib","series-title":"CPP 2017","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018615","article-title":"The HoTT Library: A Formalization of Homotopy Type Theory in Coq","volume-title":"Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs","author":"Bauer","year":"2017"},{"key":"Bohne-three-steps","series-title":"Electronic Proceedings in Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4204\/EPTCS.267.1","article-title":"Learning how to Prove: From the Coq Proof Assistant to Textbook Style","volume-title":"Proceedings 6th International Workshop on Theorem proving components for Educational software, Gothenburg, Sweden, 6 Aug 2017","volume":"267","author":"B\u00f6hne","year":"2018"},{"key":"diproche-1","series-title":"Electronic Proceedings in Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.4204\/EPTCS.328.4","article-title":"Number Theory and Axiomatic Geometry in the Diproche System","volume-title":"Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, Paris, France, 29th June 2020","volume":"328","author":"Carl","year":"2020"},{"key":"diproche-2","series-title":"Electronic Proceedings in Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.4204\/EPTCS.354.5","article-title":"Natural Language Proof Checking in Introduction to Proof Classes - First Experiences with Diproche","volume-title":"Proceedings 10th International Workshop on Theorem Proving Components for Educational Software, (Remote) Carnegie Mellon University, Pittsburgh, PA, United States, 11 July 2021","volume":"354","author":"Carl","year":"2022"},{"key":"Lurch","first-page":"299","article-title":"From Formal to Expository: Using the Proof-Checking Word Processor Lurch to Teach Proof Writing","volume-title":"Beyond Lecture: Resources and Pedagogical Techniques for Enhancing the Teaching of Proof-Writing Across the Curriculum","author":"Carter","year":"2016"},{"key":"jsCoq","series-title":"Electronic Proceedings in Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.4204\/EPTCS.239.2","article-title":"jsCoq: Towards Hybrid Theorem Proving Interfaces","volume-title":"Proceedings of the 12th Workshop on User Interfaces for Theorem Provers, Coimbra, Portugal, 2nd July 2016","volume":"239","author":"Gallego Arias","year":"2017"},{"key":"Martin-Aquinas","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-25379-9_16","article-title":"Teaching Experience: Logic and Formal Methods with Coq","volume-title":"Certified Programs and Proofs","author":"Henz","year":"2011"},{"key":"french-experience-proof-assistants","first-page":"35","article-title":"Utilisation des assistants de preuves pour l\u2019enseignement en L1: Retours d'exp\u00e9riences.","volume":"174","author":"Kerjean","year":"2022","journal-title":"La Gazette de la Soci\u00e9t\u00e9 Math\u00e9matique de France"},{"key":"Bohne-evidence","series-title":"ICER '17","doi-asserted-by":"publisher","DOI":"10.1145\/3105726.3106184","article-title":"Theorem Provers as a Learning Tool in Theory of Computation","volume-title":"Proceedings of the 2017 ACM Conference on International Computing Education Research","author":"Knobelsdorf","year":"2017"},{"issue":"2","key":"Femke-and-Wiedijk","first-page":"35","article-title":"Teaching logic using a state-of-art proof assistant","volume":"3","author":"Maxim","year":"2010","journal-title":"Acta Didactica Napocensia"},{"issue":"3","key":"Moore1994","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/BF01273731","article-title":"Making the transition to formal proof","volume":"27","author":"Moore","year":"1994","journal-title":"Educational Studies in Mathematics"},{"key":"lean","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","article-title":"The Lean Theorem Prover (System Description)","volume-title":"Automated Deduction - CADE-25","author":"de Moura","year":"2015"},{"key":"Nipkow-VMCAI12","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-27940-9_3","article-title":"Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Nipkow","year":"2012"},{"key":"isabelle","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","volume":"2283","author":"Nipkow","year":"2002"},{"key":"mizar-history","first-page":"35","article-title":"Mizar as a Tool for Teaching Mathematics","volume":"4","author":"Retel","year":"2005","journal-title":"Mechanized Mathematics and Its Applications"},{"key":"edukera","article-title":"Pr\u00e9sentation de la plateforme edukera","volume-title":"Vingt-septi\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2016)","author":"Rognier","year":"2016"},{"key":"seldenselden2008","series-title":"MAA Notes","doi-asserted-by":"publisher","DOI":"10.5948\/UPO9780883859759.009","volume-title":"Overcoming Students' Difficulties in Learning to Understand and Construct Proofs","author":"Selden","year":"2008"},{"key":"Thoma2021","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/s40753-021-00140-1","article-title":"Learning about Proof with the Theorem Prover LEAN: the Abundant Numbers Task","volume":"8","author":"Thoma","year":"2021","journal-title":"International Journal of Research in Undergraduate Mathematics Education"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2024,4,11]],"date-time":"2024-04-11T07:25:22Z","timestamp":1712820322000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/2211.13513v2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,6]]},"references-count":19,"URL":"https:\/\/doi.org\/10.4204\/eptcs.400.7","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,6]]}}}