Prof. Dr. Zoltan Horvath

Proving properties of components of functional programs

Zum Vortrag:

The components of distributed applications run concurrently, and can collaborate with one another by not only synchronization and communication of data, but also by communication of mobile code. The correctness of programs written in a functional language can be proven more easily than that of programs written in the more widely used imperative languages. In a pure functional language, referential transparency allows many program properties to be proven by mathematical induction. The behaviour and the state changes of intricate distributed systems can be described without the violation of referential transparency in modern functional languages like Haskell, Clean, etc. Thus the proof and the verification of the safety properties and the invariants of such systems can be completed more easily. In a pure functional language like Clean the values of the functional variables are constants; variables of functional programs do not change in time. Hence it seems that temporality has no meaning in functional programs. However, in certain cases (e.g. in interactive or distributed programs, or in ones that use IO) we would like to consider a series of values computed from each other as different states of the same ``abstract object''. For this abstract object we can already prove temporal properties. Additionaly we propose a certified property carrying code model of safe mobile code exchange.

Zur Person:

Zoltan Horvath is associate professor at the Faculty of Informatics, University Eotvos Lorand, Budapest, Head of Department of Programming Languages and Compilers. He graduated and received his PhD in informatics at the same university. He is leader of research projects in functional and distributed computing, supported by the National Science Foundation of Hungary. He received also the Bolyai Research Fellowship of the Hungarian Academy of Sciences for the period 2003-2006. Zoltan Horvath is the network coordinator of the H-81 CEEPUS program, in which Uni. Klagenfurt and 6 other universities of Central Europe are involved.


Sprecher: Prof. Dr. Zoltan Horvath
Wann:     Freitag, 24. Oktober 2003, 15:30 Uhr (s.t.)
Wo:       HS 1, Universität Klagenfurt