Prawf: an interactive proof system for program extraction. (English) Zbl 07633503
Anselmo, Marcella (ed.) et al., Beyond the horizon of computability. 16th conference on computability in Europe, CiE 2020, Fisciano, Italy, June 29 – July 3, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12098, 137-148 (2020).
Summary: We present an interactive proof system dedicated to program extraction from proofs. In a previous paper [5] the underlying theory IFP (Intuitionistic Fixed Point Logic) was presented and its soundness proven. The present contribution describes a prototype implementation and explains its use through several case studies. The system benefits from an improvement of the theory which makes it possible to extract programs from proofs using unrestricted strictly positive inductive and coinductive definitions, thus removing the previous admissibility restrictions.
For the entire collection see [Zbl 1502.68017].
For the entire collection see [Zbl 1502.68017].
MSC:
| 68Qxx | Theory of computing |
References:
| [1] | Isabelle. https://isabelle.in.tum.de/ |
| [2] | Agda official website. http://wiki.portal.chalmers.se/agda/ |
| [3] | Berger, U.: Realisability for induction and coinduction with applications to constructive analysis. J. Univ. Comput. Sci. 16(18), 2535-2555 (2010) · Zbl 1219.03074 |
| [4] | Berger, U., Miyamoto, K., Schwichtenberg, H., Seisenberger, M.: Minlog - a tool for program extraction supporting algebras and coalgebras. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 393-399. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22944-2_29 · Zbl 1344.68201 · doi:10.1007/978-3-642-22944-2_29 |
| [5] | Berger, U., Petrovska, O.: Optimized program extraction for induction and coinduction. In: Manea, F., Miller, R.G., Nowotka, D. (eds.) CiE 2018. LNCS, vol. 10936, pp. 70-80. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94418-0_7 · Zbl 1509.03089 · doi:10.1007/978-3-319-94418-0_7 |
| [6] | Berger, U., Tsuiki, H.: Intuitionistic fixed point logic (2019). Unpublished manuscript available on ArXiv · Zbl 1498.03065 |
| [7] | Bertot, Y., Castéran, P.: Interactive theorem proving and program development (2004) · Zbl 1069.68095 |
| [8] | Constable, R.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Upper Saddle River (1986) |
| [9] | The Coq Proof Assistant. https://coq.inria.fr · Zbl 1039.68543 |
| [10] | Lockwood, J.: Nuprl: an open logical programming environment: a practical framework for sharing formal models and tools. Program extraction (1998). http://www.nuprl.org |
| [11] | Prawf official website. https://prawftree.wordpress.com/ |
| [12] | Tsuiki, H.: Real number computation through gray code embedding. Theor. Comput. Sci. 284(2), 467-485 (2002) · Zbl 1042.68071 · doi:10.1016/S0304-3975(01)00104-9 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
