Wojciech Jedynak
ABSTRACT
We introduce a semantic toolbox for Ltac, the tactic language of the popular Coq proof assistant. We present three formats of operational semantics, each of which has its use in the practice of tactic programming: a big-step specification in the form of natural semantics, a model of implementation in the form of an abstract machine, and a small-step characterization of computation in the form of reduction semantics. The three semantics are provably equivalent and have been obtained via off-the-shelf derivation techniques of the functional correspondence and the syntactic correspondence. We also give examples of Ltac programs and discuss some of the issues that the formal semantics help to clarify.
With this work we hope to enhance the operational understanding of Ltac as well as to set up a framework to reason about Coq scripts and to build tools supporting tactic programming based on rigorous semantics.
- M. S. Ager, D. Biernacki, O. Danvy, and J. Midtgaard. A functional correspondence between evaluators and abstract machines. In PPDP 2003, pp. 8--19, Uppsala, Sweden, 2003. Google Scholar
Digital Library
- D. Aspinall, E. Denney, and C. Lüth. Tactics for hierarchical proof. Mathematics in Computer Science, 3(3):309--330, 2010.Google ScholarCross Ref
- Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Springer, 2004. Google ScholarDigital Library
- M. Biernacka, D. Biernacki, and O. Danvy. An operational foundation for delimited continuations in the CPS hierarchy. Logical Methods in Computer Science, 1(2:5):1--39, 2005.Google Scholar
- M. Biernacka and O. Danvy. A concrete framework for environment machines. ACM Transactions on Computational Logic, 9(1):1--30, 2007. Google ScholarDigital Library
- T. Bourke, M. Daum, G. Klein, and R. Kolanski. Challenges and experiences in managing large-scale proofs. In ICICM, pp. 32--48, Bremen, Germany, 2012. Google ScholarDigital Library
- A. Chlipala. Certified programming with dependent types. http://adam.chlipala.net/cpdt/.Google Scholar
- C. Sacerdoti Coen, E. Tassi, and S. Zacchiroli. Tinycals: Step by step tacticals. ENTCS, 174(2):125--142, 2007. Google ScholarDigital Library
- O. Danvy and L. R. Nielsen. Syntactic theories in practice. In RULE 2001, ENTCS, 59(4), Firenze, Italy, 2001.Google Scholar
- R. Davies and F. Pfenning. A modal analysis of staged computation. Journal of the ACM, 48(3):555--604, 2001. Google ScholarDigital Library
- D. Delahaye. A tactic language for the system Coq. In LPAR 2000, LNCS 1955, pp. 85--95, Reunion Island, 2000. Google ScholarDigital Library
- D. Delahaye. A Proof Dedicated Meta-Language. In LFM 2002, ENTCS, 70(2), pp. 96--109, Copenhagen, Denmark, 2002.Google Scholar
- E. Denney, J. Power, and K. Tourlas. Hiproofs: A hierarchical notion of proof tree. ENTCS, 155, pp. 341--359, 2006. Google ScholarDigital Library
- G. Gonthier. The four colour theorem: Engineering of a formal proof. In ASCM 2007, LNCS 5081, pp. 333--333. Singapore, 2007.Google Scholar
- G. Gonthier. Engineering mathematics: the odd order theorem proof. In POPL 2013, pp. 1--2, Rome, Italy, 2013. Google ScholarDigital Library
- M. J. C. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, LNCS 78, 1979.Google Scholar
- T. Hardin, L. Maranget, and B. Pagano. Functional runtime systems within the lambda-sigma calculus. Journal of Functional Programming, 8(2):131--172, 1998. Google ScholarDigital Library
- F. Kirchner. Coq tacticals and PVS strategies: A small-step semantics. In Design and Application of Strategies/Tactics in Higher Order Logics, pp. 69--83, 2003.Google Scholar
- Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and Amr Sabry. Backtracking, interleaving, and terminating monad transformers. In ICFP 2005, SIGPLAN Notices, Vol. 40, No. 9, pp. 192--203, Tallinn, Estonia, 2005. Google ScholarDigital Library
- G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: formal verification of an OS kernel. In SIGOPS 2009, pp. 207--220. 2009. Google ScholarDigital Library
- J.-L. Krivine. A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation, 20(3):199--207, 2007. Google ScholarDigital Library
- P. J. Landin. The mechanical evaluation of expressions. The Computer Journal, 6(4):308--320, 1964.Google ScholarCross Ref
- D. K. Lee, K. Crary, and R. Harper. Towards a mechanized metatheory of Standard ML. In POPL 2007, pp. 173--184, Nice, France, 2007. Google ScholarDigital Library
- X. Leroy. The Zinc experiment: an economical implementation of the ML language. Rapport Technique 117, INRIA Rocquencourt, Le Chesnay, France, 1990.Google Scholar
- X. Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In POPL 2006, pp. 42--54, Charleston, South Carolina, 2006. Google ScholarDigital Library
- S. Marlow and S. L. Peyton Jones. Making a fast curry: push/enter vs. eval/apply for higher-order languages. Journal of Functional Programming, 16(4-5):415--449, 2006. Google ScholarDigital Library
- A. P. Martin, H. B. Gardiner, and J. C. P. Woodcock. A tactic calculus -- abridged version. Formal Aspects of Computing, 8(4):479--489, 1996.Google ScholarCross Ref
- A. P. Martin and J. Gibbons. A monadic interpretation of tactics. Unpublished note, 2002.Google Scholar
- T. Nipkow, M. Wenzel, and L. C. Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer-Verlag, 2002. Google ScholarDigital Library
- The Caml Language. http://caml.inria.fr/.Google Scholar
- S. L. Peyton Jones. Implementing lazy functional languages on stock hardware: The spineless tagless G-machine. Journal of Functional Programming, 2(2):127--202, 1992.Google ScholarCross Ref
- F. Pfenning and C. Schürmann. System description: Twelf -- a meta-logical framework for deductive systems. In CADE 1999, LNAI 1632, pp. 202--206, Trento, Italy, 1999. Google ScholarDigital Library
- M. Piróg and D. Biernacki. A systematic derivation of the STG machine verified in Coq. In Jeremy Gibbons, editor, Haskell'10, pp. 25--36, Baltimore, MD, 2010. Google ScholarDigital Library
- J. C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation 11(4):363--397, 1998. Google ScholarDigital Library
- The Coq Development Team. The Coq Proof Assistant Reference Manual, Version 8.4pl2, 2013.Google Scholar
- I. Whiteside, D. Aspinall, L. Dixon, and G. Grov. Towards formal proof script refactoring. In ICICM 2011, pp. 260--275, Bertinoro, Italy, 2011. Google ScholarDigital Library
Index Terms
- An operational foundation for the tactic language of Coq
Recommendations
Coinductive big-step operational semantics
Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We ...
Inter-deriving semantic artifacts for object-oriented programming
We present a new abstract machine for Abadi and Cardelli's untyped non-imperative calculus of objects. This abstract machine mechanically corresponds to both the reduction semantics (i.e., small-step operational semantics) and the natural semantics (...
Defunctionalized interpreters for programming languages
ICFP '08This document illustrates how functional implementations of formal semantics (structural operational semantics, reduction semantics, small-step and big-step abstract machines, natural semantics, and denotational semantics) can be transformed into each ...
Comments