Refine
Year of publication
Document Type
- Working Paper (59)
- Conference Proceeding (2)
- Article (1)
- Diploma Thesis (1)
- Report (1)
Has Fulltext
- yes (64)
Is part of the Bibliography
- no (64)
Keywords
- Lambda-Kalkül (14)
- Formale Semantik (10)
- lambda calculus (7)
- Nebenläufigkeit (6)
- Operationale Semantik (6)
- functional programming (6)
- Programmiersprache (5)
- concurrency (5)
- pi-calculus (5)
- semantics (5)
- Logik (4)
- Verifikation (4)
- adequate translations (4)
- contextual equivalence (4)
- Funktionale Programmierung (3)
- context lemma (3)
- functional programming languages (3)
- observational semantics (3)
- Funktionale Programmiersprache (2)
- Kontextuelle Gleichheit (2)
- Logics (2)
- Pufferspeicher (2)
- Semantics (2)
- Verification (2)
- letrec (2)
- program transformation (2)
- verification (2)
- Abstrakte Reduktion (1)
- Abstrakter Automat (1)
- Alice ML (1)
- Alpha equivalence (1)
- Call-by-Need (1)
- Clean (1)
- Contextual Equivalence (1)
- Correctness (1)
- Futures (1)
- Haskell (1)
- Lambda Calculus (1)
- Letrec-Kalkül (1)
- ML <Programmiersprache> (1)
- Nichtdeterminismus (1)
- Operational Semantics (1)
- Program Transformations (1)
- Programmiersprachen (1)
- Programmkalküle (1)
- Programmkorrektheit (1)
- Reduktionssystem (1)
- Semantik (1)
- Sharing (1)
- Striktheitsanalyse (1)
- Termination (1)
- Terrmersetzungssystem (1)
- Umbenennung (1)
- abstract reduction (1)
- adequate translation (1)
- alpha renaming (1)
- automated deduction (1)
- bisimulation (1)
- call-by-need (1)
- correctness (1)
- deduction (1)
- formal semantics (1)
- matching (1)
- meta languages (1)
- nominal unification (1)
- non-determinism (1)
- nondeterminism (1)
- observational equivalence (1)
- program correctness (1)
- programming calculi (1)
- programming languages (1)
- relative termination (1)
- rewriting (1)
- rewriting systems (1)
- strictness analysis (1)
- string rewriting (1)
- termination (1)
- translation (1)
Institute
- Informatik (64)
This paper proves correctness of Nocker s method of strictness analysis, implemented for Clean, which is an e ective way for strictness analysis in lazy functional languages based on their operational semantics. We improve upon the work of Clark, Hankin and Hunt, which addresses correctness of the abstract reduction rules. Our method also addresses the cycle detection rules, which are the main strength of Nocker s strictness analysis. We reformulate Nocker s strictness analysis algorithm in a higherorder lambda-calculus with case, constructors, letrec, and a nondeterministic choice operator used as a union operator. Furthermore, the calculus is expressive enough to represent abstract constants like Top or Inf. The operational semantics is a small-step semantics and equality of expressions is defined by a contextual semantics that observes termination of expressions. The correctness of several reductions is proved using a context lemma and complete sets of forking and commuting diagrams. The proof is based mainly on an exact analysis of the lengths of normal order reductions. However, there remains a small gap: Currently, the proof for correctness of strictness analysis requires the conjecture that our behavioral preorder is contained in the contextual preorder. The proof is valid without referring to the conjecture, if no abstract constants are used in the analysis.
Motivated by the question of correctness of a specific implementation of concurrent buffers in the lambda calculus with futures underlying Alice ML, we prove that concurrent buffers and handled futures can correctly encode each other. Correctness means that our encodings preserve and reflect the observations of may- and must-convergence. This also shows correctness wrt. program semantics, since the encodings are adequate translations wrt. contextual semantics. While these translations encode blocking into queuing and waiting, we also provide an adequate encoding of buffers in a calculus without handles, which is more low-level and uses busy-waiting instead of blocking. Furthermore we demonstrate that our correctness concept applies to the whole compilation process from high-level to low-level concurrent languages, by translating the calculus with buffers, handled futures and data constructors into a small core language without those constructs.
Various concurrency primitives have been added to sequential programming languages, in order to turn them concurrent. Prominent examples are concurrent buffers for Haskell, channels in Concurrent ML, joins in JoCaml, and handled futures in Alice ML. Even though one might conjecture that all these primitives provide the same expressiveness, proving this equivalence is an open challenge in the area of program semantics. In this paper, we establish a first instance of this conjecture. We show that concurrent buffers can be encoded in the lambda calculus with futures underlying Alice ML. Our correctness proof results from a systematic method, based on observational semantics with respect to may and must convergence.
Motivated by the question of correctness of a specific implementation of concurrent buffers in the lambda calculus with futures underlying Alice ML, we prove that concurrent buffers and handled futures can correctly encode each other. Correctness means that our encodings preserve and reflect the observations of may- and must-convergence, and as a consequence also yields soundness of the encodings with respect to a contextually defined notion of program equivalence. While these translations encode blocking into queuing and waiting, we also describe an adequate encoding of buffers in a calculus without handles, which is more low-level and uses busy-waiting instead of blocking. Furthermore we demonstrate that our correctness concept applies to the whole compilation process from high-level to low-level concurrent languages, by translating the calculus with buffers, handled futures and data constructors into a small core language without those constructs.