{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T04:47:38Z","timestamp":1742964458601,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030839772"},{"type":"electronic","value":"9783030839789"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-83978-9_6","type":"book-chapter","created":{"date-parts":[[2021,8,22]],"date-time":"2021-08-22T23:03:52Z","timestamp":1629673432000},"page":"116-135","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["ProofViz: An Interactive Visual Proof Explorer"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0807-8163","authenticated-orcid":false,"given":"Daniel","family":"Melcer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4760-0658","authenticated-orcid":false,"given":"Stephen","family":"Chang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,8,23]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Chang, S., Ballantyne, M., Turner, M., Bowman, W.J.: Dependent type systems as macros. In: Proceedings ACM Programming Language 4(POPL), December 2019. https:\/\/doi.org\/10.1145\/3371071","DOI":"10.1145\/3371071"},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Chang, S., Knauth, A., Greenman, B.: Type systems as macros. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. POPL 2017, pp. 694\u2013705. Association for Computing Machinery, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3009837.3009886","DOI":"10.1145\/3009837.3009886"},{"issue":"11","key":"6_CR3","doi-asserted-by":"publisher","first-page":"584","DOI":"10.1073\/pnas.20.11.584","volume":"20","author":"HB Curry","year":"1934","unstructured":"Curry, H.B.: Functionality in combinatory logic. Proc. Nat. Acad. Sci. 20(11), 584\u2013590 (1934). https:\/\/doi.org\/10.1073\/pnas.20.11.584","journal-title":"Proc. Nat. Acad. Sci."},{"issue":"4","key":"6_CR4","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BF01211308","volume":"6","author":"P Dybjer","year":"1994","unstructured":"Dybjer, P.: Inductive families. Formal Aspects Comput. 6(4), 440\u2013465 (1994)","journal-title":"Formal Aspects Comput."},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In: 2019 IEEE Symposium on Security and Privacy (SP), pp. 1202\u20131219, May 2019. https:\/\/doi.org\/10.1109\/SP.2019.00005","DOI":"10.1109\/SP.2019.00005"},{"key":"6_CR6","unstructured":"Felleisen, M., et al.: The racket manifesto. In: 1st Summit on Advances in Programming Languages (SNAPL 2015), pp. 113\u2013128 (2015)"},{"key":"6_CR7","unstructured":"Friedman, D.P., Christiansen, D.T., Bibby, D., Harper, R., McBride, C.: The Little Typer. The Massachusetts Institute of Technology, Cambridge, Massuchesetts (2018)"},{"key":"6_CR8","unstructured":"Howard, W.A.: The Formulae-as-Types Notion of Construction. To HB Curry: essays on combinatory logic, lambda calculus and formalism 44, 479\u2013490 (1980)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-030-02768-1_9","volume-title":"Programming Languages and Systems","author":"H Kawabata","year":"2018","unstructured":"Kawabata, H., Tanaka, Y., Kimura, M., Hironaka, T.: Traf: a graphical proof tree viewer cooperating with Coq through proof general. In: Ryu, S. (ed.) APLAS 2018. LNCS, vol. 11275, pp. 157\u2013165. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02768-1_9"},{"key":"6_CR10","doi-asserted-by":"publisher","first-page":"35","DOI":"10.4204\/EPTCS.167.6","volume":"167","author":"T Libal","year":"2014","unstructured":"Libal, T., Riener, M., Rukhaia, M.: Advanced proof viewing in ProofTool. Electron. Proc. Theoretical Comput. Sci. 167, 35\u201347 (2014). https:\/\/doi.org\/10.4204\/EPTCS.167.6","journal-title":"Electron. Proc. Theoretical Comput. Sci."},{"key":"6_CR11","unstructured":"McBride, C.: Dependently Typed Functional Programs and Their Proofs. Ph.D. thesis, University of Edinburgh (2000)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-46028-4_4","volume-title":"Implementation of Functional Languages","author":"M de Mol","year":"2002","unstructured":"de Mol, M., van Eekelen, M., Plasmeijer, R.: Theorem proving for functional programmers. In: Arts, T., Mohnen, M. (eds.) IFL 2001. LNCS, vol. 2312, pp. 55\u201371. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46028-4_4"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"6_CR14","unstructured":"Pierce, B., et al.: Logical Foundations, Software Foundations, vol. 1, September 2020. https:\/\/softwarefoundations.cis.upenn.edu\/lf-current\/index.html"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Pit-Claudel, C.: Untangling mechanized proofs. In: Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering. SLE 2020, pp. 155\u2013174. Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3426425.3426940","DOI":"10.1145\/3426425.3426940"},{"issue":"3","key":"6_CR16","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/s001650050053","volume":"11","author":"J Siekmann","year":"1999","unstructured":"Siekmann, J., et al.: L$${\\Omega }$$UI: lovely $${\\Omega }$$MEGA user interface. Formal Aspects Comput. 11(3), 326\u2013342 (1999). https:\/\/doi.org\/10.1007\/s001650050053","journal-title":"Formal Aspects Comput."},{"key":"6_CR17","unstructured":"Tews, H.: Prooftree: Proof Tree Visualization for Proof General (2017). http:\/\/askra.de\/software\/prooftree\/. Accessed 05 Nov 2020"},{"issue":"12","key":"6_CR18","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/2699407","volume":"58","author":"P Wadler","year":"2015","unstructured":"Wadler, P.: Propositions as types. Commun. ACM 58(12), 75\u201384 (2015). https:\/\/doi.org\/10.1145\/2699407","journal-title":"Commun. ACM"},{"key":"6_CR19","doi-asserted-by":"publisher","unstructured":"Zinzindohou\u00e9, J.K., Bhargavan, K., Protzenko, J., Beurdouche, B.: Hacl*: a verified modern cryptographic library. In: Conference on Computer and Communications Security (CCS) (2017). https:\/\/doi.org\/10.1145\/3133956.3134043","DOI":"10.1145\/3133956.3134043"}],"container-title":["Lecture Notes in Computer Science","Trends in Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-83978-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,22]],"date-time":"2021-08-22T23:25:14Z","timestamp":1629674714000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-83978-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030839772","9783030839789"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-83978-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 August 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TFP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Trends in Functional Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 February 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 February 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tfp2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/tfp2021.org\/","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":"18","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":"6","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":"33% - 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":"3-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)"}}]}}