研究業績

The environment is the relationship between variables and their bound values during program execution and is a notion in program semantics. A first-class environment is a mechanism that allows the environment to be treated like data, such as integer values or Boolean values, and can be passed to a function as an argument or received as a return value. The environment calculus is a formal computational system proposed by Nishizaki and is a lambda calculus that extends the first-class environment mechanism. The formulation of the environment was based on explicit substitution by Curien et al., who viewed the environment as a substitution. The operational semantics of the environmental calculus, or the reduction, is based on the reduction of the lambda-sigma calculus. In the calculus, there are two constructs for first-class environments: one is the identity environment to reify the current environment, that is, to transfer a meta-level environment to object-level data; the other is the environment composition to reflect the object-level environment data, that is, to transfer object-level environment data back to a meta-level environment. In this paper, instead of the environment composition, we propose a new interface with a first-class environment, a functionally referable environment. If object-level environment data is given as an argument for a function application, the functional reflection brings the environment back to the meta-level and makes the lambda term evaluable under that environment. Using the functionally referable environment, one can unify the environment composition with the function application. We define the untyped lambda calculus with functionally referable environments: we give the syntax of the calculus and its reduction. Then we provide the semantics for the reduction using a translation of the environment calculus into the record calculus. We prove the soundness of the translation semantics. Finally, we discuss the evaluation strategy, especially the call-by-value reduction.

Design by Contract is a programming methodology by which it is possible to annotate program codes with contracts in order to increase the safety of the program. The contracts represent the specification of the software and are categorized into three groups: pre-condition, post-condition, and invariant. The idea of Design by Contract provides the correctness of a program code, satisfying that the caller of each procedure assumes the responsibility for the pre-condition and the callee assumes the responsibility for the post-condition. Findler et al. proposed a formal system based on the typed lambda calculus in which contracts are verified dynamically, that is, in run-time. Flanagan et al. introduced a formal system in which both static and dynamic checking of contracts are possible. In their system, it is possible to represent a contract as static, typing information using refinement type and dependent type. In our paper, we introduce the typed lambda calculus with dependent type and refinement type in the style of Flanagan and study a static analysis in the calculus. The static analysis provides refining of contracts and code optimization based on the contracts. We implement the analyzer using an SMT (Satisfiability Modulo Theory) server.

The Curry-Howard isomorphism shows that an intuitionistic deductive system is similar to a formal computational system; propositions correspond to types, proofs to lambda-terms, and a proof normalization procedure to an evaluation strategy. Furthermore, the duality between computation values and continuations is discovered under the Curry-Howard isomorphism. In the traditional lambda calculus, duplication and erasing of values are allowed but those of continuations prohibited. On the other hand, in the lambda calculus with first-class continuations, both values and continuations are permitted to be duplicated and erased. In our previous paper, we proposed a linear lambda calculus with first-class continuations, in which we cannot duplicate and erase values but can do continuations. In this paper, we propose an ML polymorphic type system for the linear lambda calculus with first-class continuations and design a type inference algorithm of the type system.

Recently, many companies in the Information Technology (IT) industry are shifting focus from software development to providing software services. So, the design thinking that proposes to start from the user's point of view is accepted by many industries. We executed the collaboration workshop that the IT students learn practical lean start-up by short-term PBL (Project Based Learning) with overseas engineers. There are two aims of the workshop. The one is an exercise of business idea creation and verification it using lean canvas. The other is the learning of team building and communication. The communication includes the team building. It is a just 5 days’ workshop, but the students got the progress in communication skills and also engineers improved their communication skills, business creation skills and changed their business viewpoint. In this paper, we report on its detail and efforts.

The categorical combinatory logic CCLβηSP is a combinatory logic motivated by the cartesian closed category, proposed by Pierre-Louis Curien. The combinatory logic is used for modeling of the lambda calculus and gives a design of an abstract machine, the Categorical Abstract Machine (CAM). The first-class environment is a mechanism in programming languages which enables us to manipulate an environment, that is, a mapping of variables to bound values. We have studied the lambda calculus with first-class environments for several years. In this paper, we depict that the first-class environment indwells in the categorical combinatory logic, giving the translation of the simply-typed lambda calculus with first-class environments into the categorical combinatory logic. We show the translation respects the typing and the reduction.

The Curry-Howard isomorphism is the correspondence between propositions and types, proofs and lambda-terms, and proof normalization and evaluation. In Curry-Howard isomorphism, we find a duality between values and continuations in pure functional languages with respect to logical negation. My previous paper and other researchers' studies reveal that we can obtain a first-class continuation mechanism by providing duplicability and removability of continuations, which is equivalent to the right-contraction and weakening rules in Gentzen's deductive system, the sequent calculus. In the lambda calculus, it is allowed to duplicate and remove values, but the continuations are impossible to duplicate and remove. In our previous paper, we showed that we can obtain the lambda calculus with first-class continuations providing duplicability and removability of both values and continuations. In this paper, we will study a calculus in which we only have duplicability and removability of continuations. We formalize this calculus in the framework of linear logic, which is a logical system sensitive to duplicability and removability, proposed by Jean-Yves Girard.

Unification is a useful process by which one attempts to find a substitute satisfying a given set of equations. Among several kinds of unification algorithms, the unification for equations between first-order terms is known to be decidable and to satisfy the completeness. A unification mechanism plays an important role in logic programming languages, such as Prolog. In this paper, we propose an approach to incorporating a unification mechanism into a functional programming language via first-class environments. The first-class environment is a reflective feature in a programming language, which enables us to reify environments, to handle them as first-class values such as integers and Boolean values, and to reflect the reified environment as an environment at a meta-level. By identifying resulting substitutions of unification problems as first-class environments, we can introduce unification into functional programming languages. In this paper, we first give the syntax of a simple functional language with unifications. Second, we give its operational semantics in the style of Kahn’s natural semantics. Finally, we introduce some related works and show the future direction of our works.

The environment is one of the execution states in programming language processors. The first-class environment is a reflective programming facility which enables us to use meta-level environments as object-level entities, and inversely, to use the object-level environments as meta-level entities. We named a lambda calculus with first-class environments the environment calculus, and studied various systems of the environment calculus. PCF (Programming Computable Functions) is a simply typed lambda calculus with natural numbers, Boolean values, and recursive operators, which was proposed as a formal framework for the semantical study of evaluation strategies.In this paper, we introduce an extended system of PCF with first-class environments and study evaluation strategies, such as call-by-name and call-by-value strategies.

A single-page application is a web application which is retrieved with a single page load, and has become popular recently. In such web applications, real-time interaction is offered by long polling of HTML requests, typically the Comet model. However, such communication between a client and a server is inefficient because of the TCP handshake and HTTP header overhead. In order to improve this kind of inefficiency, WebSocket is proposed as a web technology providing full-duplex communications between web browsers and servers. In this paper, we design and implement a load balancer suitable for Web applications using the WebSocket protocol, which enables us to get improved performance with respect to simultaneous connectability. Usually, load balancers handle TCP packets in the transport layer, or L4, of the network. Our load balancer is designed as a relay in the application layer, or L7, in order to provide a finer distribution of the network load. We implement the load balancer on an event-driven web application framework, Node.js. We evaluate the implementation of efficiency of the load balancer.

Nowadays, regulatory compliance is one of the most important issues in Japan. Due to the increasing number of regulations, it will not be easy to ensure that all governance requirements are fulfilled by the business processes of an information system. In this paper, we propose a new method of strengthening the compliance controls in information systems using model checking. We formulate an information system as a timed automaton and compliance requirements as CTL formulas. We employ the model checker UPPAAL to check whether the automaton satisfies the requirements. We apply our method to an example taken from Japanese banking regulations.

Programs contain variables, and the bindings of these variables to the corresponding values are kept in a so-called ’environment’. A first-class environment is a mechanism that the environments in programs can be treated as first-class entities, which are objects that can to be passed and returned between functions and procedures. Nishizaki proposed the lambda calculus with first-class environments, called the environment lambda calculus, and has investigated its theoretical properties [6–8, 10]. The various systems of the environment lambda calculus are based on weak reduction, that is, application of a substitution to a lambda abstraction is postponed until an argument is applied to it. In this paper, we propose a simply-typed lambda calculus with strong reduction. We investigate several theoretical properties such as the subject reduction theorem.

Nowadays, blogs are regarded as standard text-based communication tools on the internet. In contrast to traditional web pages, the blog has several significant features: it allows authoring via a web browser, and offers automatic backlink requesting, called trackback. The latter provides direct communication between blog servers. In this paper, we propose a distributed computation method based on trackback communication and present the implementation of a software verification system based on distributed computing. The software verification system consists of ordinary blog systems which are used as frontend interfaces, and verification blog bots which are used as backend inference engines. One of the prominent features is that one can limit the danger of intrusion into vulnerable verifier programs to the private networks where the verification blog bots are operated.

Since the 1960s, Fault Tree Analysis has been extensively used in Safety Engineering and Reliability Engineering, and other methodologies have been proposed. We study reliability analysis with formal methods. Fault tree analysis is one of the most popular methods of reliability analysis. With this, one analyzes the causes of a fault in a top-down manner. Model checking is an automatic verification method and has recently become popular. In this paper, we incorporate model checking into the fault tree analysis and show a case study of a pressure tank control system. Moreover, we propose a formal approach for introducing a fault detection mechanism. We show an example of a fault detection mechanism in the pressure tank control system, in which it is implemented using a set of lights to check electric current. We successfully show that model checking can evaluate the effectiveness of the fault detection mechanism.

Vulnerability of communication protocols can cause several kinds of attacks, which cause significant damage to systems connected to the Internet. Denial-of-service attack (DoS attack) is an instance of them. Analysis of resistance against DoS attacks is considered as significant. We previously proposed a formal framework for DoS attack resistance, the spice calculus. In this paper, we develop a method for analyzing communication protocols from the aspect of DoS attack resistance. In this method, we first formalize a communication protocol in terms of the spice calculus. Then we translate expressions of the spice calculus into timed automata and analyze them using the real-time model checker UPPAAL. We explain the method by showing an example of a simple communication protocol.

First-class continuations have proven convenient for expressing a variety of control structures. In existing programming languages and formal systems, continuations are usually reified as first-class functions. This means that simple calling is the only operation applicable to continuations. To investigate the benefits of other operations on first-class continuations, we propose a variation of the object calculus in which we can formalize continuations that allow contents to be accessed and/or modified. The object calculus is a series of formal systems proposed by Abadi and Cardelli that formulates object-oriented computation. The sigma-calculus is the simplest variation of such calculi. Nishizaki et al. extended the sigma-calculus by adding first-class continuations that are formalized as Plotkin and Felleisen-style evaluation contexts. In our calculus, which is a successor of this extended sigma-calculus, continuations are represented as mutable objects. Thus, the contents of continuations can be accessed/modified using normal operations on objects. This paper presents the syntax and operational semantics of the calculus, and provides examples describing the usage of the modifiable continuations.

Cooper and Wadler introduced the RPC calculus, which is obtained by incorporating a mechanism for remote procedure calls (RPC) into the lambda calculus. The location where a caller’s code is executed is designated in a lambda abstraction in the RPC calculus. Nishizaki et al. proposed a simplified abstract machine for the lambda calculus, known as a Simple Abstract Machine (SAM). The configuration of an SECD machine is a quadruple of data sequences: Stack, Environment, Code, and Dump. In contrast, the SAM configuration is a double of data sequences: Stack and Code. In this paper, we introduce a SAM-based abstract machine for the RPC calculus, called a Location-aware Simple Abstract Machine (LSAM). This machine makes it possible to model parallelism more clearly. We provide a translation of the RPC calculus into LSAM, and prove a correctness theorem for the translation. We then show that the translation can be extended to allow parallel execution in LSAM.

In order to describe and analyze cryptographic protocols, several researchers have proposed formal frameworks and have studied the security properties of communication protocols, such as authenticity. Abadi and Gordon used Milner’s pi-calculus for their research into security properties. The resistance to denial-of-service (DoS) attacks is one of the most important properties of communication protocols. This paper proposes a new calculus for analyzing the resistance to DoS. One crucial point that the analysis considers is the estimation of the resource consumption in each CPU. In the proposed calculus, the time and space costs for each CPU are determined by referring to its type and application data.

We are developing a secure and certified e-mail system AnZenMail that provides an experimental testbed for our cutting-edge security enhancement technologies. In addition to a provably secure message transfer protocol, we have designed and implemented a server (MTU) and a client (MUA) in order that they could survive recent malicious attacks such as server-cracking and e-mail viruses. The AnZenMail server is implemented in Java, a memory-safe language, and so it is free from stack smashing. Some of its safety properties have been formally verified in Coq mostly at the source code level by manually translating Java methods into Coq functions. The AnZenMail client is designed to provide a support for secure execution of mobile code arriving as e-mail attachments. It has plug-in interfaces for code inspection and execution modules such as static analysis tools, runtime/inline reference monitors, and an anti-virus engine, which are currently being developed by members of our research project.

The polymorphic environment calculus is a polymorphic lambda calculus which enables us to treat environments as first-class citizens. In the calculus, environments are formalized as explicit substitutions, and the substitutions are included in the set of terms of the calculus. First, we introduce an untyped environment calculus, and we present a semantics of the calculus as a translation into the lambda calculus. Second, we propose a polymorphic type system for the environment calculus based on Damas-Milner's ML-polymorphic type system. In ML, polymorphism is allowed only in let-expressions; in the polymorphic environment calculus, polymorphism is provided with environment compositions. We prove a subject-reduction theorem for the type system. Third, a type-inference algorithm is given to the polymorphic environment calculus, and we establish its soundness, termination, and principal-typing theorem.

グラフの探索問題は計算機科学の諸分野で基礎理論として用いられ,対象領域に沿った様々な最適化アルゴリズムが提案されている。これらの最適化アルゴリズムは高度な工夫や複雑な前提条件のためにその正当性が必ずしも自明ではなく,形式的検証の対象として相応しいと言える。証明検証系による形式的検証の効果を最大限に発揮するには,問題領域の適切な抽象化が不可欠である。本論文では,グラフ探索アルゴリズムのあるクラスの抽象化と実際の検証,最適化アルゴリズムの検証への発展について述べる。さらに,状態空間がなすグラフの網羅的探索によって検証を行うモデル検査について,そこで用いられるアルゴリズムの検証への応用に関して述べる。

This paper describes a formalization of a class of fixed-point problems on graphs and its applications. This class captures several well-known graph theoretical problems such as those of shortest path type and for data flow analysis. An abstract solution algorithm of the fixed-point problem is formalized and its correctness is proved using a theorem proving system. Moreover, the validity of the A* algorithm, considered as a specialized version of the abstract algorithm, is proved by extending the proof of the latter. The insights we obtained through these formalizations are described. We also discuss the extension of this approach to the verification of model checking algorithms.

We have developed a knowledge-based but partially analytic simulation system. This system simulates regulatory action in lambda phage, a virus which infects E. coli. Specifically, we simulated the decision between its two developmental pathways, lytic and lysogenic growth. Our model is composed of two levels: roughly abstracted level and precisely abstracted level. The former level is discrete-event and knowledge-based. It covers overall regulations inside lambda phage in qualitative representation. On the other hand, the latter is based on quantitative chemical equations describing the sensitive bifurcation within pathways. In this way, qualitatively clear overview of regulatory action is efficiently simulated using knowledge base, and only the unpredictable part is analytically simulated in detail. This system can output not only input knowledge but also precise prediction by computational analysis, data which help molecular biologists find new theories of regulatory actions.

We present a typed λ-calculus which enables us to handle first-class environments. The syntax and the reduction are obtained by applying the idea of Curien's “explicit substitution”. The type system has ML-polymorphism and a type inference algorithm which is sound and terminates.

A programming language with continuations is studied in the framework of Girard's linear logic. The execution of a program with continuations is in general non-deterministic: the result of computation depends on the evaluation strategy, e.g. call-by-value evaluation, call-by-name evaluation, ..., etc. In this paper, we first introduce λ →_{c} , a programming language with continuations, and then define the translation from λ →_{c} to linear logic, which eliminates the non-determinism of λ →_{c}. The relation between computation of λ →_{c} and normalization of linear logic is also shown.