Procedural Representation of CIC Proof Terms
Tóm tắt
We propose an effective procedure, the first one to our knowledge, for translating a proof term of the Calculus of Inductive Constructions (CIC), into a tactical expression of the high-level specification language of a CIC-based proof assistant like coq (Coq development team 2008) or matita (Asperti et al., J Autom Reason 39:109–139, 2007). This procedure, which should not be considered definitive at its present stage, is intended for translating the logical representation of a proof coming from any source, i.e. from a digital library or from another proof development system, into an equivalent proof presented in the proof assistant’s editable high-level format. To testify to effectiveness of our procedure, we report on its implementation in matita and on the translation of a significant set of proofs (Guidi, ACM Trans Comput Log 2009) from their logical representation as coq 7.3.1 (Coq development team 2002) CIC proof terms to their high-level representation as tactical expressions of matita’s user interface language.
Tài liệu tham khảo
Coq development team: The Coq Proof Assistant Reference Manual Version 8.1pl4. INRIA, Orsay (2008)
Asperti, A., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: User interaction with the Matita proof assistant. J. Autom. Reason. 39, 109–139 (2007) (Special issue on user interfaces for theorem proving)
Guidi, F.: The Formal System lambda-delta. ACM Trans. Comput. Log. (2010, in press)
Coq development team: The Coq Proof Assistant Reference Manual Version 7.3.1. INRIA, Orsay (2002)
Barthe, G., Pons, O.: Type isomorphisms and proof reuse in dependent type theory. In: Honsell, F., Miculan, M. (eds.) 4th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2001). LNCS, vol. 2030, pp. 57–71. Springer, Heidelberg (2001)
Sacerdoti Coen, C.: From proof-assistants to distributed libraries of mathematics: tips and pitfalls. In: Mathematical Knowledge Management 2003. LNCS, vol. 2594, pp. 30–44. Springer, Heidelberg (2003)
Coquand, T., Paulin-Mohring, C.: Inductively defined types. In: Martin-Löf, P., Mints, G. (eds.) Proceedings of the International Conference on Computer Logic (Colog ’88). LNCS, vol. 417. Springer, Heidelberg (1990)
van Benthem Jutting, L.: Description of AUT-68. In: Selected Papers on Automath, pp. 251–273. North-Holland, Amsterdam (1994)
Bundy, A.: A science of reasoning. In: Lassez, J., Plotkin, G. (eds.) Computational Logic: Essays in Honor of Alan Robinson, pp. 178–198. MIT, Cambridge (1991)
Kamareddine, F., Laan, T., Nederpelt, R.: A modern perspective on type theory from its origins until today. In: Applied Logic Series, vol. 29. Kluwer, Dordrecht (2004)
Asperti, A., Padovani, L., Sacerdoti Coen, C., Guidi, F., Schena, I.: Mathematical knowledge management in HELM. Ann. Math. Artif. Intell. 38(1), 27–46 (2003)
Network Working Group: Uniform Resource Identifiers (URI): Generic Syntax. RCF 2396 (1998)
Sacerdoti Coen, C.: Declarative representation of proof terms. J. Autom. Reason. (2009) (Special issue on programming languages and mechanized mathematics systems). doi:10.1007/s10817-009-9136-7
Sacerdoti Coen, C.: Explanation in natural language of \(\bar\lambda\mu\tilde\mu\)-terms. In: 4th Int. Conf. on Mathematical Knowledge Management (MKM2005). LNAI, vol. 3863, pp. 234–249. Springer, Heidelberg (2006)
Coscoy, Y.: A natural language explanation for formal proofs. In: Retoré, C. (ed.) Int. Conf. on Logical Aspects of Computational Linguistics (LACL). LNAI, vol. 1328, pp. 149–167. Springer, Heidelberg (1996)
Paulin-Mohring, C.: Extraction de programmes dans le Calcul des Constructions. Ph.D. thesis, Université Paris 7, Paris (1989)
Maietti, M., Sambin, G.: Towards a minimalist foundation for constructive mathematics. In: Crosilla, L., Schuster, P. (eds.) From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, Oxford Logic Guides, vol. 48, pp. 91–114. Oxford University Press, Oxford (2005)
Guidi, F.: lambda-delta. Formal specification with the proof assistant coq 7.3.1. http://helm.cs.unibo.it/lambda-delta/ (2007)
de Bruijn, N.: A survey of the project automath. In: Selected Papers on Automath, pp. 141–161. North-Holland, Amsterdam (1994)
van Benthem Jutting, L.: Checking Landau’s Grundlagen in the automath system. In: Selected Papers on Automath, pp. 299–301, 701–720, 721–732, 763–799, 805–808. North-Holland, Amsterdam (1994)
Wiedijk, F.: The De Bruijn Factor. Typescript note (2000)
Guidi, F.: Procedural representation of CIC proof terms. In: Carette, J., Wiediejk, F. (eds.) Local Proceedings of Programming Languages for Mechanized Mathematics Workshop (PLMMS 2007) RISC-LINZ Report Series 07-10 (3120), pp. 36–52. University of Linz, Linz (2007)