排序方式: 共有18条查询结果,搜索用时 31 毫秒
1.
Mariangiola Dezani-Ciancaglini Elio Giovannetti 《Electronic Notes in Theoretical Computer Science》2001,50(2):83-116
There are essentially two ways of looking at the computational behaviours of λ-terms. One consists in putting the term within a context (possibly of λ-calculus extensions) and observing some properties (typically termination). The other consists in reducing the term until some meaningful information is obtained: this naturally leads to a tree representation of the information implicitly contained in the original term. The paper is an informal overview of the role played by Böhm's Theorem in these observations of terms. 相似文献
2.
Christopher Anderson Franco Barbanera Mariangiola Dezani-Ciancaglini Sophia Drossopoulou 《Electronic Notes in Theoretical Computer Science》2003,82(8):108
We adapt the aliasing constraints approach for designing a flexible typing of evolving objects. Types are singleton types (addresses of objects, as a matter of fact) whose relevance is mainly due to the sort of safety property they guarantee. In particular we provide a type system for an imperative object based calculus with delegation and which supports method and delegate overriding, addition, and removal. 相似文献
3.
4.
Ilaria Castellani Mariangiola Dezani-Ciancaglini Jorge A. Pérez 《Formal Aspects of Computing》2016,28(4):669-696
We present a comprehensive model of structured communications in which self-adaptation and security concerns are jointly addressed. More specifically, we propose a model of multiparty, self-adaptive communications with access control and secure information flow guarantees. In our model, multiparty protocols (choreographies) are described as global types; security violations occur when process implementations of protocol participants attempt to read or write messages of inappropriate security levels within directed exchanges. Such violations trigger adaptation mechanisms that prevent the violations to occur and/or to propagate their effect in the choreography. Our model is equipped with local and global adaptation mechanisms for reacting to security violations of different gravity; type soundness results ensure that the overall multiparty protocol is still correctly executed while the system adapts itself to preserve the participants’ security. 相似文献
5.
Gael Plantard Chlo Dezani Enrique Ribeiro Brice Reoyo‐Prats Vincent Goetz 《加拿大化工杂志》2021,99(1):142-152
Compared to more conventional techniques, advanced oxidation processes (AOP) hold significant promise in terms of elimination of organic (especially persistent) compounds and microorganisms (disinfection) in wastewater. If the objective is to power these processes using solar energy, we need to be able to manage the intermittency in the solar resource. This is an essential step for design and to ensure efficient operation of the treatment processes. As solar radiation is inherently variable due to day/night cycles, seasonal cycles, and weather meteorological conditions, solar AOP performances are difficult to establish using conventional measures. To address this gap, we carry out experimental campaigns under controlled conditions and develop modelling tools capable of describing dynamic‐mode photocatalytic degradation. Here we develop a way to capture the responses of a photoreactor subjected to various stresses, including irradiation conditions, via an LED panel. Using a model that considers the influence of UV flux density and pollutant concentration made, it was possible to represent photoreactor responses under different irradiation conditions and feeds (concentration or flow at the input). The ultimate objective is to study the photocatalytic capacity of the photoreactor under irradiation conditions simulating a real day of sunshine. 相似文献
6.
Franco Barbanera Mariangiola Dezani-Ciancaglini Ugo de’Liguoro 《Formal Aspects of Computing》2016,28(4):697-722
In the setting of session behaviours, we study an extension of the concept of compliance when a disciplined form of backtracking and of output skipping is present. After adding checkpoints to the syntax of session behaviours, we formalise the operational semantics via an LTS, and define natural notions of checkpoint compliance and sub-behaviour, which we prove to be both decidable. Then we extend the operational semantics with skips and we show the decidability of the obtained compliance. 相似文献
7.
Mariangiola Dezani-Ciancaglini Jerzy Tiuryn Pawe
Urzyczyn 《Information and Computation》1999,150(2):153
The main result of the paper is a constructive proof of the following equivalence: two pureλ-terms are observationally equivalent in the lazy concurrentλ-calculusiffthey have the same Lévy–Longo trees. An algorithm which allows to build a context discriminating any two pureλ-terms with different Lévy–Longo trees is described. It follows that contextual equivalence coincides with behavioural equivalence (bisimulation) as considered by Sangiorgi. Another consequence is that the discriminating power of concurrent lambda contexts is the same as that of Boudol–Laneve's contexts with multiplicities. 相似文献
8.
Livio Bioglio Mariangiola Dezani-Ciancaglini Paola Giannini Angelo Troina 《International Journal of Software and Informatics》2013,7(4):501-526
The calculus of looping sequences is a formalism for describing the evolution of biological systems by means of term rewriting rules. Here we enrich this calculus with a type discipline which preserves some biological properties deriving from the requirement of certain elements, and the repellency of others. In particular, the type system guarantees the soundness of the application of reduction rules with respect to the elements which are required (all requirements must be satisfied) and to the elements which are excluded (two elements which repel each other cannot occur in the same compartment). As an example, we model the possible interactions (and compatibility) of di?erent blood types with different antigens. The type system does not allow transfusion with incompatible blood types. 相似文献
9.
The method described in Ref. 1 does not always correctly establish the bonds between the variables. In fact, during the reduction to normal form of the -formula ((ty)(yy)) and of all those in which the same variable that is free in the left subformula of an application occurs bound in the right subformula, this variable is wrongly considered as bound. To prevent this, it is necessary to modify the levels assigned to the formulas in the -generation. We therefore give the correct -generation statements and the correct algorithm of the -generation.See Ref. 1. 相似文献
10.
Mariangiola Dezani-Ciancaglini Ugo de''Liguoro Adolfo Piperno 《Theoretical computer science》1996,170(1-2):83-128
The distinction between the conjunctive nature of non-determinism as opposed to the disjunctive character of parallelism constitutes the motivation and the starting point of the present work. λ-calculus is extended with both a non-deterministic choice and a parallel operator; a notion of reduction is introduced, extending β-reduction of the classical calculus. We study type assignment systems for this calculus, together with a denotational semantics which is initially defined constructing a set semimodel via simple types. We enrich the type system with intersection and union types, dually reflecting the disjunctive and conjunctive behaviour of the operators, and we build a filter model. The theory of this model is compared both with a Morris-style operational semantics and with a semantics based on a notion of capabilities. 相似文献