香川考司（香川大学工学部）

２００７年６月１１日（月）・１２日（火）、７月９日（月）・１０日（火） １３：３０〜１７：００
京都大学数理解析研究所１０２号室

本講義では、関数型プログラミング言語Haskellについて、 その理論的基礎から実際的な応用までを解説する。 Haskellは、副作用を持たない、 CやJavaなどいわゆる“主流の言語”とは一風変わったプログラミング言語である。 また、強力な型システムを持つことも大きな特徴である。 本講義では、おもに次のようなトピックについて説明する。

• 遅延評価
• 型クラス
• リスト内包表記とモナド
• パーサコンビネータ

蓮尾一郎

２００７年４月２６日（木）１４：００〜１５：００
旧工学部７号館・コンピュータサイエンス室

Coalgebras are categorical presentations of state-based systems. In considering parallel composition of coalgebras (realizing "concurrency"), we observe that the same algebraic structure (e.g. the binary operation || for parallel composition and its associativity) occurring in two different domains, in a nested manner, namely: on the category CoAlg(F) and on its final object (Z -> FZ). This is an instance of what is called the microcosm principle, a prototypical example of which is the nested structure "a monoid is defined in a monoidal category". We formalize the microcosm principle using Lawvere theories in a 2-categorical setting. From this general account, we get the compositionality result (saying "behavior of a composed system is determined by that of each component") for free.

(Joint work with Bart Jacobs and Ana Sokolova)

Ewen Denney (NASA Ames Research Center，US)

２００６年９月２５日（月）１６：００ 〜
京都大学数理解析研究所２０２号室

Software is playing an increasingly important role in space missions, and as NASA transitions from the space shuttle to the new Orion Space Vehicle, this trend will certainly continue. However, new techniques are needed to give the high levels of assurance that are required for safety and mission critical software. Program synthesis (also known as automated code generation) is a technology which could be applied in many NASA missions, but concerns over the safety and comprehensibility of generated code have hampered its widespread adoption. One solution to the safety problem is to extend the generator in such a way that it automatically certifies that the code it generates is safe, a technique we call certifiable program synthesis. I will describe the domain-specific code generators, AutoBayes and AutoFilter, which work in the domains of data analysis and state estimation, respectively, and give an overview of some of the techniques used to achieve safety.

中田 景子

勝股 審也

２００６年９月５日（火）１４：００〜
京都大学数理解析研究所２０２号室

Philip Wadler (University of Edinburgh)

２００６年４月２８日（金）１４時〜
京都大学数理解析研究所１階１１５号室

Links is a programming language for web applications. Links generates code for all three tiers of a web application from a single source, compiling into JavaScript to run on the client and into SQL to run on the database. Links provides support for rich clients running in what has been dubbed `Ajax' style. Links programs are scalable in the sense that session state is preserved in the client rather than the server, in contrast to other approaches such as Java Servlets or PLT Scheme.

The Girard-Reynolds isomorphism (second edition)

２００６年４月２８日（金）１６時〜
京都大学数理解析研究所１階１１５号室

Martin Berger (Queen Mary, University of London)

２００６年３月２４日１４：００〜
京都大学数理解析研究所１１５号室

We present a compositional program logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters, return values, content of references and parts of data tructures. The program logic extends our earlier logic for alias-free imperative higher-order functions with new modal operators which serve as building blocks for clean structural reasoning about programs and data structures in the presence of aliasing. This has been an open issue since the pioneering work by Cartwright-Oppen and Morris twenty-five years ago. We illustrate usage of the logic for description and reasoning through concrete examples including a higher-order polymorphic Quicksort. The logical status of the new operators is clarified by translating them into (in)equalities of reference names. The logic is observationally complete in the sense that two programs are observationally indistinguishable iff they satisfy the same set of assertions. (Joint work with Kohei Honda and Nobuko Yoshida)

Vincent Schmitt (University of Leicester)

２００５年１２月２７日（火）１１：００〜
京都大学数理解析研究所２０２号室

This talk will be a survey on enriched category theory including recent results obtained with Max Kelly. I will recall the notion of saturated classes of weights due to Albert and Kelly. I will show that it brings considerable conceptual simplifications for the study of categories with colimits of some class: accessible categories and Cauchy-completeness. Depending on time I could say more regarding categories of continuous functors.

Irek Ulidowski (University of Leicester)

２００５年１１月２８日（月）１４：００〜
理学部６号館６階６０９号室

Reversible computation has a growing number of promising application areas such as the modelling of biochemical systems, program debugging and testing, and even programming languages for quantum computing. We formulate a procedure for converting operators of standard algebraic process calculi such as CCS, ACP and CSP into reversible operators, while preserving their operational semantics. We define a forward-reverse bisimulation and prove that it is a congruence for all reversible operators. (Joint Work with Iain Phillips)

結縁祥治 (名古屋大学大学院情報科学研究科)

２００５年７月１６日（火）〜２２日（金） １４：００〜１６：００
理学部数学教室１０９号室（３号館１階）

本講義では、CCS、CSPなどをはじめとする通信プロセスモデルによ る並行計算モデルとその上で展開される代数的意味論について述べ る。通信プロセスモデルは並行に実行されるプロセスが互いに同期 通信を行いながら計算が進行する形式的な計算モデルである。この モデルにおける特徴は、プロセスによる通信を観測して意味論を構 築することである。このことによって、計算が開始される前の入力 と終了後の出力を観測する伝統的な関数による計算の意味づけを一 般に拡張した意味論が展開することが可能になり、並行計算のもつ 非決定性、非停止性などの特徴を表現することができる。本講義で は、通信プロセスモデルにおける基本的な双模倣意味論による代数 的な意味論、様相論理による特性化、等式にもとづく公理的な特性 化などの基本的な意味付けについて述べ、一般的な意味論構築のた めの構造動作意味定義(SOS)のための理論、時間および確率などの拡 張、さらに、時間の許す範囲で近年盛んに研究されているπ計算の 動作意味についても述べる。

Donald Sannella (University of Edinburgh)

２００５年６月２日（木）１４：００〜
京都大学数理解析研究所００９号室

The Mobile Resource Guarantees (MRG) project is building infrastructure for endowing mobile bytecode programs with independently verifiable certificates describing their resource consumption. These certificates will be condensed and formalised mathematical proofs of a resource-related property which are by their very nature self-evident and unforgeable. Arbitrarily complex methods may be used to construct such a certificate, but once constructed its verification will always be a simple computation. This makes it feasible for the recipient to check that the proof is valid, and so the claimed property holds, before running the code. This work falls within an area known as "proof carrying code". Our focus in MRG on quantitative resource guarantees is different from the traditional PCC focus which is security. Another novelty is the method to be used to generate proofs, which is to use a "linear" type system that classifies programs according to their resource usage as well as according to the kinds of values they consume and produce. The intention is to generate proofs of resource usage from typing derivations. The MRG project (IST-2001-33149), which is a collaboration between the University of Edinburgh and LMU Munich, is funded by the European Commission under the FET proactive initiative on Global Computing. See http://groups.inf.ed.ac.uk/mrg/ for more information.

Paul-Andre Mellies (Universite Paris VII)

２００５年１月２６日（水）１４：００〜
京都大学数理解析研究所２０６号室

In game semantics, the higher-order value passing mechanisms of the lambda-calculus are decomposed as sequences of atomic actions exchanged by a Player and its Opponent. Seen from this angle, game semantics is akin to trace semantics in concurrency theory, where a process is identified to the sequences of requests it generates in the course of time. Asynchronous game semantics is an attempt to bridge the gap between the two subjects, and to see mainstream game semantics as a refined and interactive form of trace semantics. Asynchronous games are positional games played on Mazurkiewicz traces, which reformulate (and generalize) the usual notion of arena game. The framework enables to analyze the interleaving semantics of lambda-terms, expressed as innocent strategies, in the perspective of true concurrency. The analysis reveals that innocent strategies are positional strategies regulated by forward and backward confluence properties. A further distinction between external and internal positions in asynchronous games leads to the very first sequential game model of full propositional linear logic --- in the style of Blass games.

中田景子

２００４年１２月１６日（木）１４：００〜
数理解析研究所 １１５号室

ML-style modules and classes are complementary. The former are better at structuring and genericity, the latter at extension and mutual recursion. We investigate the convergence of both mechanisms by designing an object-oriented calculus based on a nominal module system with mutual recursion. Our modules assume simultaneously the roles of classes with subtyping, nested structures with type members, and simple functors. Flexible inter-module recursion is obtained by allowing free references not constrained by the order of definitions. Close examination of the well-foundedness of the recursion is performed, in the presence of nesting and functors. To keep the mutual recursion seen in object-oriented languages, we propose an innovative approach to the well-foundedness, by considering the topological sortability of modules. Its static inspection is possible at the cost of some forms of parametricity. The presented type system is provably decidable, and ensures well-foundedness of the recursion. The paper also presents a call-by-value semantics, for which type soundness is proved.

[To be presented at the International Workshop on Foundations of Object-Oriented Languages (FOOL-12), joint work with Akira Ito and Jacques Garrigue]

Erik Poll (University Nijmegen)

２００４年１２月１０日（金）１５：００〜
数理解析研究所 ００９号室

Algebras and coalgebras are dual notions, and are in some intuitive sense `opposites'. However, algebras and coalgebras also have certain things in common. (For example, the standard example of an algebraic specification, stacks, also occurs in the literature as an example of a coalgebraic specification.)

The notion of dialgebra, introduced by Hagino, generalises the notions of algebra and coalgebra. We investigate in how far properties of (co)algebras - in particular properties of invariants and bisimulations - can be generalised to arbitrary dialgebras, to get a better understanding of what the essential differences between algebras, coalgebras, and dialgebras are. We relate the notion of observational equivalence for dialgebras can be seen as a special case of observational equivalence of abstract datatypes (eg., as provided in the second-order lambda calculus) in type theory.

中田 景子 ／ 石原 存

中田 景子
相互参照のあるオブジェクト指向モジュールシステム

石原 存
下極限に基づく無限項書換え系

西村 進（理・数学）

２００４年８月１６日（月）１４：００〜
理学部６号館 ６０９号室

We propose a new algorithm for fusion transformation that allows both stacks and accumulating parameters. The new algorithm can fuse programs that cannot be handled by existing fusion techniques. The algorithm is formulated in a modular, type-directed style where the transformation process is comprised of several transformation steps that change types but preserve the observational behavior of programs. We identify a class of functions to which our new fusion method successfully applies and show that a closure property holds for that class. (to be presented at PEPM'04)

大崎 人士（産総研）

２００４年７月２６（月）- ３０（金） １４：００ - １５：３０
理学部数学教室１０９号室（３号館１階）

本講義では，書換系(かきかえけい)とツリー・オートマトンを 数理的な枠組みとする．はじめに，書換系についての基本概念 についての解説をする．次に，書換系のひとつのインスタンス としてのツリー・オートマトンに話題を移し，閉包性および決 定可能性の問題について述べる．さらに，最近の研究成果によ り明らかとなった等式付ツリー・オートマトンとペトリネット (等式付書換系の一種)との関連，等式付ツリー・オートマトン をもとに定義される言語階層の形式言語論的な解釈をおこなう． さらに，システム検証の自動化に向けた最近の研究の取り組み について，デモンストレーションなどを交えて紹介する．

（情報学研究科 佐藤研究室と共催）

西村 進 （理・数学）

２００３年１１月２１日（金）１６：００〜
数理解析研究所００９号室

The syntactic logical relations developed by Pitts are applied to show the correctness of a higher-order removal program transformation algorithm. The convenient proof method that resorts to the induction on the structure of programs does not apply because of the circular references to be introduced by the transformation. In this talk, it is shown that a relational reasoning based on a variant of the syntactic logical relations, where every pair of the transformation source and target are related, can break the circularity and make an inductive proof go through.

勝股 審也 (LFCS, University of Edinburgh)

２００３年８月８日（金）１６：００〜
数理解析研究所１１５号室

We extend the study of the relationship between behavioural equivalence and indistinguishability relation to the simply typed lambda calculus, where higher-order types are available. The main technical tool of this study is pre-logical relations, which give a precise characterisation of behavioural equivalence. We establish a relationship between behavioural equivalence and indistinguishability in terms of factorisability. We then consider a higher-order logic to reason about models of the simply typed lambda calculus, and relate the resulting standard satisfaction relation to behavioural satisfaction.

角谷 良彦

２００３年５月２８日（水）１６：００〜
数理解析研究所２０６号室

The $\lambda\mu$-calculus features both variables and names, together with their binding mechanisms. This means that constructions on open terms are necessarily parameterized in two different ways for both variables and names. Semantically, such a construction must be modeled by a bi-parameterized family of operators. In this paper, we study these bi-parameterized operators on Selinger's categorical models of the $\lambda\mu$-calculus called control categories. The overall development is analogous to that of Lambek's functional completeness of cartesian closed categories via polynomial categories. As a particular and important case, we study parameterizations of uniform fixed-point operators on control categories, and show bijective correspondences between parameterized fixed-point operators and non-parameterized ones under uniformity conditions.

(Joint work with Masahito Hasegawa, to appear in TLCA'03)

２００３年５月１５日〜１６日
数理解析研究所１１５号室
（京都大学数理解析研究所短期共同研究）

Irek Ulidowski (University of Leicester)

２００３年４月７日（月）１６：００〜
数理解析研究所１０２号室

A process language framework for concurrent systems is presented. The framework is defined using the Ordered Structural Operational Semantics (OSOS) approach, where traditional Plotkin-style SOS rules have orderings associated with them. The orderings allow one to control the order of application of SOS rules when deriving transitions of process terms. The framework is very expressive: it allows one to express easily a wide range of functional and temporal behaviour of concurrent systems. Also, it allows the user to define new task specific operators and features such as, for example, the notion of time and random delays.

Once the user has chosen her process language (i.e. the operators, time and other features, and a suitable semantics), the process language is given an operational definition by means of OSOS rules and orderings on rules. Depending on the chosen semantics, OSOS rules and semantics must satisfy several simple conditions. These conditions restrict the structure of OSOS rules and the type of rule orderings that can be used. As a result, the defined process language preserves the chosen semantics. As an example, a class of OSOS process languages preserves bisimulation semantics. Several other classes of process languages that preserve weak semantics, e.g. testing equivalence and eager bisimulation, will be briefly discussed.

Software tools such as Concurrency Workbench and PAC (Process Algebra Compiler) can be adapted to accept general process languages and to perform simple verification with respect to the chosen semantics.

Nobuko Yoshida (Department of Computing, Imperial College)

２００３年３月４日（火）１５：００〜
数理解析研究所２０６号室

Fedor Fomenko (LFCS, University of Edinburgh)

２００３年２月２６日（水）１６：００〜
数理解析研究所２０６号室

I will briefly describe known implicit characterisation of feasible computations and then try to outline how one can try to understand these categorically.

中野 圭介

２００３年１月２２日（水）１６：００〜
数理解析研究所２０６号室

We present a composition method for stack-attributed tree transducers. Stack-attributed tree transducers extend attributed tree transducers with a pushdown stack device for attribute values. Stack-attributed tree transducers are more powerful than attributed tree transducers due to the stack mechanism. We extend an existing composition method for attributed tree transducers to the composition method for stack- attributed tree transducers. The composition method is proved to be correct and to enjoy a closure property. In this talk, we also present a practical application of the composition method, that is an XML stream transformer generator.

In the talk, I will assume just a working mathematician's knowledge of topology. No knowledge of computation will be required.

２００２年１２月２０日（金）１１：００〜
数理解析研究所１１５号室

２００２年１２月１６日〜１９日
数理解析研究所１１５号室
（京都大学数理解析研究所短期共同研究）

２００２年１２月６日（金）１１：００〜
数理解析研究所４０２号室

細谷 晴夫

２００２年１２月４日（水）１６：００〜
数理解析研究所２０６号室

XML data are described by types involving regular expressions. This raises the question of what a convenient language feature is to manipulate such data. Previous proposals for XML processing languages such as XSLT and XQuery typically provide a ``for each'' loop construct. However, it only permits the independent processing of each children node and has no way to exploit the full structure of regular expressions. In this talk, I propose a novel programming feature {\em regular expression filters}. This construct stems from our previous proposal, regular expression pattern matching, which is inspired by the corresponding ML-style construct. We extend it by allowing pattern clauses to be closed under arbitrary regular expression operators, yielding a significat expressiveness. In particular, a clause closed by a Kleene star can iterate on sequences with no need to write an explicit recursion. In addition, we equip a typing inference mechanism that obtains (1) types for pattern variables that are {\em locally precise} with respect to the type of input values and (2) a type for the result of the whole filter expression that is also locally precise with respect to the types of the body expressions. I discuss how our construct is useful in the practice of XML processing and, in particular, how our type inference is crucial when type evolution is involved.

２００２年１１月２２日（金）１１：００〜
数理解析研究所４０２号室

長谷川 真人

２００２年１１月２０日（水）１６：００〜
数理解析研究所２０６号室

We give a simple term calculus for the multiplicative exponential fragment of Classical Linear Logic, by extending Barber and Plotkin's system for the intuitionistic case. The calculus has the non-linear and linear implications as the basic constructs, and this design choice allows a technically managable axiomatization without commuting conversions. Despite this simplicity, the calculus is shown to be sound and complete for category-theoretic models given by *-autonomous categories with linear exponential comonads.

This talk is largely based on the paper presented at CSL'02 (available from here).

２００２年１１月１５日（金）１１：００〜
数理解析研究所４０２号室

西村 進

２００２年１１月１３日（水）１６：００〜
数理解析研究所２０６号室

Classical deforestation methods fail to compose functions with accumulating parameters, which are function arguments to which intermediate result accumulates. This paper proposes a new deforestation method which solves this problem. The method is comprised of a few transformation steps, each of which is guided by type information. Though our solution draws its fundamental idea from a deforestation method that has been developed for attribute grammars, it is not merely a recast of an existing technique to another formalism. The new method provides a type-based account for the existing attribute grammar deforestation process. Further, it can deforest a class of functions that the attribute grammar deforestation cannot. These advantages are demonstrated by a few examples. It is also shown that the new method is as powerful as another method that has been developed for macro tree transducer composition.

A draft version of the accompanied paper (being prepared for APLAS'02 workshop) is available from here.

２００２年１１月８日（金）１１：００〜
数理解析研究所４０２号室

Jacques Garrigue

２００２年１１月６日（水）１６：００〜
数理解析研究所２０６号室

Restricting polymorphism to values is now the standard way to obtain soundness in ML-like programming languages with imperative features. While this solution has undeniable advantages over previous approaches, it forbids polymorphism in many cases were it would be sound. We use a subtyping based approach to recover a small part of this lost polymorphism, without changing the type algebra itself, and this has significant applications.

沢田 潤 （IBM Austin Research Lab）

２００２年８月１６日（金）１５：００〜
数理解析研究所２０２号室

The IBM Power4(TM) processor uses Chebyshev polynomials in the calculation of square root. We formally verified the correctness requirement of this algorithm using the ACL2(r) theorem prover. Such a formal verification is critical to guarantee the quality of a microprocessor.

The ACL2 theorem prover is a descendent of the Boyer-Moore prover, and it is both a programming system and a mechanical theorem proving system. The ACL2 prover does not axiomatize the real numbers, thus the user cannot prove any theorems involving irrationals. ACl2(r) is an extension of the ACL2 prover for real numbers, by way of the non-standard analysis introduced by Robinson. The ACL2(r) prover has been used to prove various theorems such as the correctness of the Fast Fourier Transformation (FFT) algorithm and the Fundamental Theorem of Analysis.

Here, we discuss the use of ACL2(r) in the analysis of a square root algorithm used in an industrial processor. This is done, by first proving Taylor's theorem, and then used it to analyze the size of the rounding and approximation error of the algorithm.

One challenge in formally verifying this particular algorithm is in the analysis of the Chebyshev polynomial. Since a Taylor polynomial has less accuracy than the Chebyshev polynomial of the same degree, the error measurement of a Chebyshev polynomial using a Taylor polynomial is not straightforward. We instead used hundreds of Taylor polynomials to evaluate the error size of a Chebyshev polynomial. This approach makes the error size analysis easier to automate.

五十嵐 淳 （京大・情報）／住井 英二郎 （東大・情報）

五十嵐 淳（１６：００〜）
On Variance-Based Subtyping for Parametric Types

We develop the mechanism of variant parametric types, inspired by structural virtual types by Thorup and Torgersen, as a means to enhance synergy between parametric and inclusive polymorphism in object-oriented languages. Variant parametric types are used to control both subtyping between different instantiations of one generic class and the visibility of their fields and methods. On one hand, one parametric class can be used as either covariant, contravariant, or bivariant by attaching a variance annotation---which can be either +, -, or *, respectively---to a type argument. On the other hand, the type system prohibits certain method/field accesses through variant parametric types, when those accesses can otherwise make the program unsafe. By exploiting variant parametric types, a programmer can write generic code abstractions working on a wide range of parametric types in a safe way. For instance, a method that only reads the elements of a container of strings can be easily modified so that it can accept containers of any subtype of string.

The theoretical issues are studied by extending Featherweight GJ---an existing core calculus for Java with generics---with variant parametric types. By exploiting the intuitive connection to bounded existential types, we develop a sound type system for the extended calculus.

This is joint work with Mirko Viroli.

住井 英二郎（１７：００〜）
Syntactic Logical Relations for Perfect Encryption, Higher-Order References and First-Class Channels

\emph{Logical relations} are relations between values in a programming language, defined by induction on their types. They were developed in the domain of denotational semantics for proving various relationships among mathematical models of typed lambda-calculi. In particular, they are known to be useful for proving contextual equivalence of different implementations of abstract types [Reynolds 83] and deriving so-called "free theorems" about polymorphic functions [Wadler 89].

This talk presents the definitions and applications of logical relations for a broader range of programming constructs such as (perfect) encryption, (higher-order) references, and (first-class) channels in concurrent languages. In spite of this diversity, the logical relations are based on a single idea of associating each \emph{generative name} $n$ with a relation $\phi(n)$ between values involved in $n$. All of these developments are syntactic and operational: that is, there are no CPOs and no categories.

Half of this talk is about premature work. Suggestions and discussions are welcome.

Jean-Philippe Vert（京都大学化学研究所バイオインフォマティクスセンター）

２００２年７月１２日（金）１６：００〜１７：００
数理解析研究所２０２号室

A major goal of post-genomic era reasearch is to better understand the functions and interactions of genes discovered during the sequencing projects recently completed. To this end new technologies such as DNA chips or Yeast 2-hybrid systems are routinely used to produce large amounts of data aimed at characterizing each gene.

In order to integrate these various types of information we propose a mathematical framework where a particular type of information is encoded into a kernel function on the set of genes, and where the comparison of two types of information can be performed using linear data mining methods in the corresponding reproducible kernel Hilbert spaces. As an application we show how to extract correlations between microarray data on the one hand, and gene networks on the other hand.

[Joint work with Naoki Kobayashi]

２００２年４月４日〜５日
数理解析研究所１１５号室
（京都大学数理解析研究所短期共同研究）

Martin Hofmann (University of Muenchen)

２００２年３月８日（金）１６：００〜
数理解析研究所２０６号室

Linear typing schemes guarantee single-threadedness and so the soundness of in-place update with respect to a functional semantics. But linear schemes are restrictive in practice, and more restrictive than necessary to guarantee soundness of in-place update. This has prompted research into static analysis and more sophisticated typing disciplines, to determine when in-place update may be safely used, or to combine linear and non-linear schemes. Here we contribute to this line of research by defining a new typing scheme which better approximates the semantic property of soundness of in-place update for a functional semantics. We begin from the observation that some data is used only in a ``read-only'' context after which it may be safely re-used before being destroyed. Formalizing the in-place update interpretation and giving a machine model semantics allows us to refine this observation. We define three \emph{usage aspects} apparent from the semantics, which are used to annotate function argument types. The aspects are (1) used destructively, (2) used read-only but shared with result, and (3) used read-only and not shared.

Lennart Beringer (LFCS, University of Edinburgh)

２００１年１１月５日（月）１６：００〜
数理解析研究所１１５号室

We consider processor architectures where communication of values is achieved through operand queues instead of registers. Explicit forwarding tags in an instruction's code denote the source of its operands and the destination of its result. We give operational models for sequential and distributed execution, where no assumptions are made about the relative speed of functional units. We introduce type systems which ensure that programs use the forwarding mechanism in a coordinated way, ruling out various run time hazards. Deadlocks due to operand starvation, operand queue mismatches, non-determinism due to race conditions and deadlock due to the finite length of operand queues are eliminated. Types are based on the shape of operand queue configurations, abstracting from the value of an operand and from the order of items in operand queues. Extending ideas from the literature relating program fragments adjacent in the control flow graph, the type system is generalised to forwarding across basic blocks.

長谷川 真人

２００１年１０月２４日（水）１６：００〜
数理解析研究所２０６号室

今年のContinuation Workshop (CW'01)でBerdine達が発表した"linearly used continuations"の仕事を、MLやSchemeのような副作用（effects）を持つ 値呼びプログラミング言語に対応するcalculusからlinear lambda calculusへ のコンパイル（monadic変換）として定式化・一般化して、syntax・semantic 両面から攻める...という、現在進行中の研究です。特に、continuationの場 合には、linear lambda calculusへのCPS (continuation-passing style) 変 換が、fully completeという良い性質を持つことがわかっています。

この型システムの設計には、スキーマの正規性を多用している。正規性とは、 スキーマがツリーオートマトン（ツリーを受理する有限状態機械）と等価とい うことである。これによって、２つのスキーマの和、積、もしくは差を表すス キーマを計算することが可能であるということや、包含関係を判定することも 可能であることがわかる。特に、本型システムにおける部分型は包含関係であ ると定義され、ユーザに高い柔軟性を提供するために重要である。一方、包含 関係の判定は指数時間完全という高い計算量を持つことがわかっている。その ため本研究では、実際の入力に対しては実用的速度で動作する「トップダウン」 なアルゴリズムを開発した。

Jacques Garrigue

２００１年１０月１０日（水）１６：００〜
数理解析研究所２０２号室