
Hannan, John; Miller, Dale
We demonstrate how a specification for the standard evaluation of a simple functional programming language can be systematically extended to a specification for mixed evaluation. Using techniques inspired by natural semantics we specify a standard evaluator by a set of inference rules. The evaluation of programs is then performed by a restricted kind of theorem proving in this logic. We then describe a systematic method for extending the proof system for standard evaluation to a new proof system that provides greater flexibility in treating bound variables in the objectlevel functional programs. We demonstrate how this extended proof system provides the...

Pareschi, Remo; Miller, Dale
Definite Clause Grammars (DCGs) have proved valuable to computational linguists since they can be used to specify phrase structured grammars. It is well known how to encode DCGs in Horn clauses. Some linguistic phenomena, such as fillergap dependencies, are difficult to account for in a completely satisfactory way using simple phrase structured grammar. In the literature of logic grammars there have been several attempts to tackle this problem by making use of special arguments added to the DCG predicates corresponding to the grammatical symbols. In this paper we take a different line, in that we account for fillergap dependencies by...

Vaughan, Jeffrey A; Jia, Limin; Mazurak, Karl; Zdancewic, Stephan A
Authorization logics provide a principled and flexible approach to specifying access control policies. One of their compelling benefits is that a proof in the logic is evidence that an accesscontrol decision has been made in accordance with policy. Using such proofs for auditing reduces the trusted computing base and enables the ability to detect flaws in complex authorization policies. Moreover, the proof structure is itself useful, because proof normalization can yield information about the relevance of policy statements. Untrusted, but welltyped, applications that access resources through an appropriate interface must obey the access control policy and create proofs useful for...

Miller, Dale
A universally quantified goal can be interpreted intensionally, that is, the goal ∀x.G(x) succeeds if for some new constant c, the goal G(c) succeeds. The constant c is, in a sense, given a scope: it is introduced to solve this goal and is "discharged" after the goal succeeds or fails. This interpretation is similar to the interpretation of implicational goals: the goal D ⊃ G should succeed if when D is assumed, the goal G succeeds. The assumption D is discharged after G succeeds or fails. An interpreter for a logic programming language containing both universal quantifiers and implications in...

Hodas, Joshua S; Miller, Dale
We present a logic programming language that uses implications and universal quantifiers in goals and in the bodies of clauses to provide a simple scoping mechanism for program clauses and constants. Within this language it is possible to define a simple notion of parametric module and local constant. Given this ability to structure programs, we explore how objectoriented programming, where objects are viewed as abstractions with behaviors, state, and inheritance, might be accommodated. To capture the notion of mutable state, we depart from the pure logic setting by adding a declaration that certain local predicates are deterministic (they succeed at...

Tannen, Val; Subrahmanyam, Ramesh
We study issues that arise in programming with primitive recursion over nonfree datatypes such as lists, bags and sets. Programs written in this style can lack a meaning in the sense that their outputs may be sensitive to the choice of input expression. We are, thus, naturally led to a settheoretic denotational semantics with partial functions. We set up a logic for reasoning about the definedness of terms and a deterministic and terminating evaluator. The logic is shown to be sound in the model, and its recursion free fragment is shown to be complete for proving definedness of recursion free...

Gallier, Jean H; Narendran, Paliath; Plaisted, David; Snyder, Wayne
Rigid Eunification is a restricted kind of unification modulo equational theories, or Eunification, that arises naturally in extending Andrews's theorem proving method of matings to firstorder languages with equality. This extension was first presented in Gallier, Raatz, and Snyder, where it was conjectured that rigid Eunification is decidable. In this paper, it is shown that rigid Eunification is NPcomplete and that finite complete sets of rigid Eunifiers always exist. As a consequence, deciding whether a family of mated sets is an equational mating is an NPcomplete problem. Some implications of this result regarding the complexity of theorem proving in firstorder...

Hodas, Joshua S; Miller, Dale
Logic programming languages based on fragments of intuitionistic logic have recently been developed and studied by several researchers. In such languages, implications are permitted in goals and in the bodies of clauses. Attempting to prove a goal of the form D ⊃ G in a context τ leads to an attempt to prove the goal G in the extended context τ ∪{D}. While an intuitionistic notion of context has many uses, it has turned out to be either too powerful or too limiting in several settings. We refine the intuitionistic notion of context by using a fragment of Girard's linear...

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...