共查询到20条相似文献,搜索用时 12 毫秒
1.
Aiken Alexander Wimmers Edward L. Palsberg Jens 《Higher-Order and Symbolic Computation》1999,12(3):237-282
Many type inference and program analysis systems include notions of subtyping and parametric polymorphism. When used together, these two features induce equivalences that allow types to be simplified by eliminating quantified variables. Eliminating variables both improves the readability of types and the performance of algorithms whose complexity depends on the number of type variables. We present an algorithm for simplifying quantified types in the presence of subtyping and prove it is sound and complete for non-recursive and recursive types. We also show that an extension of the algorithm is sound but not complete for a type language with intersection and union types, as well as for a language of constrained types. 相似文献
2.
3.
Craig interpolation has become a versatile tool in formal verification, used for instance to generate program assertions that
serve as candidates for loop invariants. In this paper, we consider Craig interpolation for quantifier-free Presburger arithmetic (QFPA). Until recently, quantifier elimination was the only available interpolation method for this theory, which is, however,
known to be potentially costly and inflexible. We introduce an interpolation approach based on a sequent calculus for QFPA
that determines interpolants by annotating the steps of an unsatisfiability proof with partial interpolants. We prove our calculus to be sound and complete. We have extended the Princess theorem prover to generate interpolating proofs, and applied it to a large number of publicly available Presburger arithmetic
benchmarks. The results document the robustness and efficiency of our interpolation procedure. Finally, we compare the procedure
against alternative interpolation methods, both for QFPA and linear rational arithmetic. 相似文献
4.
The polymorphic environment calculus is a polymorphic lambda calculus which enables us to treat environments as first-class citizens. In the calculus, environments are formalized as explicit substitutions, and the substitutions are included in the set of terms of the calculus. First, we introduce an untyped environment calculus, and we present a semantics of the calculus as a translation into the lambda calculus. Second, we propose a polymorphic type system for the environment calculus based on Damas-Milner's ML-polymorphic type system. In ML, polymorphism is allowed only in let-expressions; in the polymorphic environment calculus, polymorphism is provided with environment compositions. We prove a subject-reduction theorem for the type system. Third, a type-inference algorithm is given to the polymorphic environment calculus, and we establish its soundness, termination, and principal-typing theorem. 相似文献
5.
Types for the Ambient Calculus 总被引:1,自引:0,他引:1
The ambient calculus is a concurrent calculus where the unifying notion of ambient is used to model many different constructs for distributed and mobile computation. We study a type system that describes several properties of ambient behavior. The type system allows ambients to be partitioned in disjoint sets (groups), according to the intended design of a system, in order to specify both the communication and the mobility behavior of ambients. 相似文献
6.
7.
Subtyping in first order object calculi is studied with respect to the logical semantics obtained by identifying terms that
satisfy the same set of predicates, as formalised through an assignment system. It is shown that equality in the full first
order ς-calculus is modelled by this notion, which in turn is included in a Morris-style contextual equivalence.
U. de’Liguoro’s research was partially supported by project PRIN’05 prot. 2005015785_003. 相似文献
8.
本文从Ideal的基本概念出发,研究了Ideal作为类型的语义模型所具有的性质.在类型的Ideal模型下,讨论了Garment中参数化多态类型和约束多态类型的语义.并在此基础上,证明了Garment中类型规则的语义可靠性. 相似文献
9.
Aarne Ranta 《Journal of Logic, Language and Information》1998,7(4):413-431
The aim of this study is to look at the the syntactic calculus of Bar-Hillel and Lambek, including semantic interpretation, from the point of view of constructive type theory. The syntactic calculus is given a formalization that makes it possible to implement it in a type-theoretical proof editor. Such an implementation combines formal syntax and formal semantics, and makes the type-theoretical tools of automatic and interactive reasoning available in grammar.In the formalization, the use of the dependent types of constructive type theory is essential. Dependent types are already needed in the semantics of ordinary Lambek calculus. But they also suggest some natural extensions of the calculus, which are applied to the treatment of morphosyntactic dependencies and to an analysis of selectional restrictions. Finally, directed dependent function types are introduced, corresponding to the types of constructive type theory.Two alternative formalizations are given: one using syntax trees, like Montague grammar, and one dispensing with them, like the theory called minimalistic by Morrill. The syntax tree approach is presented as the main alternative, because it makes it possible to embed the calculus in a more extensive Montague-style grammar. 相似文献
10.
11.
12.
This paper presents a type system for the calculus of Mobile Resources (MR) proposed by Godskesen et al. The type system is able to prevent undesirable border-crossing behaviour such as Trojan horses. This is achieved by combining the notion of group with a notion of security policy. Well-typed processes satisfy a safety property which is preserved under reduction. An algorithm is presented which computes the minimal security policy making a process well typed. 相似文献
13.
类型系统在分布式系统理论中有着非常重要的作用。在为π演算引入多态类型系统后,需要对新的环境下进程的等价关系进行研究。在多态类型系统下,环境只能得知进程中通道的抽象类型,而无法得知通道的具体类型,此时环境的区分能力被削弱,所得到的互模拟关系更为粗糙。本文在以往文献研究的基础上给出了多态π演算互模拟的一个公理系统,并证明了公理系统的一致性和完备性。 相似文献
14.
15.
《Information and Computation》1999,148(1):1-70
We introduce the spi calculus, an extension of the pi calculus designed for describing and analyzing cryptographic protocols. We show how to use the spi calculus, particularly for studying authentication protocols. The pi calculus (without extension) suffices for some abstract protocols; the spi calculus enables us to consider cryptographic issues in more detail. We represent protocols as processes in the spi calculus and state their security properties in terms of coarse-grained notions of protocol equivalence. 相似文献
16.
Jason Hickey Aleksey Nogin Xin Yu Alexei Kopylov 《Electronic Notes in Theoretical Computer Science》2007,174(5):79
It is well-known that adding reflective reasoning can tremendously increase the power of a proof assistant. In order for this theoretical increase of power to become accessible to users in practice, the proof assistant needs to provide a great deal of infrastructure to support reflective reasoning. In this paper we explore the problem of creating a practical implementation of such a support layer.Our implementation takes a specification of a logical theory (which is identical to how it would be specified if we were simply going to reason within this logical theory, instead of reflecting it) and automatically generates the necessary definitions, lemmas, and proofs that are needed to enable the reflected meta-reasoning in the provided theory.One of the key features of our approach is that the structure of a logic is preserved when it is reflected. In particular, all variables, including meta-variables, are preserved in the reflected representation. This also allows the preservation of proof automation—there is a structure-preserving one-to-one map from proof steps in the original logic to proof step in the reflected logic.To enable reasoning about terms with sequent context variables, we develop a principle for context induction, called teleportation.This work is fully implemented in the MetaPRL theorem prover. 相似文献
17.
Bounded existential types are a powerful language feature for modeling partial data abstraction and information hiding. However,
existentials do not mingle well with subtyping as found in current object-oriented languages: the subtyping relation is already
undecidable for very restrictive settings. 相似文献
18.
George H.L. Fletcher Catharine M. Wyss Edward L. Robertson Dirk Van Gucht 《Electronic Notes in Theoretical Computer Science》2006,150(2):37
Technologies for overcoming heterogeneities between autonomous data sources are key in the emerging networked world. In this paper we discuss the initial results of a formal investigation into the underpinnings of technologies for alleviating structural heterogeneity. At the core of structural heterogeneity is the data mapping problem: discovering effective mappings between structured representations of data. Automating the discovery of these mappings is one of the fundamental unsolved challenges for data interoperability, integration, and sharing. We introduce a novel data model and calculus for expressing data mappings between relational data sources, laying the ground for a better understanding of the data mapping problem. This research uncovers several new safety issues in data mapping languages. We discuss ongoing investigations of syntactic and semantic restrictions on the calculus to deal with these issues. 相似文献
19.
The calculus c serves as a general framework for representing contexts. Essential features are control over variable capturing and the freedom to manipulate contexts before or after hole filling, by a mechanism of delayed substitution. The context calculus c is given in the form of an extension of the lambda calculus. Many notions of context can be represented within the framework; a particular variation can be obtained by the choice of a pretyping, which we illustrate by three examples. 相似文献
20.
Maribel Fernndez Ian Mackie Jorge Sousa Pinto 《Electronic Notes in Theoretical Computer Science》2007,72(1):45
This paper presents a formalism for defining higher-order systems based on the notion of graph transformation (by rewriting or interaction). The syntax is inspired by the Combinatory Reduction Systems of Klop. The rewrite rules can be used to define first-order systems, such as graph or term-graph rewriting systems, Lafont's interaction nets, the interaction systems of Asperti and Laneve, the non-deterministic nets of Alexiev, or a process calculus. They can also be used to specify higher-order systems such as hierarchical graphs and proof nets of Linear Logic, or to specify the operational semantics of graph-based languages. 相似文献