'Galculator': functional prototype of a Galois-connection based proof assistant

ABSTRACT

Galculator is the name of the prototype of a proof assistant of a special brand: it is solely based on the algebra of Galois connections. When combined with the pointfree transform and tactics such as the indirect equality principle, Galois connections offer a very powerful, generic device to tackle the complexity of proofs in program verification. The paper describes the architecture of the current Galculator prototype, which is implemented in Haskell in order to steer types as much as possible. The prospect of integrating the Galculator with other proof assistants such as e.g. Coq is also discussed

REFERENCES

• 1: C. Aarts, R.C. Backhouse, P. Hoogendijk, E. Voermans, and J. van der Woude. A relational theory of datatypes. Available from www.cs.nott. ac. uk/~rcb/ papers, December 1992.
• 2: J.C. Almeida. Program verification in Coq, 2008. Lecture notes for MAP-I course on Program Semantics, Verification, and Construction available from http://twiki.di.uminho.pt.
• 3: Arthur I. Baars , S. Doaitse Swierstra, Typing dynamic typing, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.157-166, October 04-06, 2002, Pittsburgh, PA, USA
• 4: Kevin Backhouse , Roland Backhouse, Safety of abstract interpretations for free, via logical relations and Galois connections, Science of Computer Programming, v.51 n.1-2, p.153-196, May 2004 [doi>10.1016/j.scico.2003.06.002]
• 5: R.C. Backhouse. Mathematics of Program Construction. Univ. of Nottingham, 2004. Draft of book in preparation. 608 pages.
• 6: John Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, Communications of the ACM, v.21 n.8, p.613-641, Aug. 1978 [doi>10.1145/359576.359579]
• 7: Y. Bertot and P. Castéran. Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions. Texts in theoretical computer science. Springer, 2004.
• 8: Richard Bird , Oege de Moor, Algebra of programming, Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
• 9: J. Bohorquez and C. Rocha. Towards the effective use of formal logic in the teaching of discrete math. Information Technology Based Higher Education and Training, 2005. ITHET 2005., pages S3C/1¿S3C/8, 2005.
• 10: James Cheney , Ralf Hinze, A lightweight implementation of generics and dynamics, Proceedings of the 2002 ACM SIGPLAN workshop on Haskell, p.90-104, October 03, 2002, Pittsburgh, Pennsylvania [doi>10.1145/581690.581698]
• 11: Horatiu Cirstea , Claude Kirchner , Luigi Liquori, The Rho Cube, Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures, p.168-183, April 02-06, 2001
• 12: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• 13: Alcino Cunha , Joost Visser, Strongly Typed Rewriting For Coupled Software Transformation, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.1, p.17-34, April, 2007 [doi>10.1016/j.entcs.2006.10.019]
• 14: A. Cunha, J.N. Oliveira, and J. Visser. Type-safe two-level data transformation. In FM'06 , volume 4085 of LNCS, pages 284--289. Springer-Verlag, Aug. 2006.
• 15: D. Delahaye and M. Mayero. Dealing with algebraic expressions over a field in coq using maple. J.Symb.Comput., 39(5):569--592, 2005.
• 16: J.-C. Filliâtre and C. Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. In W. Damm and H. Hermanns, editors, CAV, volume 4590 of LNCS, pages 173--177. Springer, 2007.
• 17: P.J. Freyd and A. Ščedrov. Categories, Allegories, volume 39 of Mathematical Library. North-Holland, 1990.
• 18: R. Hinze and A. Löh. Guide2lhs2tex (for version 1.13), February 2008.
• 19: R. Hinze, A. Löh, and B.C.d.S. Oliveira. "Scrap your boilerplate" reloaded. In Proc. 8th Int. Symp. on Functional and Logic Programming, volume 3945 of LNCS, pages 13--29. Springer, 2006.
• 20: Daniel Jackson, Software Abstractions: Logic, Language, and Analysis, The MIT Press, 2006
• 21: Mark P. Jones, Functional Programming with Overloading and Higher-Order Polymorphism, Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques-Tutorial Text, p.97-136, May 24-30, 1995
• 22: Ralf Lämmel , Joost Visser, A Strafunski Application Letter, Proceedings of the 5th International Symposium on Practical Aspects of Declarative Languages, p.357-375, January 13-14, 2003
• 23: D. Leijen and E. Meijer. Parsec: Direct style monadic parser combinators for the real world. Technical Report UU-CS-2001-27, Department of Computer Science, Universiteit Utrecht, 2001.
• 24: P. Lincoln M. Clavel, S. Eker and J. Meseguer. Principles of Maude. In J. Meseguer, editor, Electronic Notes in Theoretical Computer Science, volume 4. Elsevier Science Publishers, 2000.
• 25: R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348--375, August 1978.
• 26: C. Necco, J.N. Oliveira, and J. Visser. Extended static checking by strategic rewriting of pointfree relational expressions. Technical Report FAST:07.01, CCTC Research Centre, University of Minho, 2007.
• 27: J.N. Oliveira. Transforming Data by Calculation. In Ralf Lämmel, João Saraiva, and Joost Visser, editors, GTTSE 2007 Proceedings, pages 139--198, July 2007.
• 28: J.N. Oliveira and C.J. Rodrigues. Transposing relations: from Maybe functions to hash tables. In MPC'04, volume 3125 of LNCS, pages 334--356. Springer, 2004.
• 29: O. Ore. Galois connexions, 1944. Trans. Amer. Math. Soc., 55:493--513.
• 30: S. Peyton Jones. Haskell 98: Language and libraries. J. Funct. Program., 13(1):1--255, 2003.
• 31: D. Pichardie. Interprétation abstraite en logique intuitionniste: extraction d'analyseurs Java certifiés. PhD thesis, Univ. de Rennes, 2005.
• 32: V. Pratt. Origins of the calculus of binary relations. In Proc. of the Seventh Annual IEEE Symposium on Logic in Computer Science, pages 248--254, Santa Cruz, CA, 1992. IEEE Computer Soc.
• 33: T. Sheard, J. Hook, and N. Linger. GADTs + Extensible Kinds = Dependent Programming. Technical report, Portland State University, 2005. URL http://www.cs.pdx.edu/ sheard.
• 34: P.F. Silva and J.N. Oliveira. Report on the design of a Galculator. Technical Report FAST:08.01, CCTC Research Centre, University ofMinho, 2008.
• 35: P.F. Silva, J.C. Almeida, and J.N. Oliveira. Galculator meets Coq. Technical report, CCTC, University of Minho, 2008. (In preparation).
• 36: J. M. Spivey, The Z notation: a reference manual, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 37: A. Tarski and S. Givant. A Formalization of Set Theory without Variables. American Mathematical Society, 1987. AMS Colloquium Publications, volume 41, Providence, Rhode Island.
• 38: D. Turner. A new implementation technique for applicative languages. Software-Practice & Experience, 9:31--49, 1979.
• 39: Eelco Visser, Stratego: A Language for Program Transformation Based on Rewriting Strategies, Proceedings of the 12th International Conference on Rewriting Techniques and Applications, p.357-362, May 22-24, 2001
• 40: E. Visser and Z. Benaissa. A Core Language for Rewriting. In C. Kirchner and H. Kirchner, editors, WRLA'98, volume 15 of ENTCS, Pont-à-Mousson, France, September 1998. Elsevier Science.
• 41: Philip Wadler, Comprehending monads, Proceedings of the 1990 ACM conference on LISP and functional programming, p.61-78, June 27-29, 1990, Nice, France [doi>10.1145/91556.91592]
• 42: Philip Wadler, Theorems for free!, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.347-359, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99404]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming

General Terms:
Design, Languages, Theory, Verification

Keywords:
DSL, GADT, Galois connections, haskell, point-free notation, proof assistant