Browsing LCS Publications by Title
Now showing items 1138-1157 of 1163
-
Verification of Programs Operating on Structured Data
(1974-03)The major method for verifying the correctness of computer program is the inductive assertion approach. This approach has been limited in the past by the lack of techniques for handling data structures. In particular, ... -
Verification of the Randomized Consensus Algorithm of Aspnes and Herlihy: a Case Study*
(1997-06)The Probabilistic I/O Automaton model of [20] is used as the basis for a formal presentation and proof of the randomized consensus algorithm of Aspnes and Herlihy. The algorithm guarantees termination within expected ... -
The Vidboard:A Video Capture and Processing Peripheral for the ViewStation System
(1992-09)With the growth of multimedia applications, video is increasingly being handled within the computing environment. Since video presents serious technological challenges to the current generation of personal computers and ... -
Video Coding and the Application Level Framing Protocol Architecture
(1992-06)As networks and computers become faster, real time video transmission is expected to become common. Variable bit rate video coders will be used in order to take advantage of the statistical multiplexing gain and bandwidth ... -
Video Games and Computer Aided Instruction
(1983-06)This document will briefly outline the evolution of video games, discuss current video game theory, and describe a program to teach typing on the IBM Personal Computer. -
View-based abstraction: Enhancing Maintainability and Modularity in the presence of Implementation Dependencies
(1997-09)This dissertation presents a new, backwards compatible, language independent, and incremental programming methodology called view-based abstraction. Unlike the well-known black-box abstraction approach, view-based abstraction ... -
Viewstamped Replication for Highly Available Distributed Systems
(1988-08)This dissertation presents viewstamped replication, a new algorithm for the implementation of highly available computer services that continue to be usable in spite of node crashes and network partitions. Our goal is to ... -
Virtual Wires: Overcoming Pin Limitations in FPGA-based Logic Emulation
(1993-11)Existing FPGA-based logic emulators are limited by inter-chip communication bandwidth, resulting in low gate utilization (10 to 20 percent of usable gates). This resource imbalance increases the number of chips needed to ... -
Virtual Wires: Overcoming Pin Limitations in FPGA-based Logic Emulators
(1992-11)Existing FPGA-based logic emulators suffer from limited inter-chip communication bandwidth, resulting in low gate utilization (10 20 percent). This resource imbalance increases the number of chips needed to emulate a ... -
Wafer-scale Integration of Systolic Arrays
(1983-02)VLSI technologists are fast developing wafer-scale integration. Rather than partitioning a silicon wafer into chips as is usually done, the idea behind wafer-scale integration is to assemble an entire system (or network ... -
Waiting Algorithms for Synchornization in Large-scale Multiprocessors
(1991-02)Through analysis and experiments, this paper investigates two-phase waiting algorithms to minimize the cost of waiting for synchronization in large-scale multiprocessors. In a two-phase algorithm, a thread first waits by ... -
Walter User's Manual (Version 1.0)
(1987-09)Walter is a UNIX program that provides access to databases located at MIT via the DARPA Internet. The databases provided by Walter include the full-text of the New York Times for the past 90 days. A sophisticated full-text ... -
Weak Consistency: A Generalized Theory and Optimistic Implementations for Distributed Transactions
(1999-03)Current commercial databases allow application programmers to trade off consistency for performance. However, existing definitions of weak consistency levels are either imprecise or they disallow efficient implementation ... -
Weak Monadic Second Order Theory of Successor is not Element-recurive
(1973-12)Let L SIS be the set of formulas expressible in a week monadic second order logic using only the predicates [x =y+1] and [x E z]. Bucci and Elgot [3,4] have shown that the truth of sentences in L SIS (under the standard ... -
What are principal typings and what are they good for?
(1995-11)We demonstrate the pragmatic value of the principal typing property, a property more general than ML's principal type property, by studying a type system with principal typings. The type system is based on rank 2 intersection ... -
What are principal typings and what are they good for?
(1995-08)We demonstrate the pragmatic value of the principal typing property, a property more general than ML's principal type property, by studying a type system with principal typings. The type system is based on rank 2 intersection ... -
What is a Model of the Lamda Calculus? Expanded Version
(1981-07)An elementary, purely algebraic definition of model for the untypes lambda calculus is given. This definition is shown to be equivalent to the natural semantic definition based on environments. These definitions of model ... -
What Price for Eliminating Expression Side-effects?
(1985-06)Separating a programming language into side-effect-free expressions and effect-only statements should make the language more amenable to axiomatization, as well as providing benefits for style, pedagogy, and implementation ... -
Width-3 Permutation Branching Programs
(1985-12)We consider a restricted class of width-3 branching programs where each column of nodes depends on a single variable, and the 0-edges and the 1-edges out of each column form a permutation. In this model, parity and the ...