ﻻ يوجد ملخص باللغة العربية
A rigid loop is a for-loop with a counter not accessible to the loop body or any other part of a program. Special instructions for rigid loops are introduced on top of the syntax of the program algebra PGA. Two different semantic projections are provided and proven equivalent. One of these is taken to have definitional status on the basis of two criteria: `normative semantic adequacy and `indicative algorithmic adequacy.
Constraint Handling Rules (CHR) are a committed-choice declarative language which has been designed for writing constraint solvers. A CHR program consists of multi-headed guarded rules which allow one to rewrite constraints into simpler ones until a
We propose a general proof technique to show that a predicate is sound, that is, prevents stuck computation, with respect to a big-step semantics. This result may look surprising, since in big-step semantics there is no difference between non-termina
We make a formal analogy between random sampling and fresh name generation. We show that quasi-Borel spaces, a model for probabilistic programming, can soundly interpret Starks $ u$-calculus, a calculus for name generation. Moreover, we prove that th
It is well-known that big-step semantics is not able to distinguish stuck and non-terminating computations. This is a strong limitation as it makes very difficult to reason about properties involving infinite computations, such as type soundness, whi
It has been an open question as to whether the Modular Structural Operational Semantics framework can express the dynamic semantics of call/cc. This paper shows that it can, and furthermore, demonstrates that it can express the more general delimited control operators control and shift.