Names and name-binding are useful concepts in the theory and practice of formal systems. In this thesis we study them in the context of dependent type theory. We propose a novel dependent type theory with primitives f...
Names and name-binding are useful concepts in the theory and practice of formal systems. In this thesis we study them in the context of dependent type theory. We propose a novel dependent type theory with primitives for the explicit handling of names. As the main application, we consider programming and reasoning with abstract syntax involving variable binders. Gabbay and Pitts have shown that Fraenkel Mostowski (FM) set theory models a notion of name using which informal work with names and binding can be made precise. They have given a number of useful constructions for working with names and binding, such as a syntax-independent notion of freshness that formalises when two objects do not share names, and a freshness quantifier that simplifies working with names and binding. Related to FM set theory, a number of systems for working with names have been given, among them are the first-order Nominal logic, the higher-order logic FM-HOL, the theory of Contexts as well as the programming language FreshML. In this thesis we study how dependent type theory can be extended with primitives for working with names and binding. Our choice of primitives is different from that in FM set theory. In FM set theory the fundamental primitive for working with names is swapping. All other concepts such as -equivalence classes and binding are constructed from it. For dependent type theory, however, this approach of constructing everything from swapping is not ideal, since it requires us to make strong assumptions on the type theory. For instance, the construction of -equivalence classes from swapping appears to require quotient types. Our approach is to treat constructions such as -equivalence classes and name-binding directly, turning them into primitives of the type theory. To do this, it is convenient to take freshness rather than swapping as the fundamental primitive. Based on the close correspondence between type theories and categories, we approach the design of the dependent ty
By introducing the Regular Membership Constraint, Gilles Pesant pioneered the idea of basing constraints on formal languages. The paper presented here is highly motivated by this work, taking the obvious next step, na...
详细信息
ISBN:
(纸本)3540462678
By introducing the Regular Membership Constraint, Gilles Pesant pioneered the idea of basing constraints on formal languages. The paper presented here is highly motivated by this work, taking the obvious next step, namely to investigate constraints based on grammars higher up in the Chomsky hierarchy. We devise an arc-consistency algorithm for context-free grammars, investigate when logic combinations of grammar constraints are tractable, show how to exploit non-constant size grammars and reorderings of languages, and study where the boundaries run between regular, context-free, and context-sensitive grammar filtering.
In this paper, we propose a new technique for the verification of concurrent multi-threaded programs. In general, the problem is known to be undecidable even for programs with just two threads [1]. However, we exploit...
详细信息
ISBN:
(纸本)0769526314
In this paper, we propose a new technique for the verification of concurrent multi-threaded programs. In general, the problem is known to be undecidable even for programs with just two threads [1]. However, we exploit the observation that, in practice, a large fraction of concurrent programs can either be modeled as Pushdown Systems communicating solely using locks or can be reduced to such systems by applying. standard abstract interpretation techniques or by exploiting separation of data from control. Moreover, standard programmingpractice guidelines typically recommend that programs use locks in a nestedfashion. Infact, in languages like Java and C#, locks are guaranteed to be nested. For such a fi-amework, we show, by using the new concept of Lock Constrained Multi-Automata Pair (LMAP), that pre* -closures of regular sets of states can be computed efficiently. This is accomplished by reducing the pre* -closure computation for a regular set of states of a concurrent program with nested locks to those for its individual threads. Leveraging this new technique then allows us to formulate a fully automatic, efficient and exact (sound and complete) decision procedure for model checking threads communicating via nested locks for indexed linear-time temporal logicfonnulae.
We introduce a constraint-based framework for studying infinite qualitative simulations concerned with contingencies such as time, space, shape, size, abstracted into a finite set of qualitative relations. To define t...
详细信息
ISBN:
(纸本)3540462678
We introduce a constraint-based framework for studying infinite qualitative simulations concerned with contingencies such as time, space, shape, size, abstracted into a finite set of qualitative relations. To define the simulations we combine constraints that formalize the background knowledge concerned with qualitative reasoning with appropriate inter-state constraints that are formulated using linear temporal logic. We implemented this approach in a constraint programming system ((ECLPSe)-P-i) by drawing on the ideas from bounded model checking. The implementation became realistic only after several rounds of optimizations and experimentation with various heuristics. The resulting system allows us to test and modify the problem specifications in a straightforward way and to combine various knowledge aspects. To demonstrate the expressiveness and simplicity of this approach we discuss in detail two examples: a navigation problem and a simulation of juggling.
Ideally, programming propagators as implementations of constraints should be an entirely declarative specification process for a large class of constraints: a high-level declarative specification is automatically tran...
详细信息
ISBN:
(纸本)3540462678
Ideally, programming propagators as implementations of constraints should be an entirely declarative specification process for a large class of constraints: a high-level declarative specification is automatically translated into an efficient propagator. This paper introduces the use of existential monadic second-order logic as declarative specification language for finite set propagators. The approach taken in the paper is to automatically derive projection propagators (involving a single variable only) implementing constraints described by formulas. By this, the paper transfers the ideas of indexicals to finite set constraints while considerably increasing the level of abstraction available with indexicals. The paper proves soundness and completeness of the derived propagators and presents a run-time analysis, including techniques for efficiently executing projectors for n-ary constraints.
The language Timed Concurrent Constraint (tccp) is the extension over time of the Concurrent Constraint programming (cc) paradigm that allows us to specify concurrent systems where timing is critical, for example reac...
详细信息
Some type systems are first described formally, to be sometimes followed by an implementation. Other type systems are first implemented as language extensions, to be sometimes retrofitted with a formal description. In...
详细信息
We describe how the propagator for the ALL-DIFFERENT constraint can be generalized to prune variables whose domains are not just simple finite domains. We show, for example, how it can be used to propagate set variabl...
详细信息
ISBN:
(纸本)354034215X
We describe how the propagator for the ALL-DIFFERENT constraint can be generalized to prune variables whose domains are not just simple finite domains. We show, for example, how it can be used to propagate set variables, multiset variables and variables which represent tuples of values. We also describe how the propagator for the global cardinality constraint (which is a generalization of the ALL-DIFFERENT constraint) can be generalized in a similar way. Experiments show that such propagators can be beneficial in practice, especially when the domains are large.
The proceedings contain 33 papers. The topics discussed include: weighted pushdown systems and trust management systems;automatic verification of parameterized data structures;parameterized verification of π calculus...
详细信息
ISBN:
(纸本)3540330569
The proceedings contain 33 papers. The topics discussed include: weighted pushdown systems and trust management systems;automatic verification of parameterized data structures;parameterized verification of π calculus systems;easy parameterized verification of biphase mark and 8N1 protocols;evaluating the effectiveness of slicing for model reduction of concurrent object oriented programs;new metrics for static variable ordering in decision diagrams;widening ROBDDs with prime implicants;efficient guided symbolic reachability using reachability expressions;SAT - based software certification;exploration of the capabilities of constraint programming for software verification;efficient abstraction refinement in interpolation based unbounded model checking;and approximating predicate images for bit vector logic.
Pattern detection is part of many solutions to software engineering problems. Unfortunately, it is a hard problem in itself in both theory and practice. Both exact and approximative approaches have been used earlier t...
详细信息
Pattern detection is part of many solutions to software engineering problems. Unfortunately, it is a hard problem in itself in both theory and practice. Both exact and approximative approaches have been used earlier to increase efficiency. We propose a novel method to improve the performance of pattern detection, which is in many cases both exact and efficient. It is based on the idea of filtering information from the program representation (graphs), which is unnecessary for detecting a particular pattern. This makes the remaining program representation graph planar, in many cases, thus allowing for linear pattern detection. We evaluate our approach experimentally: we detect six design patterns in six software systems. Filtering leads to planar program representation graphs in 14 out of 36 cases. For most of the remaining graphs, filtering makes the graphs almost planar and gives a significant reduction of the graph size, which speeds up existing heuristics.
暂无评论