Soft linear logic ([Lafont02]) is a subsystem of linear logic characterizing the class PTIME. We introduce Soft lambda- calculus as a calculus typable in the intuitionistic and affine variant of this logic. We prove t...
详细信息
ISBN:
(纸本)3540212981
Soft linear logic ([Lafont02]) is a subsystem of linear logic characterizing the class PTIME. We introduce Soft lambda- calculus as a calculus typable in the intuitionistic and affine variant of this logic. We prove that the (untyped) terms of this calculus are reducible in polynomial time. We then extend the type system of Soft logic with recursive types. this allows us to consider non-standard types for representing lists. Using these datatypes we examine the concrete expressiveness of Soft lambda-calculus withthe example of the insertion sort algorithm.
Message sequence charts (MSC) are a graphical language for the description of communication scenarios between asynchronous processes. Our starting point is to model systems using an assume-guarantee formalism, in the ...
详细信息
ISBN:
(纸本)3540212981
Message sequence charts (MSC) are a graphical language for the description of communication scenarios between asynchronous processes. Our starting point is to model systems using an assume-guarantee formalism, in the style of LSCs and Triggered MSCs. We enrich MSCs withthe possibility of using gaps (template MSC), and show their ex-pressivity. this formalism also allows to express logical formulas. We analyze the model-checking problem, whose complexity is linear in the size of the system, and ranges from PTIME to EXPSPACE in the size of the template formula.
it is generally thought that reasoning about programs in memory safe, garbage collected languages is much easier than in languages where the programmer has more explicit control over memory. Paradoxically, existing pr...
it is generally thought that reasoning about programs in memory safe, garbage collected languages is much easier than in languages where the programmer has more explicit control over memory. Paradoxically, existing program logics are based on a low-level view of storage that is sensitive to the presence or absence of unreachable cells, and Reynolds has pointed out that the Hoare triples derivable in these logics are even incompatible with garbage collection. We present a study of a small language whose operational semantics includes a rule for reclaiming garbage. Our main results include an analysis of propositions that are garbage insensitive, and full abstraction results connecting partial and total correctness to two natural notions of observational equivalence between programs. (C) 2002 Elsevier science B.V. All rights reserved.
the shared dataspace metaphor is historically the most prominent representative of the family of coordination models. According to this approach, concurrent processes interact via the production, consumption, and test...
详细信息
the shared dataspace metaphor is historically the most prominent representative of the family of coordination models. According to this approach, concurrent processes interact via the production, consumption, and test for presence/absence of data in a common repository. Recently, the problem of the accumulation of outdated and unwanted information in the shared repository has been addressed. Typical garbage collection algorithms cannot be adopted in this context because there is no notion of unaccessible data. the most promising solution to this problem consists of the introduction of the notion of temporary data, intended as data with an associated expiration time. In this paper, we investigate the impact of different mechanisms for expired data collection on the expressiveness of shared dataspace coordination systems with temporary data. (C) 2002 Elsevier science B.V. All rights reserved.
the shared dataspace metaphor is historically the most prominent representative of the family of coordination models. According to this approach, concurrent processes interact via the production, consumption, and test...
详细信息
the shared dataspace metaphor is historically the most prominent representative of the family of coordination models. According to this approach, concurrent processes interact via the production, consumption, and test for presence/absence of data in a common repository. Recently, the problem of the accumulation of outdated and unwanted information in the shared repository has been addressed. Typical garbage collection algorithms cannot be adopted in this context because there is no notion of unaccessible data. the most promising solution to this problem consists of the introduction of the notion of temporary data, intended as data with an associated expiration time. In this paper, we investigate the impact of different mechanisms for expired data collection on the expressiveness of shared dataspace coordination systems with temporary data. (C) 2002 Elsevier science B.V. All rights reserved.
it is generally thought that reasoning about programs in memory safe, garbage collected languages is much easier than in languages where the programmer has more explicit control over memory. Paradoxically, existing pr...
详细信息
it is generally thought that reasoning about programs in memory safe, garbage collected languages is much easier than in languages where the programmer has more explicit control over memory. Paradoxically, existing program logics are based on a low-level view of storage that is sensitive to the presence or absence of unreachable cells, and Reynolds has pointed out that the Hoare triples derivable in these logics are even incompatible with garbage collection. We present a study of a small language whose operational semantics includes a rule for reclaiming garbage. Our main results include an analysis of propositions that are garbage insensitive, and full abstraction results connecting partial and total correctness to two natural notions of observational equivalence between programs. (C) 2002 Elsevier science B.V. All rights reserved.
the proceedings contain 25 papers. the special focus in this conference is on Static Analysis, Dynamic Systems, Abstract Interpretation, Model Checking and Security Protocols. the topics include: software model checki...
ISBN:
(纸本)9783540003489
the proceedings contain 25 papers. the special focus in this conference is on Static Analysis, Dynamic Systems, Abstract Interpretation, Model Checking and Security Protocols. the topics include: software model checking with abstraction refinement;model-checking and abstraction to the aid of parameterized systems;automatic verification by abstract interpretation;abstract interpretation-based certification of assembly code;property checking driven abstract interpretation-based static analysis;complexity of nesting analysis in mobile ambients;types for evolving communication in safe ambients;abstraction of expectation functions using Gaussian distributions;efficient verification of timed automata with BDD-like data-structures;bisimulation and unwinding for verifying possibilistic security properties;formal verification of the horn-preneel micropayment protocol;action refinement from a logical point of view;reasoning about layered message passing systems;using simulated execution in verifying distributed algorithms;efficient computation of recurrence diameters and shape analysis through predicate abstraction and model checking.
We develop a system of type assignment with intersection types, union types, indexed types, and universal and existential dependent types that is sound in a call-by-value functional language. the combination of logica...
详细信息
暂无评论