An Axiomatization of Arrays for Kleene Algebra with Tests

1. More, T.: Axioms and theorems for a theory of arrays. IBM J. Res. Dev. 17(2), 135–175 (1973)

   Article  MathSciNet  MATH  Google Scholar 

2. Downey, P.J., Sethi, R.: Assignment commands with array references. J. ACM 25(4), 652–666 (1978)

   Article  MathSciNet  MATH  Google Scholar 

3. McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress, pp. 21–28 (1962)

   Google Scholar 

4. McCarthy, J., Painter, J.: Correctness of a compiler for arithmetic expressions. In: Schwartz, J.T. (ed.) Proceedings Symposium in Applied Mathematics, 19th edn. Mathematical Aspects of Computer Science, pp. 33–41. American Mathematical Society, Providence, RI (1967)

   Google Scholar 

5. Hoare, C.A.R., Wirth, N.: An axiomatic definition of the programming language PASCAL. Acta Informatica 2(4), 335–355 (1973)

   Article  Google Scholar 

6. Power, A.J., Shkaravska, O.: From comodels to coalgebras: State and arrays. Electr. Notes Theor. Comput. Sci. 106, 297–314 (2004)

   Article  MathSciNet  Google Scholar 

7. Bornat, R.: Proving pointer programs in Hoare logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 102–126. Springer, Heidelberg (2000)

   Chapter  Google Scholar 

8. Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: Logic in Computer Science, pp. 29–37 (2001)

   Google Scholar 

9. Collins, G., Syme, D.: A theory of finite maps. In: Schubert, E.T., Alves-Foss, J., Windley, P. (eds.) HUG 1995. LNCS, vol. 971, pp. 122–137. Springer, Heidelberg (1995)

   Google Scholar 

10. Kozen, D.: Kleene algebra with tests. Transactions on Programming Languages and Systems 19(3), 427–443 (1997)

    Article  Google Scholar 

11. Angus, A., Kozen, D.: Kleene algebra with tests and program schematology. Technical Report 2001-1844, Computer Science Department, Cornell University (2001)

    Google Scholar 

12. Barth, A., Kozen, D.: Equational verification of cache blocking in LU decomposition using Kleene algebra with tests. Technical Report 2002-1865, Computer Science Department, Cornell University (2002)

    Google Scholar 

13. Cohen, E.: Lazy caching in Kleene algebra 22581 (1994), http://citeseer.nj.nec.com/22581.html

14. Cohen, E.: Hypotheses in Kleene algebra. Technical Report TM-ARH-023814, Bellcore (1993)

    Google Scholar 

15. Cohen, E.: Using Kleene algebra to reason about concurrency control. Technical report, Telcordia, Morristown, N.J (1994)

    Google Scholar 

16. Kozen, D., Patron, M.-C.: Certification of compiler optimizations using Kleene algebra with tests. In: Lloyd, J., Dahl, V., Furbach, U., Kerber, M., Lau, K.K., Palamidessi, C., Pereira, L.M., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 568–582. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

17. Kozen, D.: On Hoare logic and Kleene algebra with tests. Trans. Computational Logic 1(1), 60–76 (2000)

    Article  MathSciNet  Google Scholar 

18. Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Shannon, C.E., McCarthy, J. (eds.) Automata Studies, pp. 3–41. Princeton University Press, Princeton (1956)

    Google Scholar 

19. Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall, London (1971)

    MATH  Google Scholar 

20. Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Infor. and Comput. 110(2), 366–390 (1994)

    Article  MathSciNet  MATH  Google Scholar 

21. Fischer, M.J., Ladner, R.E.: Propositional modal logic of programs. In: Proc. 9th Symp. Theory of Comput., ACM, pp. 286-294 (1977)

    Google Scholar 

22. Aboul-Hosn, K., Kozen, D.: KAT-ML: An interactive theorem prover for Kleene algebra with tests. In: Proc. 4th Int. Workshop on the Implementation of Logics, University of Manchester, pp. 2–12 (2003)

    Google Scholar 

23. Aboul-Hosn, K.: An axiomatization of arrays for Kleene algebra with tests. Technical report, Cornell University (2006)

    Google Scholar 

24. Filliâtre, J.C., Magaud, N.: Certification of sorting algorithms in the Coq system. In: Theorem Proving in Higher Order Logics: Emerging Trends (1999)

    Google Scholar 

25. Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. The MIT Electrical Engineering and Computer Science Series. MIT Press/McGraw Hill, Cambridge (1990)

    Google Scholar 

26. Aboul-Hosn, K., Kozen, D.: KAT-ML: An interactive theorem prover for Kleene algebra with tests. Journal of Applied Non-Classical Logics 16(1) (2006)

    Google Scholar 

Download references