Computer Sciencehttp://hdl.handle.net/1813/5172016-05-25T13:09:52Z2016-05-25T13:09:52ZA Calculus for Flow-Limited Authorization: Technical ReportArden, OwenMyers, Andrew C.http://hdl.handle.net/1813/424062016-05-11T05:01:34Z2016-05-09T00:00:00ZA Calculus for Flow-Limited Authorization: Technical Report
Arden, Owen; Myers, Andrew C.
Real-world applications routinely make authorization decisions based on dynamic computation. Reasoning about dynamically computed authority is challenging. Integrity of the system might be compromised if attackers can improperly influence the authorizing computation. Confidentiality can also be compromised by authorization, since authorization decisions are often based on sensitive data such as membership lists and passwords. Previous formal models for authorization do not fully address the security implications of permitting trust relationships to change, which limits their ability to reason about authority that derives from dynamic computation. Our goal is a way to construct dynamic authorization mechanisms that do not violate confidentiality or integrity.; We introduce the Flow-Limited Authorization Calculus (FLAC), which is both a simple, expressive model for reasoning about dynamic authorization and also an information flow control language for securely implementing various authorization mechanisms. FLAC combines the insights of two previous models: it extends the Dependency Core Calculus with features made possible by the Flow-Limited Authorization Model. FLAC provides strong end-to-end information security guarantees even for programs that incorporate and implement rich dynamic authorization mechanisms. These guarantees include noninterference and robust declassification, which prevent attackers from influencing information disclosures in unauthorized ways. We prove these security properties formally for all FLAC programs and explore the expressiveness of FLAC with several examples.
2016-05-09T00:00:00ZJRIF: Reactive Information Flow Control for JavaKozyri, ElisavetArden, OwenMyers, Andrew C.Schneider, Fred B.http://hdl.handle.net/1813/411942016-02-17T16:25:24Z2016-02-12T00:00:00ZJRIF: Reactive Information Flow Control for Java
Kozyri, Elisavet; Arden, Owen; Myers, Andrew C.; Schneider, Fred B.
A reactive information flow (RIF) automaton for a value v specifies (i) allowed uses for v and (ii) the RIF automaton for any value that might be directly or indirectly derived from v. RIF automata thus specify how transforming a value alters how the result might be used. Such labels are more expressive than existing approaches for controlling downgrading. We devised a type system around RIF automata and incorporated it into Jif, a dialect of Java that supports a classic form of labels for information flow. By implementing a compiler for the resulting JRIF language, we demonstrate how easy it is to replace a classic information-flow type system by a more expressive RIF-based type system. We programmed two example applications in JRIF, and we discuss insights they provide into the benefits of RIF-based security labels.
2016-02-12T00:00:00ZA Conversation with Fred SchneiderSchneider, Fred B.Gries, Davidhttp://hdl.handle.net/1813/413702015-12-07T15:40:12Z2015-09-09T00:00:00ZA Conversation with Fred Schneider
Schneider, Fred B.; Gries, David
Fred Schneider, an expert in concurrent and distributed systems and in computer and cybersecurity, shares insights about how his professional interests evolved, and provides sweeping views about how his field and department have changed.
2015-09-09T00:00:00ZA Conversation with Claire CardieCardie, ClaireConstable, Robert L.http://hdl.handle.net/1813/412162015-11-10T19:47:46Z2015-09-09T00:00:00ZA Conversation with Claire Cardie
Cardie, Claire; Constable, Robert L.
Claire Cardie discusses the role of Gerard Salton, natural language processing and the creation of the Information Science Department.
2015-09-09T00:00:00ZA Conversation with Ken BirmanBirman, KenVan Renesse, Robberthttp://hdl.handle.net/1813/412072015-11-03T15:02:25Z2015-09-10T00:00:00ZA Conversation with Ken Birman
Birman, Ken; Van Renesse, Robbert
Ken Birman discusses the origins of cloud computing.
2015-09-10T00:00:00ZA Conversation with Dexter KozenKozen, DexterConstable, Robert L.http://hdl.handle.net/1813/412062015-11-03T15:01:49Z2015-09-09T00:00:00ZA Conversation with Dexter Kozen
Kozen, Dexter; Constable, Robert L.
Kozen discusses his experiences at Cornell – his research and teaching experience, textbooks, participation in sports & music, etc.
2015-09-09T00:00:00ZA Conversation with Charlie Van LoanVan Loan, CharlieBala, Kavitahttp://hdl.handle.net/1813/412012015-10-30T14:52:34Z2015-09-15T00:00:00ZA Conversation with Charlie Van Loan
Van Loan, Charlie; Bala, Kavita
Van Loan discusses his experiences with teaching, writing textbooks, administering degree programs, MatLab, matrices and more.
2015-09-15T00:00:00ZA Conversation with Tim TeitelbaumTeitelbaum, TimGries, Davidhttp://hdl.handle.net/1813/408652015-10-13T16:53:13Z2015-09-10T00:00:00ZA Conversation with Tim Teitelbaum
Teitelbaum, Tim; Gries, David
A discussion of the teaching of large, introductory courses in programming in the early days-using the Terak and Macintosh computers and
the development of integrated programming environments that implement language-aware editing capabilities.
2015-09-10T00:00:00ZA Conversation with David GriesGries, DavidConstable, Robert L.http://hdl.handle.net/1813/405762015-08-07T19:09:34Z2015-07-21T00:00:00ZA Conversation with David Gries
Gries, David; Constable, Robert L.
2015-07-21T00:00:00ZA Conversation with John E. HopcroftHopcroft, John E.Gries, Davidhttp://hdl.handle.net/1813/405682015-08-03T15:17:11Z2015-07-21T00:00:00ZA Conversation with John E. Hopcroft
Hopcroft, John E.; Gries, David
This ACM Turing Award recipient talks about research, textbooks, working with graduate students, his role as a senior statesman of his field and concludes with some words of wisdom.
2015-07-21T00:00:00ZA Conversation with Richard W. ConwayConway, Richard W.Gries, Davidhttp://hdl.handle.net/1813/405642015-07-31T14:38:44Z2015-07-21T00:00:00ZA Conversation with Richard W. Conway
Conway, Richard W.; Gries, David
2015-07-21T00:00:00ZA Conversation with Robert L. ConstableConstable, Robert L.Gries, Davidhttp://hdl.handle.net/1813/405602015-07-31T15:07:37Z2015-07-21T00:00:00ZA Conversation with Robert L. Constable
Constable, Robert L.; Gries, David
2015-07-21T00:00:00ZA Conversation with Anil NerodeNerode, AnilGries, Davidhttp://hdl.handle.net/1813/405272015-07-22T18:23:44Z2014-10-16T00:00:00ZA Conversation with Anil Nerode
Nerode, Anil; Gries, David
2014-10-16T00:00:00ZFlow-Limited AuthorizationArden, OwenLiu, JedMyers, Andrewhttp://hdl.handle.net/1813/401382015-07-09T02:50:00Z2015-05-08T00:00:00ZFlow-Limited Authorization
Arden, Owen; Liu, Jed; Myers, Andrew
Because information flow control mechanisms often rely on an underlying
authorization mechanism, their security guarantees can be
subverted by weaknesses in authorization. Conversely, the security
of authorization can be subverted by information flows that
leak information or that influence the delegation of authority among
principals.
We argue that interactions between information flow and authorization
create security vulnerabilities that have not been fully identified or
addressed in prior work.
We explore how the security of decentralized information
flow control (DIFC) is affected by
three aspects of its underlying authorization mechanism: first,
delegation of authority between principals; second, revocation of
previously delegated authority; third, information flows created by
the authorization mechanisms themselves. It is no surprise
that revocation poses challenges, but we show that even delegation
is problematic because it enables unauthorized
downgrading. Our solution is a new security model, the Flow-Limited
Authorization Model (FLAM), which offers a new, integrated approach to
authorization and information flow control.
FLAM ensures robust authorization, a novel security condition for
authorization queries that ensures attackers cannot influence
authorization decisions or learn confidential trust relationships.
We discuss our prototype implementation and its algorithm for
proof search.
Content file updated at author's request on 2015-06-04.
2015-05-08T00:00:00ZA Conversation with Juris HartmanisHartmanis, Jurishttp://hdl.handle.net/1813/149342015-07-14T20:19:55Z2010-03-31T00:00:00ZA Conversation with Juris Hartmanis
Hartmanis, Juris
Juris Hartmanis is video taped in a far-reaching conversation (70 minutes) with colleague David Gries. They discuss Hartmanis’ childhood and family background and his immigration to the United States. Next they trace his extraordinary career at the GE Research Laboratory, where he collaborated with Richard Stearns on pioneering research that eventually was recognized by ACM’s prestigious, highest honor – the Turing Award. After having served earlier as an Instructor in Cornell’s Mathematics Department, Juris returned to Cornell as a full professor and the founding chair of a new department of Computer Science. This Department was embedded in two colleges, Engineering
and Arts and Sciences. Cornell was among the first Universities to establish a Department of Computer Science. His pioneering work on computational
complexity blossomed into a new field and under his leadership the Computer Science department matured into a robust, national leader with a strong theoretical emphasis.
After a successful stint at the National Science Foundation leading the transition
of the academic research network NSFnet to become the Internet, he returned to Cornell. At Cornell he continues an active program of research and maintains a leadership role in developing information technologies that have become a ubiquitous element across the entire Cornell academic scene.
2010-03-31T00:00:00ZA Linear List Merging AlgorithmHopcroft, John E.Ullman, Jeffrey D.http://hdl.handle.net/1813/108102015-07-08T02:31:17Z2008-05-14T13:42:16ZA Linear List Merging Algorithm
Hopcroft, John E.; Ullman, Jeffrey D.
A linear list merging algorithm and its analysis is presented. Starting with n lists, each containing a single element, the algorithm will execute an arbitrary sequence of requests to merge lists and to find the name of the list currently containing a given element. If the length of the sequence of requests is bounded by a constant times n, then the execution time of the algorithm on a random access computer is bounded by a constant times n.
2008-05-14T13:42:16ZOn the Modelling Power of Petri NetsMeiling, Erikhttp://hdl.handle.net/1813/75162015-07-07T22:39:38Z1979-12-01T00:00:00ZOn the Modelling Power of Petri Nets
Meiling, Erik
The behavior of a Petri net is expressed as a formal language. Certain families of Petri net languages are characterized by propositions similar to the classical pumping theorems. The results are used to give examples of behaviors that cannot be expressed by languages in these families.
1979-12-01T00:00:00ZCand and Cor Before and Then or Else in AdaGries, Davidhttp://hdl.handle.net/1813/75152015-07-08T00:42:47Z1979-11-01T00:00:00ZCand and Cor Before and Then or Else in Ada
Gries, David
NO ABSTRACT SUPPLIED
1979-11-01T00:00:00ZA Proof Technique for Communicating Sequential Processes(With an Example)Levin, Gary Marchttp://hdl.handle.net/1813/75142015-07-07T22:52:46Z1979-11-01T00:00:00ZA Proof Technique for Communicating Sequential Processes(With an Example)
Levin, Gary Marc
We present proof rules for an extension of the Communicating Sequential Processes proposed by Hoare. The send and receive statements are treated symmetrically, simplifying the rules and allowing send to appear in guards. An example is given to explain the use of the technique. This is an outline of a substantial part of a PhD thesis that is expected to be completed in June 1980.
1979-11-01T00:00:00ZOn Linear Natural DeductionLeivant, Danielhttp://hdl.handle.net/1813/75132015-07-07T23:03:19Z1979-11-01T00:00:00ZOn Linear Natural Deduction
Leivant, Daniel
NO ABSTRACT SUPPLIED
1979-11-01T00:00:00ZThe System Architecture for CORE: A Tolerant Program Development EnvironmentArcher, James E., Jr.Conway, Richard W.Shore, Andrew I.Silver, Leonard S.http://hdl.handle.net/1813/75122015-07-08T00:07:31Z1979-10-01T00:00:00ZThe System Architecture for CORE: A Tolerant Program Development Environment
Archer, James E., Jr.; Conway, Richard W.; Shore, Andrew I.; Silver, Leonard S.
CORE is a program development environment intended primarily to explore a highly tolerant useer interface. In some respects the internal architecture is also novel. It permits a highly interactive and supportive user interface to be implemented with processing routines which are essentially oblivious to any user interaction.
1979-10-01T00:00:00ZA Program Development System Execution SupervisorArcher, James E., Jr.Shore, Andrew I.http://hdl.handle.net/1813/75112015-07-07T22:33:10Z1979-10-01T00:00:00ZA Program Development System Execution Supervisor
Archer, James E., Jr.; Shore, Andrew I.
The Cornell Program Development System is an experimental vehicle to explore the applicability of highly cooperative tactics to a contemporary development environment. The CPDS provides significant facilities for modifying and immediately executing programs. The execution supervisor and the internal user program representation it uses to implement these facilities are described.
1979-10-01T00:00:00ZQuadratic Programming with M-MatricesLuk, Franklin T.Pagano, Marcellohttp://hdl.handle.net/1813/75102015-07-07T22:49:28Z1979-10-01T00:00:00ZQuadratic Programming with M-Matrices
Luk, Franklin T.; Pagano, Marcello
In this paper, we study the problem of quadratic programming with M-matrices. We describe (1) an effective algorithm for the case where the variables are subject to a lower bound constraint, and (2) an analogous algorithm for the case where the variables are subject to lower and upper bounds constraints. We demonstrate the special monotone behavior of the iterate and gradient vectors. The result on the gradient vector is new. It leads us to consider a simple updating procedure which preserves the monotonicity of both vectors. The procedure uses the fact that an M-matrix has a non-negative inverse. Two new algorithms are then constructed by incorporating this updating procedure into the two given algorithms. We give numerical examples which show that the new methods can be more efficient than the original ones.
1979-10-01T00:00:00ZAda/CS - An Instructional Subset of the Programming Language AdaArcher, James E., Jr.http://hdl.handle.net/1813/75092015-07-08T00:29:35Z1979-10-01T00:00:00ZAda/CS - An Instructional Subset of the Programming Language Ada
Archer, James E., Jr.
NO ABSTRACT SUPPLIED
1979-10-01T00:00:00ZA Unified View of SemanticsMajster, Mila E.http://hdl.handle.net/1813/75082015-07-08T01:34:19Z1979-10-01T00:00:00ZA Unified View of Semantics
Majster, Mila E.
NO ABSTRACT SUPPLIED
1979-10-01T00:00:00ZEfficient On-Line Construction and Correction of Position TreesMajster, Mila E.http://hdl.handle.net/1813/75072015-07-08T00:38:07Z1979-10-01T00:00:00ZEfficient On-Line Construction and Correction of Position Trees
Majster, Mila E.
This paper presents an on-line algorithm for the construction of position trees, i.e. an algorithm which constructs the position tree for a given string while reading the string from left to right. In addition, an on-line correction algorithm is presented which - upon a change in the string - can be used to construct the new position tree. Moreover, special attention is paid to computers with small memory. Compactification of the trees and transport costs between main and secondary storage are discussed.
1979-10-01T00:00:00ZEnsuring Consistency in a Distributed Database System by Use of Distributed SemaphoresSchneider, Fred B.http://hdl.handle.net/1813/75062015-07-08T00:17:56Z1979-09-01T00:00:00ZEnsuring Consistency in a Distributed Database System by Use of Distributed Semaphores
Schneider, Fred B.
Solutions to the database consistency problem in distributed databases are developed. It is shown how any solution to the consistency problem for a centralized database system that involves locking can be adapted for use in distributed systems. This is done, constructively, in two steps. First, it is shown how locking can be implemented in terms of semaphores. Then, a semaphore implementation that is suitable for use in distributed systems is developed.
1979-09-01T00:00:00ZSynchronization in Distributed ProgramsSchneider, Fred B.http://hdl.handle.net/1813/75052015-07-07T22:47:27Z1979-09-01T00:00:00ZSynchronization in Distributed Programs
Schneider, Fred B.
A technique for solving synchronization problems in distributed programs is described. Use of this technique in environments in which processes may fail is discussed. The technique can be used to solve synchronization problems directly, to implement new synchronization mechanisms (which are presumably well suited for use in distributed programs), and to construct distributed versions of existing synchronization mechanisms. Use of the technique is illustrated with implementations of distributed semaphores and a conditional message passing facility.
1979-09-01T00:00:00ZOn Easily Infinite Sets and On a Statement of R. LiptonLeivant, Danielhttp://hdl.handle.net/1813/75042015-07-08T01:01:26Z1979-09-01T00:00:00ZOn Easily Infinite Sets and On a Statement of R. Lipton
Leivant, Daniel
For a complexity measure $\kappa$, a set is $\kappa$-infinite if it contains a $\kappa$-decidable infinite subset. For a time-based $\kappa$, we prove that there is a recursive S s.t. both S and its complements, $\bar{S}$, are infinite but not $\kappa$-infinite. Lipton [6] states that the existence of a recursive set S s.t. neither S nor $\bar{S}$ os polynomially infinite is not a purely logical consequence of $\prod^{0}_{2}$ theorems of Peano's Arithmetic PA. His proof uses a construction of an algorithm within a non-standard model of of Arithmetic, in which the existence of infinite descending chains in such models is overlooked. We give a proof of a stronger statement to the effect that the existence of a recursive set S s.t. neither S nor $\bar{S}$ is linearly infinite is not a tautological consequence of all true $\prod^{0}_{2}$ assertions. We comment on other aspects of [6], and show $(\S 2)$ that a tautological consequence of true $\prod^{0}_{2}$ assertions may not be equivalent (in PA, say) to a $\prod^{0}_{2}$ sentence. The three sections of this paper use techniques of Recursion Theory, Proof Theory and Model Theory, respectively.
1979-09-01T00:00:00ZA Logic For Correct Program DevelopmentBates, Joseph Louishttp://hdl.handle.net/1813/75032015-07-07T23:07:22Z1979-08-01T00:00:00ZA Logic For Correct Program Development
Bates, Joseph Louis
1979-08-01T00:00:00ZThe Complexity of Parallel ComputationsWyllie, James C.http://hdl.handle.net/1813/75022015-07-07T23:02:53Z1979-08-01T00:00:00ZThe Complexity of Parallel Computations
Wyllie, James C.
Recent advances in microelectronics have brought closer to feasibility the construction of computers containing thousands (or more) of processing elements. This thesis addresses the question of effective utilization of such processing power. We study the computational complexity of synchronous paarallel computations using a model of computation based on random access machines operating in parallel and sharing a common memory, the P-RAM. Two main areas within the field of parallel computational complexity are investigated. First, we explore the power of the P-RAM model viewed as an abstract computing device. Later, we study techniques for developing efficient algorithms for parallel computers. We are able to give concise characterizations of the power of deterministic and nondeterministic P-RAMS in terms of the more widely known space and time complexity classes for multi-tape Turing machines. Roughly speaking, time-bounded deterministic P-RAMS are equivalent in power to (can accept the same sets as) space-bounded Turing machines, where the time and space bounds differ by at most a polynomial. In the context of comparing models of computation, we consider such polynomial differences in resources to be insignificant. Adding the feature of nondeterminism to the time-bounded P-RAM changes its power to that of a nondeterministic Turing machine with an exponentially higher running time. The later sections of the thesis examine algorithm design techniques for parallel computers. We first develop efficient procedures for some common operations on linked lists and arrays. Given this background, we introduce three techniques that permit the design of parallel algorithms that are efficient in terms of both their time and processor requirements. We illustrate the use of these techniques by presenting time and processor efficient algorithms for three problems, in each case improving upon the best previously known parallel resource bounds. We show how to compute minimum string edit distances, using the technique of pairwise function composition. We describe an algorithm for the off-line MIN that organizes its computation in the form of a complete binary tree. Finally, we present an algorithm for undirected graph connectivity that relies on redundancy in its representation of the input graph.
1979-08-01T00:00:00ZA Linear Time Algorithm for the Generalized Consecutive Retrieval ProblemDietz, Paul F.Furst, MerrickHopcroft, John E.http://hdl.handle.net/1813/75012015-07-08T01:14:49Z1979-07-01T00:00:00ZA Linear Time Algorithm for the Generalized Consecutive Retrieval Problem
Dietz, Paul F.; Furst, Merrick; Hopcroft, John E.
THe Generalized Consecutive Retrieval Problem (GCRP) is to find a directed tree on $n$ records in which each of $k$ subsets forms a directed path. The problem arises in organizing information for efficient retrieval. A linear time algorithm for the GCRP is given. Further generalization leads to problems that are complete for NP.
1979-07-01T00:00:00ZA Time-Space Tradeoff for In-Place Array PermutationMelville, Robert C.http://hdl.handle.net/1813/75002015-07-07T23:35:46Z1979-07-01T00:00:00ZA Time-Space Tradeoff for In-Place Array Permutation
Melville, Robert C.
NO ABSTRACT SUPPLIED
1979-07-01T00:00:00ZConvergence Theorems for Least Change Secant Update MethodsDennis, John E. Jr.Walker, Homer F.http://hdl.handle.net/1813/74992015-07-07T23:47:59Z1979-07-01T00:00:00ZConvergence Theorems for Least Change Secant Update Methods
Dennis, John E. Jr.; Walker, Homer F.
The purpose of this paper is to present a convergence analysis of the least change secant methods in which part of the derivative matrix being approximated is computed by other means. The theorems and proofs given here can be viewed as generalizations of those given by Broyden-Dennis-More and by Dennis-More. The analysis is done in the orthogonal projection setting of Dennis-Schnabel and many readers might feel that it is easier to understand. The theorems here readily imply local and q-superlinear convergence of all the standard methods in addition to proving these results for the first time for the sparse symmetric method of Marwil and Toint and the nonlinear least squares method of Dennis-Gay-Welsch.
1979-07-01T00:00:00ZLocal Convergence Theorems for Quasi-Newton MethodsDennis, John E. Jr.Walker, Homer F.http://hdl.handle.net/1813/74982015-07-07T23:57:05Z1979-07-01T00:00:00ZLocal Convergence Theorems for Quasi-Newton Methods
Dennis, John E. Jr.; Walker, Homer F.
This paper presents generalizations of the two results which have been useful for analyzing methods of the form $x_{k+1} = x_{k} - B_{k}^{-1}F(x_{k})$. The bounded deterioration theorem of Broyden-Dennis-More is generalized to show that if \{$B_{k}$\} or \{$B_{k}^{-1}$\} is of bounded deterioration as a sequence of approximants to some $B_{*}$ or $B_{*}^{-1}$ then the iteration above has the same local convergence properties and arbitrarily nearly the same linear rate as would be achieved by the stationary iteration function which uses $B_{k} = B_{*}$. The characterization theorem for superlinear convergence given by Dennis-More is then generalized to give conditions under which the rates are the same. In the case when $B_{*} = F'(x_{*})$, these results reduce to those already known.
1979-07-01T00:00:00ZEfficiency Considerations In Implementing Dijkstra's Guarded Command ConstructsMcGuire, Marguerite Elainehttp://hdl.handle.net/1813/74972015-07-07T23:33:13Z1979-07-01T00:00:00ZEfficiency Considerations In Implementing Dijkstra's Guarded Command Constructs
McGuire, Marguerite Elaine
The guarded command alternative and iterative constructs proposed by E. W. Dijkstra subsume the conventional alternative and iterative constructs. The extra flexibility of these guarded command constructs enables the programmer to express his ideas more directly and clearly. Moreover, Dijkstra has developed a calculus for the derivation of correct programs that utilizes these guarded command constructs. This thesis addresses the problem of efficiently implementing these guarded command constructs. Several new optimizations that are particularly well suited to the guarded command constructs are described. The most useful is the elimination of redundant boolean expressions. This optimization provides a means of implementing the guarded command alternative statement with efficiency comparable to the IF-THEN-ELSE statement. The main contribution of this thesis is a detailed description of an algorithm for eliminating redundant boolean expressions. The algorithm itself is presented in a program written in a PASCAL supplemented with the guarded command constructs. The basis method involves considering individual execution paths through the guarded command construct and applying rules of inference to recognize and avoid evaluation of many boolean expressions. It is shown that the number of execution paths through a guarded command construct remains small enough to make this method practical.
1979-07-01T00:00:00ZThe Cornell Program Synthesizer: A Tutorial IntroductionTeitelbaum, Timhttp://hdl.handle.net/1813/74962015-07-07T23:39:58Z1979-07-01T00:00:00ZThe Cornell Program Synthesizer: A Tutorial Introduction
Teitelbaum, Tim
This tutorial introduces a novice student to the basic facilities of the Cornell Program Synthesizer for developing programs written in the PL/CS dialect of PL/I. No knowledge of programming is assumed or required. It is assumed that you possess a Synthesizer diskette and have access to a TERAK microcomputer.
1979-07-01T00:00:00ZOn the Proof Theory of the Modal Logic GLeivant, Danielhttp://hdl.handle.net/1813/74952015-07-08T00:08:50Z1979-07-01T00:00:00ZOn the Proof Theory of the Modal Logic G
Leivant, Daniel
NO ABSTRACT SUPPLIED
1979-07-01T00:00:00ZA Procedure Call Proof Rule (With a Simple Explanation)Gries, DavidLevin, Gary Marchttp://hdl.handle.net/1813/74942015-07-07T22:45:06Z1979-05-01T00:00:00ZA Procedure Call Proof Rule (With a Simple Explanation)
Gries, David; Levin, Gary Marc
NO ABSTRACT SUPPLIED
1979-05-01T00:00:00ZUpson's Familiar QuotationsGaulle, Alhttp://hdl.handle.net/1813/74932015-07-07T22:30:39Z1979-05-01T00:00:00ZUpson's Familiar Quotations
Gaulle, Al
This report is a compilation of several hundred examples of context free language and very irregular expressions. Contributions were submitted over the last five years by numerous computer science graduate students who collected these now immortal words in classes and seminars. We wish to express our gratitude to the faculty, guest lecturers, and students who provided the bulk of this work.
1979-05-01T00:00:00ZA Hamiltonian-Schur DecompositionPaige, ChrisVan Loan, Charleshttp://hdl.handle.net/1813/74922015-07-07T23:30:15Z1979-09-01T00:00:00ZA Hamiltonian-Schur Decomposition
Paige, Chris; Van Loan, Charles
1979-09-01T00:00:00ZComputer Science and the Liberal Arts StudentVan Loan, Charleshttp://hdl.handle.net/1813/74912015-07-08T00:18:48Z1979-05-01T00:00:00ZComputer Science and the Liberal Arts Student
Van Loan, Charles
The computer science education of nontechnical liberal arts students is a matter of increasing concern. In this paper it is argued that computer scientists should promote and teach their subject more in line with the traditional aims of liberal education when dealing with students of this type. A framework for doing this is presented which involves a broad view of "computer literacy" based upon what other authors have written about "scientific literacy." The structure of a computer science appreciation course is outlined which embodies the ideas of liberal education described. The importance of historical perspective is emphasized. Key Words and Phrases: Computer literacy, liberal arts student, liberal education, history of computation, scientific literacy.
1979-05-01T00:00:00ZRepresentation of Almost Constant VectorsSteensgaard-Madsen, Jorgenhttp://hdl.handle.net/1813/74902015-07-07T23:59:10Z1979-04-01T00:00:00ZRepresentation of Almost Constant Vectors
Steensgaard-Madsen, Jorgen
An example in a recent report on the programming language Russell has illustrated difficulties related to user defined storage management. Here is demonstrated how the dynamic approach to encapsulation earlier proposed by the author provides means to solve the particular storage management problem. The method used is, however, easily generalized to other similar cases. In addition to the example a number of notational conveniences are introduced. One that allows abbreviated references to components of record-like structures is called controlled coercion. Another allows a function-like use of classes. Keywords: Classes, abstract data types, storage management, programming languages.
1979-04-01T00:00:00ZOn Restrictions to Ensure Reproducible Behavior in Concurrent ProgramsSchneider, Fred B.Bernstein, A. J.http://hdl.handle.net/1813/74892015-07-08T01:45:51Z1979-03-01T00:00:00ZOn Restrictions to Ensure Reproducible Behavior in Concurrent Programs
Schneider, Fred B.; Bernstein, A. J.
One of the major difficulties encountered when dealing with concurrent programs is that reproducible behavior may not be assumed. As a result, it is difficult to validate and debug such systems. In this paper, structural restrictions are presented that ensure that reproducible behavior will occur in concurrent programs. The application of this to system design is discussed. Keywords: time dependent behavior, concurrency, synchronization, monitors, Concurrent Pascal.
1979-03-01T00:00:00ZAPL and the Grzegorczyk HierarchyBreidbart, Sethhttp://hdl.handle.net/1813/74882015-07-07T23:44:57Z1979-03-01T00:00:00ZAPL and the Grzegorczyk Hierarchy
Breidbart, Seth
We show in this paper that the set of "traditional" APL 1-liners (using arithmetic functions only) compute precisely the set of functions in the class E4 of Grzegorczyk hierarchy (the class immediately above the elementary functions). We also show that if we extend the set of 1-liners to include either the "execute" operator, or 1 line programs with gotos, then any partial recursive function can be computed.
1979-03-01T00:00:00ZThe Cornell Program Synthesizer: A Microcomputer Implementationof PL/CSTeitelbaum, Timhttp://hdl.handle.net/1813/74872015-07-07T22:50:37Z1979-03-01T00:00:00ZThe Cornell Program Synthesizer: A Microcomputer Implementationof PL/CS
Teitelbaum, Tim
NO ABSTRACT SUPPLIED
1979-03-01T00:00:00ZComments on a Draft Pascal StandardSteensgaard-Madsen, Jorgenhttp://hdl.handle.net/1813/74862015-07-08T00:06:33Z1979-02-01T00:00:00ZComments on a Draft Pascal Standard
Steensgaard-Madsen, Jorgen
NO ABSTRACT SUPPLIED
1979-02-01T00:00:00ZA Progress Report on Automatic Information RetrievalSalton, Gerardhttp://hdl.handle.net/1813/74852015-07-07T23:02:46Z1979-02-01T00:00:00ZA Progress Report on Automatic Information Retrieval
Salton, Gerard
This study is a state-of-the-art report of work in automatic information retrieval. Various enhancements of operational on-line retrieval systems are described such as the utilization of special front-end devices providing compatibility among different search services, the introduction of fast back-end search devices, and the use of local clustering and query reformulation operations designed to improve retrieval output. Certain new algorithms for fast text matching and for optimum term weighting are also mentioned, as are advances in the construction of theoretical retrieval models.
1979-02-01T00:00:00ZImplementation of an Unrestricted File Organization for Micro-PL/CSArcher, James E. Jr.http://hdl.handle.net/1813/74842015-07-08T00:51:14Z1979-02-01T00:00:00ZImplementation of an Unrestricted File Organization for Micro-PL/CS
Archer, James E. Jr.
Micro PL/CS is a version of PL/CS developed for a single-user, interactive environment. A file system extension makes PL/CS self-sufficient for standalone file processing and secondary storage management. The basis of the file system extension is the Unrestricted File Organization which provides a free mixture of sequential, indexed and random file operations. The structure, operation, and system-interfaced procedures of the UFO are presented and explained. The Micro-PL/CS file extension implementation is then sketched in terms of the UFO primitives.
1979-02-01T00:00:00ZA File System Extension to Micro-PL/CSArcher, James E., Jr.http://hdl.handle.net/1813/74832015-07-07T22:59:52Z1979-02-01T00:00:00ZA File System Extension to Micro-PL/CS
Archer, James E., Jr.
Micro-PL/CS is a version of PL/CS developed for interactive use with a dedicated microprocessor. A file system extension is proposed to give PL/CS a simple, but extremely powerful file system capability. The system allows for the creation and manipulation of files for sequential, random, or keyed access (or any combination) in an unrestricted manner. Essential to the capability is a set of built-in functions and pseudo-variables which allow file manipulation without syntactic complication.
1979-02-01T00:00:00Z