Correctness of Distributed Functional Programs -- OTKA T037742

Contents

• Correctness of Distributed Functional Programs -- OTKA T037742
  • Contents
  • Abstract
  • People
  • Preliminary Results
  • Results
    • Papers
      • 2002
      • 2003
    • Software
      • 2003
      • 2007
    • Reports, Textbook Chapters, Notes
      • 2002
    • Thesis for National Scientific Students' Associations Conference
      • 2002
    • Thesis
      • 2002
      • 2003
    • Lectures, Example Programs
      • 2002
      • 2003
  • Related projects

Back to the top of this page

Abstract

Nowadays distributed systems form one of the most important research areas in informatics. The appearance of the Java programming language, the CORBA standard and other software tools made it possible to utilize the object-oriented software technology also in the development of distributed applications. Hence the design and implementation of distributed systems came into practice. The components of such 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.

Our goal is to extend mobile code (which is already equipped with certain type information) with further semantical information concerning its behaviour, and to make the run-time verification of those properties possible. We are going to let a proof system examine the code of a Clean program before sending it to another host, and to bundle the properties---and also the main steps of the proof of the properties---with the code. Thus the receiving party can easily and efficiently check whether the code indeed possesses the supposed properties, so it can be sure that the safety properties of some program components or of the whole distributed system will not be violated. In this research we have to define the appropriate programming language constructs that allow of the description of different safety properties, we have to develop the methodology of proving these properties, automating the proving process as much as possible, and checking the proofs during run-time.

Back to the top of this page

People

Back to the top of this page

Preliminary Results

• Csizmazia B.: Clean IIOP 0.3
  software
• Horváth Z. - Zsók V. - Serrarens, P. - Plasmeijer, R.: Parallel Functional Skeletons in Concurrent Clean.
  In Abstracts of the Third Joint Conference on Mathematics and Computer Science, Jun. 6-12, 1999, Visegrád. Hungary, p.37.
  abstract PS, PDF
• Harmat K. - Tandi P. - Horváth Z. - Wierich, M. - Plasmeijer, R.: Web Computing in Clean.
  In Proceedings of the 4th International Conference on Applied Informatics, Eger-Noszvaj, Hungary, Sept. 1999, 87-93.
  abstract PS, PDF (PDF version is in poor quality)
  software
• Horváth Z. - Achten, P. - Kozsik T. - Plasmeijer, R.: Verification of the Temporal Properties of Dynamic Clean Processes.
  Proceedings of Implementation of Functional Languages'99, Lochem, The Netherlands, Sept. 7-10, 1999. pp. 203-218.
  full article PS, PDF (PDF version is in poor quality)
• Horváth Z. - Achten, P. - Kozsik T. - Plasmeijer, R.: Proving the Temporal Properties of the Unique World.
  Proceedings of the Sixth Symposium on Programming Languages and Software Tools, Tallin, Estonia, August, 1999., pp. 113-125.
• Horváth Z. - Zsók V. - Serrarens, P. - Plasmeijer, R.: Parallel Functional Reactive Skeletons in Concurrent Clean
  Conference of PhD Students in Computer Science CSCS'2000, Volume of Extended Abstract, Szeged, Hungary, July 20-23, 2000, page 50.
  abstract PS, PDF (PDF version is in poor quality)
• Kozsik T. - van Arkel, D. - Plasmeijer, R.: Subtyping with Strengthening Type Invariants
  In: Mohnen, M., Koopman, P. eds. Proceedings of the 12th International Workshop on Implementation of Functional Languages, Aachener Informatik-Berichte, Aachen, Germany, September 2000. pp. 315-330.
  
• Varga Z.: Clean - Corba interface
  MSc Thesis, ELTE, Budapest, Hungary, 2000.
  software
  documentation (in Hungarian)
• Varga Z.: Haskell - Corba interface
  software
• Zsók V. - Horváth Z.: Skeleton Algorithms in Concurrent Clean.
  4th Joint Conference on Mathematics and Computer Science, Abstracts, Felix-Oradea, Romania, page 99, 2001.
  abstract PS, PDF (PDF version is in poor quality)
• Csempesz J.: Subtype Systems of Functional Languages
  MSc Thesis, ELTE, Budapest, Hungary, 2001.
  
• Hegedűs H.: Haskell to Clean Front End
  MSc Thesis, ELTE, Budapest, Hungary, 2001.
  
• Horváth Z. - Zsók V. - Serrarens, P. - Plasmeijer, R.: Parallel Elementwise Processing in Concurrent Clean.
  5th International Conference on Applied Informatics, Eger, Hungary, 2001 Selected paper of ICAI.2001 to appear in Computers & Mathematics With Applications, Elsevier, 2002.
  abstract PS, PDF

Back to the top of this page

Results

Papers

2002

• Horváth Z. - Kozsik T.: Safe Mobile Code (CPPCC): Certified Proven Property Carrying Code.
  16th European Conference on Object-Oriented Programming (ECOOP 2002), University of Málaga, Spain, June 10-14, 2002.
  
  • Resource Management for Safe Languages (Workshop #01)
  • The 8th ECOOP Workshop on Mobile Object Systems: New Frontiers (Workshop #18)
  extended abstract PS, PDF
  position paper PS, PDF (PDF version is in poor quality)
  
• Zsók V. - Horváth Z. - Tejfel M.: Parallel Functional Programming on Cluster.
  The Third Conference of PhD Students in Computer Science, CSCS'2002, Volume of Extended Abstract, Szeged, Hungary, July 1-4. 2002, page 114.
  extended abstract PS, PDF (PDF version is in poor quality)
• Csörnyei Z. - Nagy S.: Type Theory and Object Oriented Programming
  Informatics in the Hungarian Higher Education. Debrecen, Aug. 28-30, 2002.
  full article (in Hungarian) PS, PDF
• Hegedűs H. - Horváth Z. - Zsók V.: Comparative Analysis of Haskell and Clean
  Informatics in the Hungarian Higher Education. Debrecen, Aug. 28-30, 2002, pages 1075-1084.
  full article (in Hungarian) PS, PDF
• Horváth Z. - Tejfel M. - Pásztorné Varga K.: Verification of Functional Programs
  Informatics in the Hungarian Higher Education. Debrecen, Aug. 28-30, 2002, pages 942-946.
  full article (in Hungarian) PS, PDF
• Zsók V. - Horváth Z. - Tejfel M.: Parallel Functional Programming
  Informatics in the Hungarian Higher Education. Debrecen, Aug. 28-30, 2002, pages 1085-1094.
  full article (in Hungarian) PS, PDF
• Daxkobler K. - Horváth Z. - Kozsik T.: A Prototype of CPPCC - Safe Functional Mobile Code in Clean.
  Proceedings of Implementation of Functional Languages'02, Madrid, Spain, Sept. 15-19, 2002. pp. 301-310.
  full article PS, PDF (PDF version is in poor quality)
  slides PS, PDF
• Horváth Z. - Hernyák Z. - Kozsik T. - Tejfel M. - Ulbert A.: A Data Intensive Application on a Cluster - Parallel Elementwise Processing.
  In P. Kacsuk, D. Kranzlmüller, Zs. Nemeth, J. Volkert (Eds.): Distributed and Parallel System - Cluster and Grid Computing, Proc. 4th Austrian-Hungarian Workshop on Distributed and Parallel Systems, Kluwer Academic Publishers, The Kluwer International Series in Engineering and Computer Science, Vol. 706, pp. 46-53, Linz, Austria, September 29-October 2, 2002.
  abstract PS, PDF (PDF version is in poor quality)
  

Back to the top of this page

2003

• Horváth Z. - Kozsik T. - Tejfel M.: Proving Invariants of Functional Programs
  In Proceedings of Eighth Symposium on Programming Languages and Software Tools, Kuopio, Finland, June 17-18, 2003., pp. 115-126
  full article PS, PDF
  
• Horváth Z. - Varga Z. - Zsók V.: Clean-Corba Interface for Parallel Functional Programming on Clusters
  In Proceedings of Eighth Symposium on Programming Languages and Software Tools, Kuopio, Finland, June 17-18, 2003., pp. 127-136.
  full article PS, PDF
  
  Zsók V. - Horváth Z. - Varga Z.: Functional Programs on Clusters
  In: Striegnitz, Jörg; Davis, Kei (Eds.) (2003) Proceedings of the Workshop on Parallel/High-Performance Object-Oriented Scientific Computing (POOSC'03), Interner Bericht FZJ-ZAM-IB-2003-09, Juli 2003, pp. 93-100.
  position paper version of the previous article PS, PDF
  slides PS, PDF (PDF version is in poor quality)
  

Back to the top of this page

Software

2003

• Diviánszky P.: Haskell - Clean Compiler
  ELTE, Budapest, 2003.
  software
  Readme
• Simon J.: Clean Prelude
  ELTE, Budapest, 2003.
  software
  documentation PS, PDF

Back to the top of this page

2007

• Tejfel M., Kozsik T.: Proofs illustrating the applicability of the SIO model
  software
  

Back to the top of this page

Reports, Textbook Chapters, Notes

2002

• Csörnyei Z.: Implementation of Functional Programming Languages
  • λ-calculus
    lecture notes (in Hungarian) PS, PDF (PDF version is in poor quality)
  • Combinatory Logic
    lecture notes (in Hungarian) PS, PDF (PDF version is in poor quality)
  • Type theory
    lecture notes (in Hungarian) PS, PDF (PDF version is in poor quality)
• Horváth Z.: Analysis of Modal μ-calculus and ErlVer.
  full article (in Hungarian) PS, PDF (PDF version is in poor quality)
• Nyékyné Gaizler J. eds. Comparative Analysis of Programming Languages; Horváth Z.: Language Tools of Functional Languages(Chapter)
  Kiskapu Kiadó, Budapest, 2002.
• Kozsik T.: Assign predicates to subtype marks -- a case study
  Technical Report 2003-S01, ELTE, Budapest, Hungary, 2003.
  full article PS, PDF
• Tejfel M.: Property specification of Sparkle and its extension possibilities
  Technical Report 2003-S02, ELTE, Budapest, Hungary, 2003.
  full article PS, PDF

Back to the top of this page

Thesis for National Scientific Students' Associations Conference

2002

• Diviánszky P.: Syntactical Analiser with Combinators for Clean
  Scientific Students' Associations Conference, ELTE, Budapest, December, 2002.
  thesis (in Hungarian) PS, PDF
  software
• Ivicsics M.: The Dynamic Type System of Clean
  Scientific Students' Associations Conference, ELTE, Budapest, December, 2002.
  thesis (in Hungarian) PS, PDF (PDF version is in poor quality)
  
• Bárány V.: Breakable terms.
  Scientific Students' Associations Conference, ELTE, Budapest, December, 2002.
  thesis PS, PDF
  

Back to the top of this page

Thesis

2002

• Daxkobler K.: Prototype of CPPCC.
  MSc Thesis, ELTE, Budapest, Hungary, 2002.
  documentation (in Hungarian) PS, PDF (PDF version is in poor quality)

Back to the top of this page

2003

• Horváth Gy.: Resource Requirements for Functional Programs.
  MSc Thesis, ELTE, Budapest, Hungary 2003.
  MSc thesis PS, PDF (PDF version is in poor quality)
  
• Ivicsics M..: Review on Garbage Collecting Algorithms, Answer for a Practical Garbage Collection Problem.
  MSc Thesis, ELTE, Budapest, Hungary 2003.
  MSc thesis (in Hungarian) PS, PDF
  source code of the garbage collector
  
• Németh-Csóka D.: Haskell Monads. Applications of Monads.
  MSc Thesis, ELTE, Budapest, Hungary 2003.
  MSc thesis (in Hungarian) PS, PDF (PDF version is in poor quality)

Back to the top of this page

Lectures, Example Programs

2002

• Csörnyei Z.: Introduction to Type Theory
  slides PS, PDF
• Szabóné Nacsa R.: Introduction to Functional Programming
  workbook (in Hungarian) PS, PDF
  slides (in Hungarian) PS, PDF
• Smetsers, J.E.W.: Type Systems for Functional Programming
  abstract
• Verification of Distributed Functional Programs
  Information Hungary Weekend, March 21-24, 2002.
  slides (in Hungarian) PS, PDF
• Horváth Z.: CPPCC - The Certified Proven Property Code Architecture
  Institut für Informatik und Wirtschaftsinformatik, Universität Wien, Austria, May 8, 2002.
  slides PS, PDF (PDF version is in poor quality)
• Horváth Z.: CPPCC - Safe Functional Mobile Code
  System Software Group, Institut für Praktische Informatik, J. Kepler Universität Linz, Linz, Austria, July 10, 2002.
• Kozsik T.: Subtyping with Strengthening Type Invariants
  Summer School and Workshop on Generic Programming, St Anne's College, Oxford, UK. August 26-30 2002.
  slides PS, PDF
• Zsók V.: Concurrency Constructs of Functional Languages
  Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria, November, 2002.
  
• Zsók V.: Verified Mobile Code in Functional Environment
  Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria, December, 2002.
  

Back to the top of this page

2003

• Horváth Z.: Mobile Codes Written in Functional Languages, Their Semantical Properties, Proving Their Correctness.
  University of Szeged, Hungary, February 25, 2003.
  
• Horváth Z.: Temporal Properties and Safe Mobile Code.
  Erasmus guest lecture. University of Nijmegen, The Netherlands, March 26, 2003.
  
• Horváth Z.: Certified Mobile Functional Code.
  Ceepus guest lecture, Paisii Hilendarski University, Plovdiv, Bulgaria, June 17, 2003.
  
• Zsók V.: Parallel Language Elements in Functional Languages.
  Ceepus guest lecture, Paisii Hilendarski University, Plovdiv, Bulgaria, June 26, 2003.
  
• Horváth Z.: Proving Properties of Components of Functional Programs.
  University Innsbruck, Austria, July 4, 2003.
  

Back to the top of this page

Related projects

• The Clean project

Back to the top of this page

Magyar nyelvű oldalak

Last modified: Fri Feb 29 15:03:01 2008