×

Meta programming on the proof level. (English) Zbl 1178.68526

Summary: Computer aided proof generation is used for many reasons from formalization of mathematics to formal computer program development. Our research concentrates on completely declarative style proofs used to develop imperative programs in a refinement-based model (i.e. deriving the algorithm from the specification).
We investigate why and how to use meta programming techniques for proof development. We examine techniques already used in programming languages if they are applicable for proof construction and point out the specialities caused by the different application area. It is also shown that while meta programming techniques are often dangerous when used to develop programs, they are safe tools for proof development.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite