46610662
CAL: A Computer Assisted Learning System for Computation and Logic
In this paper, we describe a computer system CAL which assists students' understanding of a lecture course in logic and computation. We introduce a new foundational theory of expressions, which is inspired by the theory of expressions due to Martin-Lof [6], and use the expressions determined by the theory to implement various syntactic objects in CAL. We also introduce the concept of derivation game, and show that various logical and computational systems given in the lecture course can be defined uniformly by derivation games.
10509424
A Simply Typed Context Calculus with First-class Environments
We introduce a simply typed λ-calculus λϰƐ" which has both contexts and environments as first-class values. In λϰƐ", holes in contexts are represented by ordinary variables of appropriate types and hole filling is represented by the functional application together with a new abstraction mechanism which takes care of packing and unpacking of the term which is used to fill in the holes of the context. λϰƐ" is a conservative extension of the simply typed λβ-calculus, enjoys subject reduction property, is confluent and strongly normalizing. 
 
The traditional method of defining substitution does not work for our calculus. So, we also introduce a new method of defining substitution. Although we introduce the new definition of substitution out of necessity, the new definition turns out to be conceptually simpler than the traditional definition of substitution.
8686702
Theory of Judgments and Derivations
We propose a computational and logical framework NF (Natural Framework) which is suitable for presenting mathematics formally. Our framework is an extendable framework since it is open-ended both computationally and logically in the sense of Martin-Lof's theory or types. NF is developed in three steps. Firstly, we introduce a theory of expressions and schemata which is used to provide a universe for representing mathematical objects, in particular, judgments and derivations as well as other usual mathematical objects. Secondly, we develop a theory of judgments within the syntactic universe of expressions. Finally, we introduce the notions of derivation and derivation game and will show that we can develop mathematics as derivation games by regarding mathematics as an open-ended process of defining new concepts and deriving new judgments. Our theory is inspired by Martin-Lof's theory of expressions and Edinburgh LF, but conceptually much simpler. Our theory is also influenced by Gentzen's natural deduction systems.
1580777
Classical Brouwer-Heyting-Kolmogorov Interpretation
The Brouwer-Heyting-Kolmogorov interpretation explains the meaning of logical operations as operators that construct proofs from proofs of the operands. The BHK interpretation is usually understood as giving intuitionistic interpretation for the logical operators, but, as pointed out by Troelstra and van Dalen [12], it is possible to understand the BHK interpretation classically. We elaborate this idea and develop a classical theory of proofs as abstract mathematical entities where the truth of a proposition becomes equivalent to the existence of proofs of the proposition.
32331384
Intuitionistic and Classical Natural Deduction Systems with the Catch and the Throw Rules
1796136
Strong normalizability of the non-deterministic catch/throw calculi
The catch/throw mechanism in Common Lisp provides a simple control mechanism for non-local exits. We study typed calculi by Nakano and Sato which formalize the catch/throw mechanism. These calculi correspond to classical logic through the Curry-Howard isomorphism, and one of their characteristic points is that they have non-deterministic reduction rules. These calculi can represent various computational meaning of classical proofs. This paper is mainly concerned with the strong normalizability of these calculi. Namely, we prove the strong normalizability of these calculi, which was an open problem. We first formulate a non-deterministic variant of Parigot's λμ-calculus, and show it is strongly normalizing. We then translate the catch/throw calculi to this variant. Since the translation preserves typing and reduction, we obtain the strong normalization of the catch/throw calculi. We also briefly consider second-order extension of the catch/throw calculi. Copyright 2002 Elsevier Science B.V
18311501
TACO -- Dynamic Distributed Collections with Templates and Topologies
High-level data-parallel programming with distributed object sets eases many aspects of parallel programming. In this paper we describe the design and implementation of Taco, a template library that provides higher-order operations on polymorphic regular and irregular distributed object sets by means of reusable topology classes and C++ function templates.
16720525
Resource manager for Globus-based wide-area cluster computing
In this paper, we present a new type of Globus resource allocation manager (GRAM) called RMF (Resource Manager beyond the Firewall) for wide-area cluster computing. RMF manages computing resources such as cluster systems and enables utilization of them beyond the firewall in global computing environments. RMF consists of two basic modules, a remote job queuing system (Q system) and a resource allocator. The Q system is a remote job queuing system, which schedules jobs submitted from global computing sites. The resource allocator manages resources and allocates them for requested jobs. For communications beyond the firewall between job processes, we designed the Nexus Proxy, which relays TCP communication links beyond the firewall. RMF and the Nexus Proxy provide a global computing environment in which users can easily utilize such parallel systems as cluster systems and supercomputers beyond the firewall.
10817469
COMPaS: A Pentium Pro PC-based SMP Cluster and Its Experience
We have built an eight node SMP cluster called COMPaS (Cluster Of Multi-Processor Systems), each node of which is a quadprocessor Pentium Pro PC. We have designed and implemented a remote memory based user-level communication layer which provides lowover-head and high bandwidth using Myrinet. We designed a hybrid programming model in order to take advantage of locality in each SMP node. Intra-node computations utilize a multi-threaded programming style (Solaris threads) and inter-node programming is based on message passing and remote memory operations. In this paper we report on this hybrid shared memory/distributed memory programming on COMPaS and its preliminary evaluation. The performance of COMPaS is affected by data size and access patterns, and the proportion of inter-node communication. If the data size is small enough to all fit on the cache, parallel efficiency exceeds 1.0 using the hybrid programming model on COMPaS. But the performance is limited by the low memory bus bandwidth of PC-based SMP nodes for some memory intensive workloads.
7463356
Integrating Computing Resources on Multiple Grid-enabled Job Scheduling Systems Through a Grid RPC System
We present a framework for a parallel programming model by remote procedure calls bridging between largescale computing resource pools managed by multiple gridenabled job scheduling systems. With this system, the user can exploit not only each remote servers and clusters, but also computing resources provided with grid-enabled job scheduling systems located on different sites. This framework requires a Grid RPC system to decouple the computation in a remote node from the Grid RPC mechanism and uses document-based communication rather than connection-based communication. We implemented the proposed framework as an extension of the OmniRPC system, which is a Grid RPC system for parallel programming in a grid environment. We designed a general interface to adapt the OmniRPC system to various grid-enabled job scheduling systems easily and applied the proposed system to several grid-enabled job scheduling systems, including XtremWeb, CyberGRIP, Condor and Grid Engine. we show the preliminary performance of these implementations using a phylogenetic application. We found that the proposed system can achieve approximately the same performance as using OmniRPC and can handle interruptions in worker programs on remote nodes.
1543066
Performance Evaluation of the Hitachi SR8000 Using SPEC OMP2001 Benchmarks
This paper reports the performance of a single node of the Hitachi SR8000 when using SPEC OMP2001 benchmarks. Each processing node of the SR8000 is a shared-memory parallel computer composed of eight scalar processors with pseudo-vector processing feature. We have run the all of the SPEC OMP2001 benchmarks on the SR8000. According to the results of this performance measurement, we found that the SR8000 has good scalability continuing up to 8 processors except for a few benchmark programs. The performance results demonstrate that the SR8000 achieves high performance especially for memory-intensive applications.