
Gallier, Jean H
The purpose of this paper is to give an exposition of material dealing with constructive logics, typed λcalculi, and linear logic. The first part of this paper gives an exposition of background material (with a few exceptions). This second part is devoted to linear logic and proof nets. Particular attention is given to the algebraic semantics (in Girard's terminology, phase semantics) of linear logic. We show how phase spaces arise as an instance of a Galois connection. We also give a direct proof of the correctness of the DanosRegnier criterion for proof nets. This proof is based on a purely...

Hodas, Joshua S.
An aspect of the Generalized Phrase Structure Grammar formalism proposed by Gazdar, et al. is the introduction of the notion of "slashed categories" to handle the parsing of structures, such as relative clauses, which involve unbounded dependencies. This has been implemented in Definite Clause Grammars through the technique of gap threading, in which a difference list of extracted noun phrases (gaps) is maintained. However, this technique is cumbersome, and can result in subtle soundness problems in the implemented grammars. Miller and Pareschi have proposed a method implementing gap threading at the logical level in intuitionistic logic. Unfortunately that implementation itself...

Felty, Amy; Miller, Dale
Various forms of typed λcalculi have been proposed as specification languages for representing wide varieties of object logics. The logical framework, LF, is an example of such a dependenttype λcalculus. A small subset of intuitionistic logic with quantification over simply typed λcalculus has also been proposed as a framework for specifying general logics. The logic of hereditary Harrop formulas with quantification at all nonpredicate types, denoted here as hhω, is such a metalogic that has been implemented in both the Isabelle theorem prover and the λProlog logic programming language. Both frameworks provide for specifications of logics in which details involved...

Stone, Matthew
Modal logics offer natural, declarative representations for describing both the modular structure of logical specifications and the attitudes and behaviors of agents. The results of this paper further the goal of building practical, efficient reasoning systems using modal logics. The key problem in modal deduction is reasoning about the world in a model (or scope in a proof) at which an inference rule is applied  a potentially hard problem. This paper investigates the use of partialorder mechanisms to maintain constraints on the application of modal rules in proof search in restricted languages. The main result is a simple, incremental...

Miller, Dale
The unification of simply typed λterms modulo the rules of ß and ηconversions is often called "higherorder" unification because of the possible presence of variables of functional type. This kind of unification is undecidable in general and if unifiers exist, most general unifiers may not exist. In this paper, we show that such unification problems can be coded as a query of the logic programming language Lλ in a natural and clear fashion. In a sense, the translation only involves explicitly axiomatizing in Lλ the notions of equality and substitution of the simply typed λcalculus: the rest of the unification...

Miller, Dale
The agent expressions of the πcalculus can be translated into a theory of linear logic in such a way that the reflective and transitive closure of πcalculus (unlabeled) reduction is identified with "entailedby". Under this translation, parallel composition is mapped to the multiplicative disjunct ("par") and restriction is mapped to universal quantification. Prefixing, nondeterministic choice (+), replication (!), and the match guard are all represented using nonlogical constants, which are specified using a simple form of axiom, called here a process clause. These process clauses resemble Horn clauses except that they may have multiple conclusions; that is, their heads may...

Nadathur, Gopalan; Miller, Dale
λProlog is a logic programming language that extends Prolog by incorporating notions of higherorder functions, λterms, higherorder unification, polymorphic types, and mechanisms for building modules and secure abstract data types. These new features are provided in a principled fashion by extending the classical firstorder theory of Horn clauses to the intuitionistic higherorder theory of hereditary Harrop formulas. The justification for considering this extension a satisfactory logic programming language is provided through the prooftheoretic notion of a uniform proof. The correspondence between each extension to Prolog and the new features in the stronger logical theory is discussed. Also discussed are various...

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