摘要: This report presents the Galculator, a tool aimed at deriving equational proofs in arbitrary domains using Galois connections as fundamental concept. When combined with pointfree transform and indirect equality principle, offer very powerful, generic device to tackle complexity of program verification. We show how rewriting rules derived from properties are applied strategic term system which, current prototype, is implemented Haskell. The prospect integrating Galculator other proof assistants such eg. Coq also discussed.
参考文章(28)
David Pichardie, Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certifiés Rennes 1. ,(2005)
P.F. Hoogendijk, R.C. Backhouse, Jaap van der Woude, T.S. Voermans, C.J. Aarts, A relational theory of datatypes Technische Universiteit Eindhoven. ,(1992)
J. Roger Hindley, Basic Simple Type Theory ,(1997)
Horatiu Cirstea, Claude Kirchner, Luigi Liquori, The Rho Cube foundations of software science and computation structure. pp. 168- 183 ,(2001) , 10.1007/3-540-45315-6_11
Eelco Visser, Stratego: A Language for Program Transformation Based on Rewriting Strategies System Description of Stratego 0.5 rewriting techniques and applications. pp. 357- 361 ,(2001) , 10.1007/3-540-45127-7_27
Eelco Visser, Stratego: A Language for Program Transformation Based on Rewriting Strategies rewriting techniques and applications. pp. 357- 362 ,(2001)
Oege de Moor, Richard Bird, Algebra of programming Prentice-Hall, Inc.. ,(1997)
José N. Oliveira, César J. Rodrigues, Pointfree Factorization of Operation Refinement FM 2006: Formal Methods. ,vol. 4085, pp. 236- 251 ,(2006) , 10.1007/11813040_17
José N. Oliveira, Transforming Data by Calculation Generative and Transformational Techniques in Software Engineering II. ,vol. 5235, pp. 134- 195 ,(2007) , 10.1007/978-3-540-88643-3_4
Alcino Cunha, José Nuno Oliveira, Joost Visser, Type-Safe Two-Level Data Transformation FM 2006: Formal Methods. ,vol. 4085, pp. 284- 299 ,(2006) , 10.1007/11813040_20