Refine
Year of publication
Document Type
- Working Paper (114) (remove)
Language
- English (114) (remove)
Has Fulltext
- yes (114)
Is part of the Bibliography
- no (114) (remove)
Keywords
- Lambda-Kalkül (18)
- Formale Semantik (10)
- Operationale Semantik (8)
- Programmiersprache (7)
- lambda calculus (7)
- Nebenläufigkeit (6)
- functional programming (6)
- concurrency (5)
- pi-calculus (5)
- semantics (5)
Institute
- Informatik (114) (remove)
Correctness of program transformations and translations in concurrent programming is the focus of our research. In this case study the relation of the synchronous pi-calculus and a core language of Concurrent Haskell (CH) with asynchronous communication is investigated. We show that CH embraces the synchronous pi-calculus. The formal foundations are contextual semantics in both languages, where may- as well as should-convergence are observed. We succeed in defining and proving smart properties of a particular translation mapping the synchronous pi-calculus into CH. This implies that pi-processes are error-free if and only if their translation is an error-free CH-program Our result shows that the chosen semantics is not only powerful, but can also be applied in concrete and technically complex situations. The developed translation uses private names. We also automatically check potentially correct translations that use global names instead of private names. As a complexity parameter we use the number of MVars introduced by the transformation, where MVars are synchronized 1-place buffers. The automated refutation of incorrect translations leads to a classification of potentially correct translations, and to the conjecture that one global MVar is insufficient.
Correctness of program transformations and translations in concurrent programming is the focus of our research. In this case study the relation of the synchronous pi-calculus and a core language of Concurrent Haskell (CH) with asynchronous communication is investigated. We show that CH embraces the synchronous pi-calculus. The formal foundations are contextual semantics in both languages, where may- as well as should-convergence are observed. We succeed in defining and proving smart properties of a particular translation mapping the synchronous pi-calculus into CH. This implies that pi-processes are error-free if and only if their translation is an error-free CH-program Our result shows that the chosen semantics is not only powerful, but can also be applied in concrete and technically complex situations. The developed translation uses private names. We also automatically check potentially correct translations that use global names instead of private names. As a complexity parameter we use the number of MVars introduced by the transformation, where MVars are synchronized 1-place buffers. The automated refutation of incorrect translations leads to a classification of potentially correct translations, and to the conjecture that one global MVar is insufficient.
Correctness of program transformations and translations in concurrent programming is the focus of our research. In this case study the relation of the synchronous pi-calculus and a core language of Concurrent Haskell (CH) with asynchronous communication is investigated. We show that CH embraces the synchronous pi-calculus. The formal foundations are contextual semantics in both languages, where may- as well as should-convergence are observed. We succeed in defining and proving smart properties of a particular translation mapping the synchronous pi-calculus into CH. This implies that pi-processes are error-free if and only if their translation is an error-free CH-program Our result shows that the chosen semantics is not only powerful, but can also be applied in concrete and technically complex situations. The developed translation uses private names. We also automatically check potentially correct translations that use global names instead of private names. As a complexity parameter we use the number of MVars introduced by the transformation, where MVars are synchronized 1-place buffers. The automated refutation of incorrect translations leads to a classification of potentially correct translations, and to the conjecture that one global MVar is insufficient.
We investigate translations from the synchronous pi-calculus
into a core language of Concurrent Haskell (CH). Synchronous messagepassing of the pi-calculus is encoded as sending messages and adding synchronization using Concurrent Haskell’s mutable shared-memory locations (MVars). Our correctness criterion for translations is invariance of may- and should-convergence. This embraces that all executions of a process are error-free if and only if this also holds for the translated program. We exhibit a particular correct translation that uses a fresh, private MVar per communication interaction and that is in addition adequate, and which is also fully abstract on closed expressions. A metaresult is that CH has the expressive power and the concurrency capabilities of the synchronous pi-calculus.
We also automatically check variants of translations of synchronous communication into an asynchronous calculus where only an a priori fixed number of MVars per channel (and not per communication interaction!) is available. We obtain non-correctness results for classes of small translations, and exemplary argue for the correctness (and adequacy) for two translations with a higher number of MVars. We introduce a classification of the potentially correct translations.
We consider matching, rewriting, critical pairs and the Knuth-Bendix confluence test on rewrite rules in a nominal setting extended by atom-variables. Computing critical pairs is done using nominal unification, and rewriting using nominal matching. We utilise atom-variables to formulate rewrite rules, which is an improvement over previous approaches, using usual nominal unification, nominal matching and nominal equivalence of expressions coupled with a freshness constraint. We determine the complexity of several problems in a quantified freshness logic. In particular we show that nominal matching is Πp2-complete. We prove that the adapted Knuth-Bendix confluence test is applicable to a nominal rewrite system with atom-variabes and thus, that there is a decidable test whether confluence of the ground instance of the abstract rewrite system holds. We apply the nominal Knuth Bendix confluence criterion to the theory of monads, and compute a convergent nominal rewrite system modulo alpha-equivalence.
A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in non-deterministic polynomial time. We also explore specializations like nominal letrec-matching for expressions, for DAGs, and for garbage-free expressions and determine their complexity. As extension a nominal unification algorithm for higher-order expressions with recursive let and atom-variables is constructed, where we show that it also runs in non-deterministic polynomial time.
Our recently developed LRSX Tool implements a technique to automatically prove the correctness of program transformations in higher-order program calculi which may permit recursive let-bindings as they occur in functional programming languages. A program transformation is correct if it preserves the observational semantics of programs- In our tool the so-called diagram method is automated by combining unification, matching, and reasoning on alpha-renamings on the higher-order metalanguage, and automating induction proofs via an encoding into termination problems of term rewrite systems. We explain the techniques, we illustrate the usage of the tool, and we report on experiments.
The focus of this paper are space-improvements of programs, which are transformations that do not worsen the space requirement during evaluations. A realistic theoretical treatment must take garbage collection method into account. We investigate space improvements under the assumption of an optimal garbage collector. Such a garbage collector is not implementable, but there is an advantage: The investigations are independent of potential changes in an implementable garbage collector and our results show that the evaluation and other similar transformations are space-improvements.
We explore space improvements in LRP, a polymorphically typed call-by-need functional core language. A relaxed space measure is chosen for the maximal size usage during an evaluation. It Abstracts from the details of the implementation via abstract machines, but it takes garbage collection into account and thus can be seen as a realistic approximation of space usage. The results are: a context lemma for space improving translations and for space equivalences; all but one reduction rule of the calculus are shown to be space improvements, and the exceptional one, the copy-rule, is shown to increase space only moderately.
Several further program transformations are shown to be space improvements or space equivalences, in particular the translation into machine expressions is a space equivalence. These results are a step Forward in making predictions about the change in runtime space behavior of optimizing transformations in callbyneed functional languages.
We explore space improvements in LRP, a polymorphically typed call-by-need functional core language. A relaxed space measure is chosen for the maximal size usage during an evaluation. It Abstracts from the details of the implementation via abstract machines, but it takes garbage collection into account and thus can be seen as a realistic approximation of space usage. The results are: a context lemma for space improving translations and for space equivalences; all but one reduction rule of the calculus are shown to be space improvements, and the exceptional one, the copy-rule, is shown to increase space only moderately.
Several further program transformations are shown to be space improvements or space equivalences, in particular the translation into machine expressions is a space equivalence. These results are a step Forward in making predictions about the change in runtime space behavior of optimizing transformations in callbyneed functional languages.