ProofViz: An Interactive Visual Proof Explorer

1. 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

2. 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–705. Association for Computing Machinery, New York, NY, USA (2017). https://doi.org/10.1145/3009837.3009886

3. Curry, H.B.: Functionality in combinatory logic. Proc. Nat. Acad. Sci. 20(11), 584–590 (1934). https://doi.org/10.1073/pnas.20.11.584

   Article  MATH  Google Scholar 

4. Dybjer, P.: Inductive families. Formal Aspects Comput. 6(4), 440–465 (1994)

   Article  Google Scholar 

5. 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–1219, May 2019. https://doi.org/10.1109/SP.2019.00005

6. Felleisen, M., et al.: The racket manifesto. In: 1st Summit on Advances in Programming Languages (SNAPL 2015), pp. 113–128 (2015)

   Google Scholar 

7. Friedman, D.P., Christiansen, D.T., Bibby, D., Harper, R., McBride, C.: The Little Typer. The Massachusetts Institute of Technology, Cambridge, Massuchesetts (2018)

   Google Scholar 

8. Howard, W.A.: The Formulae-as-Types Notion of Construction. To HB Curry: essays on combinatory logic, lambda calculus and formalism 44, 479–490 (1980)

   Google Scholar 

9. 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–165. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02768-1_9

   Chapter  Google Scholar 

10. Libal, T., Riener, M., Rukhaia, M.: Advanced proof viewing in ProofTool. Electron. Proc. Theoretical Comput. Sci. 167, 35–47 (2014). https://doi.org/10.4204/EPTCS.167.6

    Article  MathSciNet  Google Scholar 

11. McBride, C.: Dependently Typed Functional Programs and Their Proofs. Ph.D. thesis, University of Edinburgh (2000)

    Google Scholar 

12. 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–71. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46028-4_4

    Chapter  MATH  Google Scholar 

13. Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_217

    Chapter  Google Scholar 

14. Pierce, B., et al.: Logical Foundations, Software Foundations, vol. 1, September 2020. https://softwarefoundations.cis.upenn.edu/lf-current/index.html

15. Pit-Claudel, C.: Untangling mechanized proofs. In: Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering. SLE 2020, pp. 155–174. Association for Computing Machinery, New York, NY, USA (2020). https://doi.org/10.1145/3426425.3426940

16. Siekmann, J., et al.: L\({\Omega }\)UI: lovely \({\Omega }\)MEGA user interface. Formal Aspects Comput. 11(3), 326–342 (1999). https://doi.org/10.1007/s001650050053

    Article  Google Scholar 

17. Tews, H.: Prooftree: Proof Tree Visualization for Proof General (2017). http://askra.de/software/prooftree/. Accessed 05 Nov 2020

18. Wadler, P.: Propositions as types. Commun. ACM 58(12), 75–84 (2015). https://doi.org/10.1145/2699407

    Article  Google Scholar 

19. Zinzindohoué, 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

Download references