×

The proof monad. (English) Zbl 1208.68144

Summary: A formalism for expressing the operational semantics of proof languages used in procedural theorem provers is proposed. It is argued that this formalism provides an elegant way to describe the computational features of proof languages, such as side effects, exception handling, and backtracking. The formalism, called proof monads, finds its roots in category theory, and in particular satisfies the monad laws. It is shown that the framework’s monadic operators are related to fundamental tactics and strategies in procedural theorem provers. Finally, the paper illustrates how proof monads can be used to implement semantically clean control structure mechanisms in actual proof languages.

MSC:

68Q55 Semantics in the theory of computing
18C15 Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

ACL2; ALF; Coq; PVS; LCF
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Adámek, J.; Herrlich, H.; Strecker, G., Abstract and Concrete Categories. Abstract and Concrete Categories, Pure and Applied Mathematics (1990), John Wiley & Sons: John Wiley & Sons New York, NY · Zbl 0695.18001
[2] M. Archer, B.D. Vito, C. Muñoz, Developing user strategies in PVS: a tutorial, in: Proc. Int. Workshop on Design and Application of Strategies/Tactics in Higher Order Logics, number CP-2003-212448 in NASA Conference Publication, pp. 16-42.; M. Archer, B.D. Vito, C. Muñoz, Developing user strategies in PVS: a tutorial, in: Proc. Int. Workshop on Design and Application of Strategies/Tactics in Higher Order Logics, number CP-2003-212448 in NASA Conference Publication, pp. 16-42.
[3] Asperti, A.; Coen, C. S.; Tassi, E.; Zacchiroli, S., Crafting a proof assistant, (Altenkirch, T.; McBride, C., Proc. 2006 Int. Workshop on Proofs and Programs. Proc. 2006 Int. Workshop on Proofs and Programs, LNCS, vol. 4502 (2007), Springer: Springer Heidelberg), 18-32 · Zbl 1178.68524
[4] Avron, A., Simple consequence relations, Inform. and Comput., 92, 105-139 (1991) · Zbl 0733.03007
[5] B. Barras, S. Boutin, C. Cornes, J. Courant, J. Filliatre, E. Giménez, H. Herbelin, G. Huet, C. Muñoz, C. Murthy, C. Parent, C. Paulin, A. Saïbi, B. Werner, The Coq Proof Assistant Reference Manual, 2006.; B. Barras, S. Boutin, C. Cornes, J. Courant, J. Filliatre, E. Giménez, H. Herbelin, G. Huet, C. Muñoz, C. Murthy, C. Parent, C. Paulin, A. Saïbi, B. Werner, The Coq Proof Assistant Reference Manual, 2006.
[6] A. Buronni, Théorie des catégories, 2004. Informal lectures.; A. Buronni, Théorie des catégories, 2004. Informal lectures.
[7] Cirstea, H.; Kirchner, C.; Liquori, L., Rewrite strategies in the rewriting calculus, (Gramlich, B.; Lucas, S., Proc. 3rd Int. Workshop on Reduction Strategies in Rewriting and Programming. Proc. 3rd Int. Workshop on Reduction Strategies in Rewriting and Programming, Electronic Notes in Theoretical Computer Science, vol. 86 (2003), Elsevier: Elsevier Amsterdam) · Zbl 1270.68122
[8] Coen, C. S.; Tassi, E.; Zacchiroli, S., Tinycals: step by step tacticals, (Proc. 7th Workshop on User Interfaces for Theorem Provers. Proc. 7th Workshop on User Interfaces for Theorem Provers, Electronic Notes in Theoretical Computer Science, vol. 174 (2007), Elsevier: Elsevier Amsterdam), 125-142 · Zbl 1278.68253
[9] Curien, P. L.; Herbelin, H., The duality of computation, ACM SIGPLAN Notices, 35 (2000) · Zbl 1321.68146
[10] Delahaye, D., A tactic language for the system Coq, (Parigot, M.; Voronkov, A., Proc. 7th Int. Conf. on Logic for Programming and Automated Reasoning. Proc. 7th Int. Conf. on Logic for Programming and Automated Reasoning, LNCS, vol. 1955 (2000), Springer: Springer Heidelberg), 85-95 · Zbl 0988.68584
[11] Dowek, G.; Hardin, T.; Kirchner, C., Theorem proving modulo, J. Automat. Reason., 31, 33-72 (2003) · Zbl 1049.03011
[12] (Gordon, M.; Melham, T., Introduction to HOL: A Theorem Proving Environment for Higher Order Logic (1993), Cambridge University Press) · Zbl 0779.68007
[13] Gordon, M.; Milner, R.; Wadsworth, C., Edinburgh LCF: A Mechanized Logic of Computation. Edinburgh LCF: A Mechanized Logic of Computation, LNCS, vol. 78 (1979), Springer: Springer Heidelberg · Zbl 0421.68039
[14] Jacobs, B., Categorical Logic and Type Theory. Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics, vol. 141 (1998), Elsevier: Elsevier Amsterdam · Zbl 0911.03001
[15] G. Jojgov, Incomplete proofs and terms and their use in interactive theorem proving, Ph.D. Thesis, Technische Universiteit Eindhoven, 2004.; G. Jojgov, Incomplete proofs and terms and their use in interactive theorem proving, Ph.D. Thesis, Technische Universiteit Eindhoven, 2004.
[16] M. Kaufmann, J.S. Moore, ACL2: An industrial strength version of Nqthm, in: Compass’96: Eleventh Annual Conference on Computer Assurance, National Institute of Standards and Technology, Gaithersburg, Maryland, 1996, p. 23.; M. Kaufmann, J.S. Moore, ACL2: An industrial strength version of Nqthm, in: Compass’96: Eleventh Annual Conference on Computer Assurance, National Institute of Standards and Technology, Gaithersburg, Maryland, 1996, p. 23.
[17] Kirchner, C.; Kirchner, F.; Kirchner, H., Strategic computations and deductions, (Reasoning in Simple Type Theory. Reasoning in Simple Type Theory, Mathematical Logic and Foundations, vol. 17 (2008), College Publications) · Zbl 1226.03027
[18] F. Kirchner, Interoperable proof systems, Ph.D. Thesis, École Polytechnique, 2007.; F. Kirchner, Interoperable proof systems, Ph.D. Thesis, École Polytechnique, 2007.
[19] Kirchner, F.; Muñoz, C., PVS#: Streamlined tacticals for PVS, (Workshop on Strategies in Automated Deduction. Workshop on Strategies in Automated Deduction, Electronic Notes in Theoretical Computer Science, vol. 174/11 (2007), Elsevier: Elsevier Amsterdam), 47-58 · Zbl 1277.68242
[20] F. Kirchner, C. Sacerdoti Coen, The Fellowship proof manager, 2007.; F. Kirchner, C. Sacerdoti Coen, The Fellowship proof manager, 2007.
[21] Lambek, J., Deductive systems and categories I: Syntactic calculus and residuated categories, Math. Systems Theory, 2, 287-318 (1968) · Zbl 0176.28901
[22] Lambek, J.; Scott, P., Introduction to Higher Order Categorical Logic. Introduction to Higher Order Categorical Logic, Cambridge Studies in Advanced Mathematics, vol. 7 (1986), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0596.03002
[23] Lane, S. M., Categories for the Working Mathematician. Categories for the Working Mathematician, Graduate Texts in Mathematics, vol. 5 (1971), Springer: Springer New York, NY · Zbl 0232.18001
[24] Lawvere, F. W., Adjointness in foundations, Dialectica, 23, 281-296 (1969) · Zbl 0341.18002
[25] L. Magnusson, The Implementation of ALF: A Proof Editor Based on Martin-Löf’s Monomorphic Type Theory with Explicit Substitution, Ph.D. Thesis, Chalmers University of Technology and Göteborg University, 1995.; L. Magnusson, The Implementation of ALF: A Proof Editor Based on Martin-Löf’s Monomorphic Type Theory with Explicit Substitution, Ph.D. Thesis, Chalmers University of Technology and Göteborg University, 1995.
[26] A. Martin, P. Gardiner, J. Woodcock, A tactic calculus, in: J. Allison (Ed.), Formal Aspects of Computing.; A. Martin, P. Gardiner, J. Woodcock, A tactic calculus, in: J. Allison (Ed.), Formal Aspects of Computing.
[27] A. Martin, J. Gibbons, A monadic interpretation of tactics, 2002.; A. Martin, J. Gibbons, A monadic interpretation of tactics, 2002.
[28] C. McBride, Dependently Typed Functional Programs and their Proofs, Ph.D. Thesis, University of Edinburgh, 1999.; C. McBride, Dependently Typed Functional Programs and their Proofs, Ph.D. Thesis, University of Edinburgh, 1999.
[29] E. Moggi, Computational lambda-calculus and monads, in: Proc. 4th IEEE Symp. Logic in Computer Science, IEEE Comp. Soc. Press, 1989 (Superseded by [30]).; E. Moggi, Computational lambda-calculus and monads, in: Proc. 4th IEEE Symp. Logic in Computer Science, IEEE Comp. Soc. Press, 1989 (Superseded by [30]). · Zbl 0716.03007
[30] Moggi, E., Notions of computation and monads, Inform. and Comput., 93, 55-92 (1991) · Zbl 0723.68073
[31] C. Muñoz, Un calcul de substitutions pour la représentation de preuves partielles en théorie de types, Thèse de doctorat, Université Paris 7, 1997 (English version available as INRIA research report RR-3309).; C. Muñoz, Un calcul de substitutions pour la représentation de preuves partielles en théorie de types, Thèse de doctorat, Université Paris 7, 1997 (English version available as INRIA research report RR-3309).
[32] Owre, S.; Rushby, J.; Shankar, N., PVS: a prototype verification system, (Kapur, D., Proc. 11th Int. Conf. on Automated Deduction. Proc. 11th Int. Conf. on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 607 (1992), Springer), 748-752
[33] Seely, R., Hyperdoctrines, natural deduction and the Beck condition, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 29, 505-542 (1983) · Zbl 0565.03032
[34] Seely, R., Locally cartesian closed categories and type theory, (Mathematical Proceedings of the Cambridge Philosophical Society, vol. 95 (1984), Cambridge Philosophical Society), 33-48 · Zbl 0539.03048
[35] Seely, R.; logic, Linear, ∗-autonomous categories and cofree coalgebras, (Gray, J.; Scedrov, A., Categories in Computer Science and Logic. Categories in Computer Science and Logic, Contemporary Mathematics, vol. 92 (1989), American Mathematical Society: American Mathematical Society Providence, Rhode Island), 371-382
[36] N. Shankar, S. Owre, J. Rushby, D. Stringer-Calvert, PVS Prover Guide, Computer Science Laboratory, SRI International, 1999.; N. Shankar, S. Owre, J. Rushby, D. Stringer-Calvert, PVS Prover Guide, Computer Science Laboratory, SRI International, 1999.
[37] A. Spiwack, [Coq-Club] Instantiating existential variables, howpublished Email conversation, 2009.; A. Spiwack, [Coq-Club] Instantiating existential variables, howpublished Email conversation, 2009.
[38] Streicher, T., Semantics of Type Theory. Semantics of Type Theory, Progress in Theoretical Computer Science, vol. 5 (1991), Birkhäuser · Zbl 0790.68068
[39] Wadler, P., Monads for functional programming, (Jeuring, J.; Meijer, E., Advanced Functional Programming. Advanced Functional Programming, LNCS, vol. 925 (1995), Springer: Springer Heidelberg)
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.