waashk/dblp huggingface dataset:
a typed lambda calculus with intersection types. intersection types are well known to type theorists mainly for two reasons. firstly, they type all and only the strongly normalizable lambda terms. secondly, the intersection type operator is a meta-level operator, that is, there is no direct logical counterpart in the curry-howard isomorphism sense. in particular, its meta-level nature implies that it does not correspond to the intuitionistic conjunction. the intersection type system is naturally a type inference system (system a la curry), but the meta-level nature of the intersection operator does not allow to easily design an equivalent typed system (system a la church). there are many proposals in the literature to design such systems, but none of them gives an entirely satisfactory answer to the problem. in this paper, we will review the main results in the literature both on the logical interpretation of intersection types and on proposed typed lambda calculi. the core of this paper is a new proposal for a true intersection typed lambda calculus, without any meta-level notion. namely, any typable term (in the intersection type inference) has a corresponding typed term (which is the same as the untyped term by erasing the type decorations and the typed term constructors) with the same type, and vice versa. the main idea is to introduce a relevant parallel term constructor which corresponds to the intersection type constructor, in such a way that terms in parallel share the same resources, that is, the same context of free typed variables. three rules allow us to generate all typed terms. the first two rules, application and lambda-abstraction, are performed on all the components of a parallel term in a synchronized way. finally, via the third rule of local renaming, once a free typed variable is bounded by lambda-abstraction, each of the terms in parallel can do its local renaming, with type refinement, of that particular resource.
towards the range property for the lambda theory h. a sketch of the proof is given for an open problem, the range property forh: the range of a closed @l-term in the closed term model modulo @b-conversion and equating unsolvable terms is either a singleton or infinite. the proof depends on one unresolved technical conjecture.
the weak lambda calculus as a reasonable machine. we define a new cost model for the call-by-value lambda-calculus satisfying the invariance thesis. that is, under the proposed cost model, turing machines and the call-by-value lambda-calculus can simulate each other within a polynomial time overhead. the model only relies on combinatorial properties of the usual beta-reduction, without any reference to a specific machine or evaluator. in particular, the cost of a single beta reduction is proportional to the difference between the size of the redex and the size of the reduct. in this way, the total cost of normalizing a lambda term will take into account the size of all intermediate results (as well as the number of steps to normal form).
on strong normalization and type inference in the intersection type discipline. we introduce a new unification procedure for the type inference problem in the intersection type discipline. it is well known that type inference in this case should succeed exactly for the strongly normalizing expressions. we give a proof for the strong normalization result in the intersection type discipline, which we obtain by putting together some well-known results and proof techniques. our proof uses a variant of klop's extended @l-calculus, for which it is shown that strong normalization is equivalent to weak normalization. this is proved here by means of a finiteness of developments theorem, obtained following de vrijer's combinatory technique. the main property of this extended calculus is uniformity, i.e. weak and strong normalizabilities coincide. the strong normalizability result is therefore a consequence of the fact, first established by coppo and dezani (for the @l-calculus) that typability implies weak normalizability. we then show that the unification process which is the basis for type inference exactly corresponds to reduction in the extended @l-calculus. finally we show that our notion of unification allows us to compute a principal typing for any typable @l-expression.
characterizing strong normalization in the curien-herbelin symmetric lambda calculus: extending the coppo-dezani heritage. we develop an intersection type system for the @l@?@m@m@? calculus of curien and herbelin. this calculus provides a symmetric computational interpretation of classical sequent style logic and gives a simple account of call-by-name and call-by-value. the present system improves upon earlier type disciplines for @l@?@m@m@?: in addition to characterizing the @l@?@m@m@? expressions that are strongly normalizing under free (unrestricted) reduction, the system enjoys the subject reduction and the subject expansion properties.
role-based access control for boxed ambients. our society is increasingly moving towards richer forms of information exchange where mobility of processes and devices plays a prominent role. this tendency has prompted the academic community to study the security problems arising from such mobile environments, and in particular, the security policies regulating who can access the information in question. in this paper we describe a calculus for mobile processes and propose a mechanism for specifying access privileges based on a combination of the identity of the users seeking access, their credentials, and the location from which they seek it, within a reconfigurable nested structure. we define baci"r, a boxed ambient calculus extended with a distributed role-based access control mechanism where each ambient controls its own access policy. a process in baci"r is associated with an owner and a set of activated roles that grant permissions for mobility and communication. the calculus includes primitives to activate and deactivate roles. the behavior of these primitives is determined by the process's owner, its current location and its currently activated roles. we consider two forms of security violations that our type system prevents: (1) attempting to move into an ambient without having the authorizing roles granting entry activated and (2) trying to use a communication port without having the roles required for access activated. we accomplish (1) and (2) by giving a static type system, an untyped transition semantics, and a typed transition semantics. we then show that a well-typed program never violates the dynamic security checks.
lambda calculus with patterns. in this paper we revisit the @l-calculus with patterns, originating from the practice of functional programming language design. we treat this feature in a framework ranging from pure @l-calculus to orthogonal combinatory reduction systems.
computability and the morphological complexity of some dynamics on continuous domains. the partially ordered set of compact intervals provides a convenient embedding space for the analysis of some dynamical systems. crucial dynamical properties are transferred to it, while allowing an investigation of stability and chaoticity, in terms of computability, in particular in the presence of singularities. we will survey some results which display the connections between the geometric complexity of the dynamics and computability issues, as well as new relations between dynamic predictability and effective decidability.
the heart of intersection type assignment: normalisation proofs revisited. this paper gives a new proof for the approximation theorem and the characterisation of normalisability using intersection types for a system with 'w and a @?-relation that is contra-variant over arrow types. the technique applied is to define reduction on derivations and to show a strong normalisation result for this reduction. from this result, the characterisation of strong normalisation and the approximation result will follow easily; the latter, in its turn, will lead to the characterisation of (head) normalisability.
distance- k knowledge in self-stabilizing algorithms. many graph problems seem to require knowledge that extends beyond the immediate neighbors of a node. the usual self-stabilizing model only allows for nodes to make decisions based on the states of their immediate neighbors. we provide a general transformation for constructing self-stabilizing algorithms which utilize distance-k knowledge. our transformation has both a slowdown and space overhead in n^o^(^l^o^g^k^), and might be thought of as a distance-k resource allocation algorithm. our main application is a polynomial-time self-stabilizing algorithm for finding maximal irredundant sets, a problem which seems to require distance-4 information. these results can be generalized to efficiently find maximal p-sets, for properties p which we call local monotonic. our techniques extend results in a recent paper by gairing et al. for achieving distance-two information.
how to meet in anonymous network. a set of k mobile agents with distinct identifiers and located in nodes of an unknown anonymous connected network, have to meet at some node. we show that this gathering problem is no harder than its special case for k=2, called the rendezvous problem, and design deterministic protocols solving the rendezvous problem with arbitrary startups in rings and in general networks. the measure of performance is the number of steps since the startup of the last agent until the rendezvous is achieved. for rings we design an oblivious protocol with cost o(nlog@?), where n is the size of the network and @? is the minimum label of participating agents. this result is asymptotically optimal due to the lower bound showed by [a. dessmark, p. fraigniaud, d. kowalski, a. pelc, deterministic rendezvous in graphs, algorithmica 46 (2006) 69-96]. for general networks we show a protocol with cost polynomial in n and log@?, independent of the maximum difference @t of startup times, which answers in the affirmative the open question by [a. dessmark, p. fraigniaud, d. kowalski, a. pelc, deterministic rendezvous in graphs, algorithmica 46 (2006) 69-96].
local spreading algorithms for autonomous robot systems. this paper studies local algorithms for autonomous robot systems, namely, algorithms that use only information of the positions of a bounded number of their nearest neighbors. the paper focuses on the spreading problem. it defines measures for the quality of spreading, presents a local algorithm for the one-dimensional spreading problem, proves its convergence to the equally spaced configuration and discusses its convergence rate in the synchronous and semi-synchronous settings. it then presents a local algorithm achieving the exact equally spaced configuration in finite time in the synchronous setting, and proves it is time optimal for local algorithms. finally, the paper also proposes a possible algorithm for the two-dimensional case and presents partial simulation results of its effectiveness.
an annotated bibliography on guaranteed graph searching. graph searching encompasses a wide variety of combinatorial problems related to the problem of capturing a fugitive residing in a graph using the minimum number of searchers. in this annotated bibliography, we give an elementary classification of problems and results related to graph searching and provide a source of bibliographical references on this field.
cleaning a network with brushes. following the decontamination metaphor for searching a graph, we introduce a cleaning process, which is related to both the chip-firing game and edge searching. brushes (instead of chips) are placed on some vertices and, initially, all the edges are dirty. when a vertex is 'fired', each dirty incident edge is traversed by only one brush, cleaning it, but a brush is not allowed to traverse an already cleaned edge; consequently, a vertex may not need degree-many brushes to fire. the model presented is one where the edges are continually recontaminated, say by algae, so that cleaning is regarded as an on-going process. ideally, the final configuration of the brushes, after all the edges have been cleaned, should be a viable starting configuration to clean the graph again. we show that this is possible with the least number of brushes if the vertices are fired sequentially but not if fired in parallel. we also present bounds for the least number of brushes required to clean graphs in general and some specific families of graphs.
fast deterministic distributed algorithms for sparse spanners. this paper concerns the efficient construction of sparse and low stretch spanners for unweighted arbitrary graphs with n nodes. all previous deterministic distributed algorithms, for constant stretch spanners of o(n^2) edges, have a running time @w(n^@e) for some constant @e>0 depending on the stretch. our deterministic distributed algorithms construct constant stretch spanners of o(n^2) edges in o(n^@e) time for any constant @e>0. more precisely, in linial's free model a.k.a local model, we construct in n^o^(^1^/^l^o^g^n^) time, for every graph, a (3,2)-spanner of o(n^3^/^2) edges, i.e., a spanning subgraph in which the distance is at most 3 times the distance of the original graph plus 2. the result is extended to (@a"k,@b"k)-spanners with o(n^1^+^1^/^klogk) edges for every integer parameter k>=1, where @a"k+@b"k=o(k^l^o^g^"^2^5). if the minimum degree of the graph is @w(n), then, in the same time complexity, a (5,4)-spanner with o(n) edges can be constructed.
distributed chasing of network intruders. graph searching is one of the most popular tools for analyzing the chase for a powerful and hostile software agent (called the ''intruder''), by a set of software agents (called the ''searchers'') in a network. the existing solutions for the graph searching problem suffer however from a serious drawback: they are mostly centralized and assume a global synchronization mechanism for the searchers. in particular: (1) the search strategy for every network is computed based on the knowledge of the entire topology of the network, and (2) the moves of the searchers are controlled by a centralized mechanism that decides at every step which searcher has to move, and what movement it has to perform. this paper addresses the graph searching problem in a distributed setting. we describe a distributed protocol that enables searchers with logarithmic size memory to clear any network, in a fully decentralized manner. the search strategy for the network in which the searchers are launched is computed online by the searchers themselves without knowing the topology of the network in advance. it performs in an asynchronous environment, i.e., it implements the necessary synchronization mechanism in a decentralized manner. in every network, our protocol performs a connected strategy using at most k+1 searchers, where k is the minimum number of searchers required to clear the network in a monotone connected way using a strategy computed in the centralized and synchronous setting.
minimum-energy broadcast and disk cover in grid wireless networks. the minimum-energy broadcast problem is to assign a transmission range to every station of an ad hoc wireless networks so that (i) a given source station is allowed to perform broadcast operations and (ii) the overall energy consumption of the range assignment is minimized. we prove a nearly tight asymptotical bound on the optimal cost for the minimum-energy broadcast problem on square grids. we also derive near-tight bounds for the bounded-hop version of this problem. our results imply that the best-known heuristic, the mst-based one, for the minimum-energy broadcast problem is far to achieve optimal solutions (even) on very regular, well-spread instances: its worst-case approximation ratio is about @p and it yields @w(n) hops, where n is the number of stations. as a by product, we get nearly tight bounds for the minimum-disk cover problem and for its restriction in which the allowed disks must have non-constant radius. finally, we emphasize that our upper bounds are obtained via polynomial time constructions.
election and rendezvous with incomparable labels. in ''can we elect if we cannot compare'' (spaa'03), barriere, flocchini, fraigniaud and santoro consider a qualitative model of distributed computing, where the labels of the entities are distinct but mutually incomparable. they study the leader election problem in a distributed mobile environment and they wonder whether there exists an algorithm such that for each distributed mobile environment, it either states that the problem cannot be solved in this environment, or it successfully elects a leader. in this paper, we give a positive answer to this question. we also give a characterization of the distributed mobile environments where election and rendezvous can be solved.
time constrained graph searching. we consider time constraints for four models of searching graphs for intruders. one model is the standard cops and robber vertex-searching model with complete visibility. the second model differs from the preceding one only in that none of the searchers can see the intruder. the third model is a vertex-searching model in which searchers and an intruder move simultaneously and none of the searchers can see the intruder. the fourth model is simultaneous edge searching with an arbitrarily fast intruder.
the role of information in the cop-robber game. we investigate the role of the information available to the players on the outcome of the cops and robbers game. this game takes place on a graph and players move along the edges in turns. the cops win the game if they can move onto the robber's vertex. in the standard formulation, it is assumed that the players can ''see'' each other at all times. a graph g is called cop-win if a single cop can capture the robber on g. we study the effect of reducing the cop's visibility. on the positive side, with a simple argument, we show that a cop with small or no visibility can capture the robber on any cop-win graph (even if the robber still has global visibility). on the negative side, we show that the reduction in cop's visibility can result in an exponential increase in the capture time. finally, we start the investigation of the variant where the visibility powers of the two players are symmetrical. we show that the cop can establish eye contact with the robber on any graph and present a sufficient condition for capture. in establishing this condition, we present a characterization of graphs on which a natural greedy pursuit strategy suffices for capturing the robber.
optimal delay for media-on-demand with pre-loading and pre-buffering. broadcasting popular media to clients is the ultimate scalable solution for media-on-demand. the simple solution of downloading and viewing the medium from one channel cannot guarantee a reasonable start-up delay for viewing with no interruptions. two known techniques to reduce the delay are pre-loading and pre-buffering. in the former an initial segment of the medium is already in the client buffer, and in the latter segments of the medium are not transmitted in sequence and clients may pre-buffer latter segments of the medium before viewing them. in both techniques, clients should be capable to receive streams from channels at the same time of handling their own buffer and view the medium from either one of the channels or the buffer. this paper considers broadcasting schemes that combine pre-loading and pre-buffering. we present a complete tradeoff between (i) the size of the pre-loading; (ii) the maximum delay for an uninterrupted playback; (iii) the number of media; and (iv) the number of channels allocated per one medium. for a given b the size of the pre-loading as a fraction of the medium length, for m media, and for h channels per medium, we first establish a lower bound for the maximum delay, d, as a fraction of the medium length, for an uninterrupted playback of any medium out of the m media. we then present an upper bound that approaches this lower bound when each medium can be fragmented into many segments.
the maximum edge-disjoint paths problem in complete graphs. in this paper, we consider the undirected version of the well known maximum edge-disjoint paths problem, restricted to complete graphs. we propose an off-line 3.75-approximation algorithm and an on-line 6.47-approximation algorithm, improving the earlier 9-approximation algorithm proposed by carmi, erlebach, and okamoto [p. carmi, t. erlebach, y. okamoto, greedy edge-disjoint paths in complete graphs, in: proc. 29th workshop on graph theoretic concepts in computer science, in: lncs, vol. 2880, 2003, pp. 143-155]. moreover, we show that for the general case, no on-line algorithm is better than a (2-@e)-approximation, for all @e>0. for the special case when the number of paths is within a linear factor of the number of vertices of the graph, it is established that the problem can be optimally solved in polynomial time by an off-line algorithm, but that no on-line algorithm is better than a (1.5-@e)-approximation. finally, the proposed techniques are used to obtain off-line and on-line algorithms with a constant approximation ratio for the related problems of edge congestion routing and wavelength routing in complete graphs.
monotonicity of non-deterministic graph searching. in graph searching, a team of searchers are aiming at capturing a fugitive moving in a graph. in the initial variant, called invisible graph searching, the searchers do not know the position of the fugitive until they catch it. in another variant, the searchers permanently know the position of the fugitive, i.e. the fugitive is visible. this latter variant is called visible graph searching. a search strategy that catches any fugitive in such a way that the part of the graph reachable by the fugitive never grows is called monotone. a priori, monotone strategies may require more searchers than general strategies to catch any fugitive. this is however not the case for visible and invisible graph searching. two important consequences of the monotonicity of visible and invisible graph searching are: (1) the decision problem corresponding to the computation of the smallest number of searchers required to clear a graph is in np, and (2) computing optimal search strategies is simplified by taking into account that there exist some that never backtrack. fomin et al. [f.v. fomin, p. fraigniaud, n. nisse, nondeterministic graph searching: from pathwidth to treewidth, in: proceedings of the 30th international symposium on mathematical foundations of computer science, mfcs'05, 2005, pp. 364-375] introduced an important graph searching variant, called non-deterministic graph searching, that unifies visible and invisible graph searching. in this variant, the fugitive is invisible, and the searchers can query an oracle that permanently knows the current position of the fugitive. the question of the monotonicity of non-deterministic graph searching was however left open. in this paper, we prove that non-deterministic graph searching is monotone. in particular, this result is a unified proof of monotonicity for visible and invisible graph searching. as a consequence, the decision problem corresponding to non-deterministic graph searching belongs to np. moreover, the exact algorithms designed by fomin et al. do compute optimal non-deterministic search strategies.
on some questions regarding k -regular and k -context-free sequences. we answer two questions of allouche and shallit regarding k-regular sequences and k-context-free sequences. one of these has been solved independently in another way by bell. we also provide a partial solution to another question of allouche and shallit regarding the subword complexity of k-context-free sequences.