講演の概要
Daniel GAINA(北陸先端科学技術大学院大学 情報科学研究科)Logical foundation of proof score method in OTS/CafeOBJ (Joint work with Kokichi Futatsugi and Kazuhiro Ogata)TBA
Rene Vestergaard(北陸先端科学技術大学院大学 情報科学研究科)The CEq approach to formal scientific reasoningThe CEq (or Cascaded Equilibria) Formal Method aims to infer emergent properties from modal influence graphs (MIGs) --- MIG is a generic specification language that is inspired by biochemical concepts and that covers a large class of reactive systems. I will outline what the above means, discuss in what sense CEq is a formal method, showcase how CEq can be used to validate lines of argumentation about gene regulation, and give my answers to some of the questions asked by the workshop.
二木 厚吉(北陸先端科学技術大学院大学 情報科学研究科)An overview of proof score method in OTS/CafeOBJ (Joint work with Kazuhiro Ogata and Daniel Gaina)TBA
五十嵐 淳(京都大学大学院情報学研究科) A Type System to Promote Code Reuse in JavaJava is a type-safe language in the sense that the type system can statically guarantee the absence of certain classes of run-time errors such as no such field or method. However, it is often the case that programmers (are forced to) use unsafe features such as downcasts to write reusable object-oriented code "naturally". In this talk, I'll address a problem of extending mutually recursive classes and present a type system to solve the problem. (Joint work with Yoshinori Hirose, Chieri Saito, and Mirko Viroli)
勝股 審也(京都大学数理解析研究所)Attribute Grammars and Categorical SemanticsWe give a new formulation of attribute grammars (AG for short) called {\em monoidal} {\em AGs} in traced symmetric monoidal categories. Monoidal AGs subsume existing domain-theoretic, graph-theoretic and relational formulations of AGs. Using a 2-categorical aspect of monoidal AGs, we also show that every monoidal AG is equivalent to a synthesised one when the underlying category is closed, and that there is a sound and complete translation from local dependency graphs to relational Ags.
大岩 寛(産業技術総合研究所 情報セキュリティ研究センター)産業技術総合研究所 情報セキュリティ研究センター ソフトウェアセキュリティチームの研究紹介TBA
星野 直彦(京都大学数理解析研究所)polymorphic lambda calculusの等式理論についてTBA
木下 佳樹(産業技術総合研究所 システム検証研究センター)産業技術総合研究所 システム検証研究センターの紹介TBA
河原 康雄(九州大学システム情報科学研究院)Axiom of choice and Zorn's lemma in Dedekind categories集合論の初歩における選択公理とZornの補題の同等性を 関係圏において、要素を使わないで証明する。
津曲 紀宏(鹿児島大学大学院理工学研究科)Two examples of probabilistic Kleene algebraWe talk about two examples of probabilistic Kleene algebra introduced by McIver and Weber for verification of probabilistic distributed systems. One of the examples is given by McIver and Weber to interpret probabilistic distributed systems in it. The other consists of multirelations satisfying certain conditions, which is given in our RelMiCS10/AKA5 paper.
浅田 和之(京都大学数理解析研究所)Extensional Universal Types for Call-by-ValueWe clarify the possibility of extensional universal types in second-order polymorphic call-by-value programing languages. Unlike products in call-by-value, extensional universal types is genuinely right adjoint to the weakening, i.e., \beta-and \eta-equality hold for not only values but all terms. We use a ``relevant'' parametric model, and show that there is a reasonable class of computational effects which have extensional universal types in the model. This class of effects admits polynomial-like construction including initial algebras, and the examples contain non-termination, exception, global state, input/output, and list-non-determinism.
浜名 誠(群馬大学工学研究科)Inductive Cyclic Sharing Data StructuresWe give an initial algebra characterisation of cyclic sharing data structures. We also show that this provides mathematically clean applications in Haskell: implemetation of cyclic sharing data structures by GADTs and a notation for Arrows with loops.
照井 一成(京都大学数理解析研究所)Towards a logical foundation of computational complexityTraditional theories of computational complexity are built on concrete machine models. As a result, the nature of explanation often tends to be procedural (eg. via transformation of machines). Aiming at a more algebraic account to complexity theoretic phenomena (eg. via logical isomorphisms), we propose a new foundation based on logic and functional computation in the paradigm of Curry-Howard correspondence. The underlying framework is ludics of J.-Y. Girard, that is a pre-logical system upon which ordinary logics are to be built and analyzed. Due to its monistic nature, data and machines are both represented by abstract proofs, and acceptance of a word by a machine is replaced by a fundamental notion of orthogonality. Space efficient composition of algorithms (which is usually explained by a peculiar construction of machines) is very naturally achieved by adopting a pointer-based normalization procedure (known as Krivine's abstract machine). After introducing the basic formalism, we shall illustrate how some basic complexity theoretic phenomena (eg. space compression) are explained by logical properties (eg. focalization) and logical isomorphisms.
石田 俊一(九州大学大学院システム情報科学府情報理学専攻) Implication and Functional Dependency in Intensional Contexts内包文脈における関数従属性と含意従属性がアームストロングの推論規則に対し完全であることを、 構文論と意味論を整理した、Willeらとは異なる証明を与えて示した。また、関数従属性と含意従属性 の違いについて例を用いて述べる。
蓮尾 一郎(京都大学数理解析研究所)Coalgebras in a Kleisli category: generic theory for traces and simulationsTBAThe microcosm principle and concurrency in coalgebraTBA
西村 進(京都大学大学院理学研究科)Safe Modification of Pointer Programs in Refinement CalculusTBA
西澤 弘毅(東北大学大学院情報科学研究科)The cube of Kleene algebra and the triangular prism of multirelationsWe define a triangular prism consisting of six classes of multirelations and define the cube consisting of eight classes of lazy Kleene algebras and show a mapping from the triangular prism to the cube. The mapping includes the result that the set of ordinary binary relations forms a Kleene algebra, the set of up-closed multirelations forms a lazy Kleene algebra, and the set of total up-closed finite multirelations forms a probabilistic Kleene algebra. The six classes of multirelations is defined by introducing types of multirelations.