
Saeed, Taher; Gill, Harjot; Fei, Qiong; Zhang, Zhuoyao; Loo, Boon Thau
This paper describes our experiences at the University of Pennsylvania in developing course projects for a large advanced undergraduate and first year graduate course in networked systems. Students work in teams to develop substantial networked systems programming projects (>10000 lines of code) using network simulator 3 (ns3), an emerging opensource network simulator that is aimed at replacing the popular ns2 simulator. Projects are developed in layers, where students build upon earlier assignments, first developing a protocol for Internet Protocol (IP) routing, followed by a distributed hash table (DHT) overlay network, and finally, a keywordbased search engine. One novelty of our...

Traw, C. Brendan S; Smith, Jonathan M
Concurrent increases in network bandwidths and processor speeds have created a performance bottleneck at the workstationtonetwork host interface. This is especially true for BISDN networks where the fixed length ATM cell is mismatched with application requirements for data transfer; a successful hardware/software architecture will resolve such differences and offer high endtoend performance.
The solution we report carefully splits protocol processing functions into hardware and software implementations. The interface hardware is highly parallel and performs all percell functions with dedicated logic to maximize performance. Software provides support for the transfer of data between the interface and application memory, as well as the...

Gallier, Jean H
The purpose of this paper is to give an exposition of material dealing with constructive logic, typed λcalculi, and linear logic. The emergence in the past ten years of a coherent field of research often named "logic and computation" has had two major (and related) effects: firstly, it has rocked vigorously the world of mathematical logic; secondly, it has created a new computer science discipline, which spans from what is traditionally called theory of computation, to programming language design. Remarkably, this new body of work relies heavily on some "old" concepts found in mathematical logic, like natural deduction, sequent calculus,...

Gallier, Jean H
This paper consists primarily of a survey of results of Harvey Friedman about some proof theoretic aspects of various forms of Krusal's tree theorem, and in particular the connection with the ordinal Ƭo. We also include a fairly extensive treatment of normal functions on the countable ordinals, and we give a glimpse of Veblen Hierarchies, some subsystems of secondorder logic, slowgrowing and fastgrowing hierarchies including Girard's result, and Goodstein sequences. The central theme of this paper is a powerful theorem due to Kruskal, the "tree theorem", as well as a "finite miniaturization" of Kruskal's theorem due to Harvey Friedman. These...

Gunter, Carl A; Jung, Achim
Almost all of the categories normally used as a mathematical foundation for denotational semantics satisfy a condition known as consistent completeness. The goal of this paper is to explore the possibility of using a different condition  that of coherence  which has its origins in topology and logic. In particular, we concentrate on those posets whose principal ideals are algebraic lattices and whose topologies are coherent. These form a cartesian closed category which has fixed points for domain equations. It is shown that a "universal domain" exists. Since the construction of this domain seems to be of general significance,...

Wang, Anduo; Liu, Changbin; Loo, Boon Thau; Sokolsky, Oleg; Basu, Prithwash
The Internet today runs on a complex routing protocol called the Border Gateway Protocol (BGP). BGP is a policybased protocol, in which autonomous Internet Service Providers (ISPs) impose their local policies on the propagation of routing information. Over the past few years, there has been a growing consensus on the complexity and fragility of BGP routing. To address these challenges, we present the DRIVER system for designing, analyzing and implementing policybased routing protocols. Our system utilizes a declarative network verifier (DNV) which leverages declarative networking’s connection to logic programming by automatically compiling highlevel declarativen networking program into formal specifications, which...

Miller, Dale
It has been argued elsewhere that a logic programming language with function variables and λabstractions within terms makes a good metaprogramming language, especially when an objectlanguage contains notions of bound variables and scope. The λProlog logic programming language and the related Elf and Isabelle systems provide metaprograms with both function .variables and λabstractions by containing implementations of higherorder unification. This paper presents a logic programming language, called Lλ, that also contains both function variables and λabstractions, although certain restrictions are placed on occurrences of function variables. As a result of these restrictions, an implementation of Lλ does not need to...

Dawar, Anuj; Lindell, Steven; Weinstein, Scott
The extensions of firstorder logic with a least fixed point operators (FO + LFP) and with a partial fixed point operator (FO + PFP) are known to capture the complexity classes P and PSPACE respectively in the presence of an ordering relation over finite structures. Recently, Abiteboul and Vianu [AV91b] investigated the relation of these two logics in the absence of an ordering, using a mchine model of generic computation. In particular, they showed that the two languages have equivalent expressive power if and only if P = PSPACE. These languages can also be seen as fragments of an infinitary...

Hannan, John; Miller, Dale
Various metalanguages for the manipulation and specification of programs and programming languages have recently been proposed. We examine one such framework, called natural semantics, which was inspired by the work of G. Plotkin on operational semantics and extended by G. Kahn and others at INRIA. Natural semantics makes use of a firstorder metalanguage which represents programs as firstorder tree structures and reasons about these using natural deductionlike methods. We present the following three enrichments of this metalanguage. First, programs are represented not by firstorder structures but by simply typed λterms. Second, schema variables in inference rules can be higherorder variables....

Bangalore, Srinivas
πcalculus is a calculus for modeling dynamically changing configurations of a network of communicating agents. This paper studies the suitability of πcalculus as a unifying framework to model the operational semantics of the three paradigms of programming: functional, logic and imperative paradigms. In doing so, the attempt is to demonstrate that πcalculus models a primitive that is pervasive in the three paradigms and to illustrate that the three forms of sequential computing are special instances of concurrent computing.

Tabuada, Paulo; Pappas, George J
The control of complex systems poses new challenges that fall beyond the traditional methods of control theory. One of these challenges is given by the need to control, coordinate and synchronize the operation of several interacting submodules within a system. The desired objectives are no longer captured by usual control specifications such as stabilization or output regulation. Instead, we consider specifications given by linear temporal logic (LTL) formulas. We show that existence of controllers for discretetime controllable linear systems and LTL specifications can be decided and that such controllers can be effectively computed. The closedloop system is of hybrid nature,...

Fainekos, Georgios E; Pappas, George J
Realtime temporal logic reasoning about trajectories of physical systems necessitates models of time which are continuous. However, discrete time temporal logic reasoning is computationally more efficient than continuous time. Moreover, in a number of engineering applications only discrete time models are available for analysis. In this paper, we introduce a framework for testing MITL specifications on continuous time signals using only discrete time analysis. The motivating idea behind our approach is that if the dynamics of the signal fulfills certain conditions and the discrete time signal robustly satisfies the MITL specification, then the corresponding continuous time signal should also satisfy...

Porter, Dot
http://repository.upenn.edu/sims_ebooks/1009/thumbnail.jpg

Porter, Dot
http://repository.upenn.edu/sims_ebooks/1053/thumbnail.jpg

Porter, Dot
http://repository.upenn.edu/sims_ebooks/1175/thumbnail.jpg

Porter, Dot
http://repository.upenn.edu/sims_ebooks/1199/thumbnail.jpg

Porter, Dot
http://repository.upenn.edu/sims_ebooks/1179/thumbnail.jpg

Porter, Dot
http://repository.upenn.edu/sims_ebooks/1178/thumbnail.jpg

Champollion, Lucas

Baumard, Nicolas
Strong reciprocity theorists claim that punishment has evolved to promote the good of the group and to deter cheating. By contrast, weak reciprocity suggests that punishment aims to restore justice (i.e., reciprocity) between the criminal and his victim. Experimental evidences as well as field observations suggest that humans punish criminals to restore fairness rather than to support group cooperation