Logic-ml

logic-ml@fos.kuis.kyoto-u.ac.jp

1792 discussions

CSセミナーin桐生
by Fujita Kenetsu 09 Sep '14

09 Sep '14

(* Apologies for any cross-postings. *) 皆様，群馬大学の藤田と申します．コンピュータ・サイエンスのセミナーのご案内です．どなたでも参加できますので，どうぞお気軽にお越し下さい．問い合わせ先：藤田憲悦 fujita(a)cs.gunma-u.ac.jp *********************************************************************** +++++ CS seminar in Kiryu: Programme +++++ URL: http://www.cs.gunma-u.ac.jp/~fujita/research/20140918Seminar.html Thursday, September 18, 2014 14:00--15:30 in the J3 lecture room (the building no. 6 of the map below), Kiryu campus, Gunma University Title: "Verification of programs using Frama-C and Why3" Speaker: Dr. Aleksy Schubert The University of Warsaw, Poland Abstract: Frama-C is a tool that makes it possible to do a variety of analyses for C programs annotated with C specification language called ACSL (The ANSI/ISO C Specification Language). One of the possible ways to use Frama-C is to generate verification conditions for appropriately defined Hoare logic that is in line with C programming language semantics. These verification conditions can subsequently be discharged by Why3 tool that makes it possible to manage the proving of necessary properties. During the talk I will present an overview of the tools and show a number of interesting examples to demonstrate how these tools work together to make possible verification of practical programs. ************************************************************************** Access to Kiryu campus, Gunma University: http://www.st.gunma-u.ac.jp/other/14.html Map of Kiryu campus: http://www.st.gunma-u.ac.jp/other/13.html For more information, please contact at: fujita(a)cs.gunma-u.ac.jp (Ken-etsu Fujita, Gunma University) -----

1 0

APLAS 2014: Call for Participation
by Jacques Garrigue 06 Sep '14

06 Sep '14

皆様、 APLASの参加募集案内をお送ります。 Jacques Garrigue ======================================================================= 12th Asian Symposium on Programming Languages and Systems (APLAS) November 17-19, 2014, Singapore http://loris-7.ddns.comp.nus.edu.sg/~aplas14 ======================================================================= C A L L F O R P A R T I C I P A T I O N C A L L F O R P O S T E R S APLAS aims to stimulate programming language research by providing a forum for the presentation of latest results and the exchange of ideas in programming languages and systems. APLAS is based in Asia, but is an international forum that serves the worldwide programming language community. APLAS is sponsored by the Asian Association for Foundation of Software (AAFS), founded by Asian researchers in cooperation with many researchers from Europe and the USA. Past APLAS symposiums were successfully held in Melbourne ('13), Kyoto ('12), Kenting ('11), Shanghai ('10), Seoul ('09), Bangalore ('08), Singapore ('07), Sydney ('06), Tsukuba ('05), Taipei ('04) and Beijing ('03) after three informal workshops. Proceedings of the past symposiums were published in Springer's LNCS. The symposium is devoted to foundational and practical issues in programming languages and systems. Invited Speakers ---------------- Zhenjiang Hu NII, Japan Dexter Kozen Cornell University, USA Julien Verlaguet Facebook, USA Program Committee ----------------- General chair Wei-Ngan Chin National University of Singapore, Singapore Program chair Jacques Garrigue Nagoya University, Japan Program committee Xiaojuan Cai Shanghai Jiao Tong University, China James Chapman Institute of Cybernetics, Estonia Cristian Gherghina Singapore University of Technology and Design Eric Goubault CEA LIST and Ecole Polytechnique, France Fei He Tsinghua University, China Gerwin Klein NICTA and UNSW, Australia Raghavan Komondoor Indian Institute of Science, Bangalore Paddy Krishnan Oracle, Australia Daan Leijen Microsoft Research, USA Yasuhiko Minamide University of Tsukuba, Japan Shin-Cheng Mu Academia Sinica, Taiwan Sungwoo Park Pohang University of Science and Technology, Korea Julian Rathke University of Southampton, UK Sukyoung Ryu KAIST, Korea Alexandra Silva Radboud University Nijmegen, Netherlands Martin Sulzmann Karlsruhe University of Applied Sciences, Germany Munehiro Takimoto Tokyo University of Science, Japan Jan Vitek Purdue University, USA Hongwei Xi Boston University, USA Venue ----- The conference will be held at the Kent Ridge Guild House of the National University of Singapore. Local information and registration are available at the following web site: http://loris-7.ddns.comp.nus.edu.sg/~aplas14 Call for Poster (Deadline 15th Sept 2014) http://loris-7.ddns.comp.nus.edu.sg/~aplas14/cfposters.html Poster Chair: Cristian Gherghina ============================= Monday, November 17th ============================= 08:30-09:00 Registration 09:00-10:00 ** Invited Talk: What is the Essence of Bidirectional Programming? Zhenjiang Hu (NII, Japan) 10:00-10:30 Coffee break 10:30-12:00 Session 1 Optimized Compilation of Multiset Rewriting with Comprehensions Edmund Soon Lee Lam, Iliano Cervesato (CMU, Qatar) Logic Programming and Logarithmic Space Clément Aubert, Marc Bagnol, Paolo Pistone (Institut de Mathématiques de Marseille, France),Thomas Seiller (Institut des Hautes Études Mathématiques,France) Automatic Memory Management Based on Program Transformation using Ownerships Tatsuya Sonobe, Kohei Suenaga, Atsushi Igarashi (Kyoto Univ., Japan) 12:00-13:30 Lunch and Posters 13:30-14:30 Session 2 The Essence of Ruby Katsuhiro Ueno, Yutaka Fukasawa (Tohoku University, Japan),Akimasa Morihata (Univ. of Tokyo, Japan), Atsushi Ohori (Tohoku Univ., Japan) Types for Flexible Objects Zachary Palmer, Scott Smith, Hari Menon, Alexander Rozenshteyn (The Johns Hopkins Univ., USA) 14:30-16:00 Posters and Tea 16:00-17:30 Session 3 A Translation of Intersection and Union Types for the lambda-mu Calculus Kentaro Kikuchi (RIEC, Tohoku Univ., Japan), Takafumi Sakurai (Chiba Univ., Japan) A Formalized Proof of Strong Normalization for Guarded Recursive Types Andreas Abel (Gothenburg Univ., Sweden), Andrea Vezzosi (Chalmers Univ. of Technology, Sweden) Functional Pearl: Nearest Shelters in Manhattan Shin-Cheng Mu (Academia Sinica, Taiwan), Ting-Wei Chen (National Taiwan Univ., Taiwan) ============================= Tuesday, November 18th ============================= 08:30-09:30 ** Invited Talk: Incremental Adoption of Static-Typing Julien Verlaguet (Facebook, USA) 09:30-10:00 Session 4 SUPPL: A flexible language for policies Robert Dockins and Andrew Tolmach (Portland State Univ., USA) 10:00-10:30 Coffee break 10:30-12:00 Session 5 A Method for Scalable and Precise Bug Finding Using Program Analysis and Model Checking Manuel Valdiviezo, Cristina Cifuentes and Padmanabhan Krishnan (Oracle Labs Brisbane, Australia) Model-checking for Android Malware Detection Fu Song (East China Normal Univ., China), Tayssir Touili (LIAFA, CNRS & Univ. Paris Diderot, France) Necessary and Sufficient Preconditions via Eager Abstraction Mohamed Nassim Seghir (Univ. of Edinburgh, UK), Peter Schrammel (Univ. of Oxford, UK) 12:00-13:30 Lunch 13:30-15:00 Session 6 Resource Protection using Atomics: Patterns and Verifications Afshin Amighi, Stefan Blom, Marieke Huisman (Univ. of Twente, Netherlands) Resource Analysis of Complex Programs with Cost Equations Antonio Flores Montoya, Reiner Hähnle (Technische Univ. Darmstadt, Germany) Simple and Efficient Algorithms for Octagons Aziem Chawdhary, Edward Robbins, Andy King (Univ. of Kent, UK) 15:00-15:30 Coffee break 15:30-17:00 Session 7 Compositional Entailment Checking for a Fragment of Separation Logic Constantin Enea (LIAFA, CNRS & Univ. of Paris, France), Ondrej Lengal (Brno Univ. of Technology, Czech Republic),Mihaela Sighireanu (LIAFA, CNRS & Univ. of Paris, France), Tomas Vojnar (Brno Univ. of Technology, Czech Republic) Automatic Constrained Rewriting Induction Towards Verifying Procedural Programs Cynthia Kop (Univ. of Innsbruck, Austria), Naoki Nishida (Nagoya Univ., Japan) A ZDD-based Efficient Higher-order Model Checking Algorithm Taku Terao, Naoki Kobayashi (Univ. of Tokyo, Japan) 18:00- APLAS Banquet ============================ Wednesday, November 19th ============================ 08:30-10:00 Session 8 Inferring Grammatical Summaries of String Values Se-Won Kim, Wooyoung Chin, Jimin Park, Jeongmin Kim, Sukyoung Ryu (KAIST, Korea) Syntax-Directed Divide-and-Conquer Data-Flow Analysis Shigeyuki Sato (The Univ. of Electro-Communications, Japan), Akimasa Morihata (Univ. of Tokyo, Japan) Address Chain: Profiling Java Objects without Overhead in Java Heaps Xiaohua Shi, Junru Xie, Hengyang Yu (Beihang Univ., China) 10:00-10:30 Coffee break 10:30-12:00 Session 9 Call-by-Value in a Basic Logic for Interaction Ulrich Schäpp (Ludwig-Maximilians-Univ. München, Germany) A precise and abstract memory model for C using symbolic values Frédéric Besson (Inria, France), Sandrine Blazy, Pierre Wilke (IRISA, France) Hereditary history-preserving bisimilarity: logics and automata Paolo Baldan, Silvia Crafa (Universita' di Padova, Italy) 12:00-13:00 Lunch 13:00-14:00 ** Invited Talk: NetKAT: A formal system for the verification of networks Dexter Kozen (Cornell Univ., USA)

1 0

第３１回量子情報技術研究会（QIT31）のご案内
by NISHIMURA Harumichi 05 Sep '14

05 Sep '14

logic-mlの皆様，第31回量子情報技術研究会のご案内を代理投稿させていただきます．よろしくお願いいたします．名古屋大学大学院情報科学研究科西村治道 ---------------------------------------------------------- 第31回量子情報技術研究会(QIT31) 研究会の内容情報科学と量子力学を融合させた新しい分野，量子情報科学に関する研究会です．情報を担う物理系の量子力学的側面を積極的に活かした新しい情報処理原理の研究とそこから開かれる新しい学問体系の構築および新しい情報技術パラダイムの創生を目指して，情報科学，物理学，光エレクトロニクスを含む理学，工学，数理科学に携わる研究者間に自由な討論の場を提供し，この研究分野の発展を図ることを目的としています．第31回研究会を下記のように開催いたします．現在この分野で活躍する研究者は勿論，自分の研究資産が何らかの形で使えそうだと予感している研究者・技術者など，広く関連する分野の研究者・技術者からの発表を募集致します．聴講のみの参加も歓迎致しますので，奮ってお申し込みください．日時: 2014年11月17日(月)～18日(火) 会場: 東北大学さくらホール (〒980-8577 仙台市青葉区片平２－１－１東北大学片平キャンパス内) 発表募集分野 (申し込み状況によっては査読の可能性あり) 量子情報，量子計算，量子暗号など広く量子情報技術に関わる理論的研究，実験的研究，計算機科学的研究，数学的研究，および，その他関連分野．定員: 200名参加費: 事前振込み一般4,000円，学生1,000円 (当日会場払いは一般5,000円，学生2,000円) (懇親会は別途) 研究会参加申込要領参加申込は下記 Web にて受付けます： http://staff.aist.go.jp/s-kawabata/qit/ 講演 (口頭，ポスター) の申込，予稿集原稿 PDF の提出は，電子情報通信学会の Web システムを使用する予定．【口頭講演申込締切】 2014年9月19日(金) 【ポスター講演申込締切】 2014年10月3日(金) 【予稿原稿提出締切】 2014年10月3日(金) 【参加申込締切】 2014年10月24日(金) 【問合せ先】枝松圭一 (東北大学電気通信研究所) 三森康義 (東北大学電気通信研究所) 吉田真人 (東北大学電気通信研究所) Email: qit31(a)quantum.riec.tohoku.ac.jp 主催: 量子情報技術時限研究専門委員会 (委員長: 枝松圭一 (東北大学)) 共催: 応用物理学会量子エレクトロニクス研究会東北大学電気通信研究所 ----------------------------------------------------------

1 0

[CFP] 情報処理学会第101回プログラミング研究発表会発表募集
by Rei Odaira 01 Sep '14

01 Sep '14

Logic-mlの皆さま、 IBMの大平です。締切約10日前ということで再度送らせて頂きます。＊＊＊＊複数受け取られた方はご容赦ください＊＊＊＊情報処理学会第101回プログラミング研究発表会発表募集今回は第101回記念ということでプログラミング研究会の初期に活躍された方を招いてのパネルセッションも催す予定です．プログラミング研究会(PRO)は，・プログラミング言語の設計，処理系の実装・プログラミングの理論，基本概念・プログラミング環境，支援システム・プログラミング方法論，パラダイム・これらを応用したシステムの開発事例・その他，プログラミングに関する面白い話題を対象とした研究発表の場で，1998年度から毎年3?4回のペースで論文誌を発行しています．PRO論文誌は研究会と密接にリンクしており，研究会で発表されたもののうちあらかじめ論文投稿を希望し，論文原稿を提出されているものが査読の対象となっています (論文誌投稿を希望しない発表も歓迎します)．おおむね研究会から3週間で論文の採否が決定されるという迅速さも大きな特徴です． 2014年11月の研究会も多くの発表ならびに論文投稿をお待ちしております．参加費は無料です．申込締切は9月12日金曜日(投稿締切は10月10日金曜日)ですので，よろしくご検討ください．なお，多数の発表申込みがある場合には，発表をお断りすることがございますので，お早めにお申し込みください．発表申込時で必要なのはタイトルと概要などとなっております．また，今回も和文として投稿された論文の英語化を支援する試みを実施します．和文原稿にて採録を判断し，(著者が希望する場合は) 採録決定後に英語化していただいてから掲載致します．この英語化に関する詳細については， http://www.ipsj.or.jp/sig/pro/english-paper-encouragement.html をご覧ください．第101回プログラミング研究会(PRO-2014-3)発表募集日程: 2014年11月10日(月)・11日(火) 会場: 東京大学創造情報学専攻 I-REF 棟 6階 Hilobby 東京都文京区弥生 1-1-1 　　交通案内: http://www.ci.i.u-tokyo.ac.jp/site/?access-j 発表申込締切:　　　　　　 2014年9月12日(金) 投稿論文原稿提出締切: 2014年10月10日(金) 申込先: 大平怜（日本アイ・ビー・エム東京基礎研究所） E-mail: odaira [at] jp.ibm.com 案内ページ: https://staff.aist.go.jp/reynald.affeldt/pro101/ ・申込みに当たっての注意はプログラミング研究会のページ http://www.ipsj.or.jp/sig/pro/を参照してください．・著者のための手引き: http://www.ipsj.or.jp/sig/pro/trans-author.html ・申込みの際には整理のために，Subject欄に以下をご指定頂けると助かります．　「PRO2014-3発表申込み」(カッコ不要) ・できるだけE-mailでお願いします．・申込み後3日以内に返信がない場合はご連絡下さい．大平　怜 (Rei Odaira), Ph.D. IBM Research - Tokyo Phone: +81-3-5144-2847

1 0

第49回 MLG 数理論理学研究集会のご案内
by Katsuhiko Sano 29 Aug '14

29 Aug '14

第49回 MLG 数理論理学研究集会のご案内 (重複してお受け取りの際はどうぞご容赦ください。) 北陸先端科学技術大学院大学の佐野勝彦と申します。少し先にはなりますが、2014年度MLG数理論理学研究集会（第49回）を下記の要領で開催いたします。多くの方のご講演・ご参加をお待ちしております。 ========================================= 第49回 MLG 数理論理学研究集会開催要領 ========================================= - 期間: 2014 年 12 月 5 日(金) 〜 12 月 7 日(日) - 場所: 山中温泉河鹿荘ロイヤルホテル（JR加賀温泉駅から車で約20分，加賀温泉駅から送迎あり） -- 〒922-0126 石川県加賀市山中温泉河鹿町ホ100 -- URL : http://www.daiwaresort.jp/kajikasou/ - 講演・宿泊申込締め切り: 2014 年 11 月 21 日（木） - 申し込みはこちらから --> http://goo.gl/RfZ5SE - ホームページ: https://sites.google.com/site/mlg2014kaga/ - 連絡先E-mail: mlg.logic.japan [at] gmail.com ============ 参加募集 ============ - 講演時間は原則40分を予定しています。 - 12月6日（土）の夜に懇親会を行います。 - 全日程参加の場合，参加費（宿泊代・食事代・会場代）は25000円前後になる予定です。 - ご講演をなさらなくても参加いただけます。山中温泉河鹿荘ロイヤルホテルで宿泊および食事をなさらない場合にも参加費（会場代）3000円をいただきます。 - 参加・講演申し込みは、http://goo.gl/RfZ5SE の registration form からお願い致します。世話人: 佐野勝彦〒923-1292 石川県能美市旭台1-1 北陸先端科学技術大学院大学情報科学研究科 MLG2014 に関するメールは，mlg.logic.japan [at] gmail.com まで。

1 0

September 1st - research talks by Yves Bertot, Pierre Casteran and Assia Mahboubi at University of Tokyo
by Jacques Garrigue 28 Aug '14

28 Aug '14

名古屋大学のGarrigueです。来る月曜日（9月1日）Coqの専門家三人による講演会を東京大学本郷キャンパスで開きます。皆様をお待ちしています。 On Monday, September 1st, three of the lecturers of the Shonan School on Coq will give talks at the University of Tokyo (Hongo Campus). We are waiting for you. David Nowak and Jacques Garrigue —— Date: September 1st, 2014 (Monday) Time: 14:00 - 16:30 Place: room 007, Faculty of Science Bldg. 7, Hongo Campus, The University of Tokyo URL: http://jfli.cnrs.fr/index.php/special-jfli-seminar-coq On the occasion of the NII Shonan School on Coq, JFLI organizes a special seminar on formal proofs in Coq with talks by three of the school's lecturers: Yves Bertot and Pierre Castéran (two of the 2013 ACM Software System Award laureates) will present some of their recent work. And Assia Mahboubi will present the formalization in Coq of the Feit-Thompson theorem (a.k.a. odd order theorem) achieved in 2012 under the direction of Georges Gonthier. 14:00 - 14:45: Yves Bertot PI, Arithmetic geometric means, and formal verification in Coq using Coquelicot In an experiment spanning over several months, we formally verified an abstract model of an algorithm to compute PI to a large number of digits using arithmetic geometric means. The proof that we used relies on a few non elementary aspects, like reasoning about improper integrals or deriving under the integral sign, and revolved around manipulating real numbers. This is why we call this an abstract model. Then we used the recent extension of Coq with native compilation to test the algorithm on a concrete setting, using large integers. As a result we are able to compute in the order of a million of decimals of PI within the theorem prover. We also proved the correctness of this implementation. This involves bounding the cumulated errors brought by multiplication, division, and square-root during fixed-point multiplications. This work benefits from the overall quality of the Coq system and the following recent contributions: the coquelicot library by Boldo & al., the psatzl tactic by F. Besson, and native compilation by M. Dénès. 14:45 - 15:30: Pierre Castéran Formal Proofs of Local Computation Systems Local Computations (LC) are an abstract model for distributed algorithms based on message passing. Each processor can only interact with its neighbours. The current configuration of a static network is represented as a labelling of the vertices and edges of a graph. This model allows us to study the importance of such hypotheses on the network's behaviour such as synchrony, anonymity, initial knowledge of the processors. Algorithms are splitted into several classes, according to the precise way in which every processor interacts with its neighbours. LoCo is a formalization of LC in the Coq proof assistant. This library allows us to simulate algorithms, to prove their correctness, and also to prove more abstract results: • Impossibility results, i.e., proving that some task is not realisable within a given subclass of LC; • Certified transformations, that are functions that map one or several proved algorithms into a new proved algorithm; • Analysis of some simple random distributed algorithms. The talk will show how Coq's rich type system and computation rules allowed us to build this library. Perspective of future work will also be discussed. 15:30 - 15:45: break 15:45 - 16:30: Assia Mahboubi Computer-checked mathematics: a formal proof of the Odd Order theorem The Odd Order Theorem is a landmark result in finite group theory, famous for its crucial role in the classification of finite simple groups, for the novel methods introduced by its original proof but also for the striking contrast between the simplicity of its statement and the unusual length and complexity of its proof. This talk presents the six-year collaborative work that led to a complete formalization of this theorem, using the Coq proof assistant. The resulting collection of libraries of formalized mathematics covers a wide variety of topics as this proof relies on a sophisticated combination of different flavours of mathematics. These libraries and the underlying methodology can be reused for a wider spectrum of applications. This is a joint work with the Mathematical Components group at the Inria Microsoft Joint Centre.

1 0

第5回松山TGSAセミナーのお知らせ
by Hiroshi Fujita 26 Aug '14

26 Aug '14

LOGICメーリングリストの皆さま、愛媛大学の藤田です。このほど下記のセミナーを愛媛大学理学部において開催することとなりましたのでお知らせいたします。 ============================================== 第5回松山TGSAセミナー ============================================== 日時: 2014年9月8日(月) 16時30分〜17時30分会場: 愛媛大学理学部 2号館201号室 (数学科大演習室) 講演者: 南裕明さん（神戸大学）演題: Mathias-Prikry forcing and dominating reals ============================================== Abstract: For a countable set X, we call $\mathcal{I}$ an ideal on X if $\mathcal{I}$ is a family of subsets of X closed under the taking subsets and unions. We assume all ideals on X contains the family of finite subsets of X. The Mathias-Prikry forcing associated with an ideal $\mathcal{I}$ on a countable subset X, denoted by $\mathbb{M}_{\mathcal{I}}$, consist of pairs (s,A) such that s is a finite subsets of X, A in $\mathcal{I}$ and $s\cap A=\emptyset$. The ordering is given by $(s,A)\leq (t,B)$ if t is a subset of s and B is a subset of A and $(s\setminus t)\cap B=\emptyset$. The Mathias-Prikry forcing adds a new subset of X which diagonalize ideal $\mathcal{I}$, that is, $\mathbb{M}_{\mathcal{I}}$ adds a new subset $\dot{A}$ of X such that $X\cap I$ is finite for every I in $\mathcal{I}$. So Mathias-Prikry forcing plays significant role when we investigate ultrafilter, ideal or mad family. Some additional nice properties of the Mathias-Prikry forcing depends on $\mathcal{I}$. For example, $\mathcal{U}$ is a Ramsey ultrafilter if and only if $\mathbb{M}_{\mathcal{U}^{*}}$ does not add Cohen real. The speaker and Michael Hru\v{s}\'{a}k give a characterization of ideals $\mathcal{I}$ such that $\mathbb{M}_{\mathcal{I}}$ adds no dominating real. We say a forcing notion $\mathbb{P}$ adds dominating reals if $\mathbb{P}$ adds a new function $\dot{g}$ from $\omega$ to $\omega$ such that for $f\in\omega^{\omega}\cap V$, $f(n)<\dot{g}(n)$ for all but finitely many $n\in\omega$. We show that $\mathbb{M}_{\mathcal{I}^{*}}$ adds dominating reals if and only if $\mathcal{I}^{<\omega}$ is $P^{+}$-ideal. Recently, David Chodounsk\'{y}, and Du\v{s}an Repov\v{s} and Lyubomyr Zdomskyy give another characterization of ideal $\mathcal{I}$ with covering property such that $\mathbb{M}_{\mathcal{I}}$ adds no dominating real. We will talk about recent development of these result and application. ============================================== 松山TGSAセミナー（Matsuyama Seminar on Topology, Geometry, Set Theory and their Applications)は、位相空間論・幾何学・集合論およびその関連分野を広く扱うセミナーで、愛媛大学のスタッフが中心となって定期的に開催しています。今後の予定についてはWebサイト <http://www.math.sci.ehime-u.ac.jp/MTGSA.html> をご覧ください。 -- 藤田博司 <fujita.hiroshi.mh(a)ehime-u.ac.jp> 愛媛大学理学部／大学院理工学研究科数理物質科学専攻

1 0

The Kyoto Summer School in Logic, Language and Information (KSSLLI)のお知らせ
by Shunsuke Yatabe 25 Aug '14

25 Aug '14

重複して受け取られたかたはご容赦ください。下記のとおりに哲学的論理学に関するサマースクールを開催いたします。どうぞふるってご参加ください。矢田部俊介＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊記日時：2014年8月30日（土）～31日（日）場所：京都大学文学部第７講義室（下地図のNo.8） http://www.kyoto-u.ac.jp/en/access/campus/main.htm 開催趣旨と内容：近年、哲学や人文学と論理学や形式的言語学、情報科学との間の垣根は低くなり、哲学や人文学の研究にも形式的な論理学等の手法の知識が必要となるケースも増えてきた。欧州や北米では、人文学・哲学の研究者とこれら三分野の研究者が国を超えて共に集い、それら手法を学び、意見交換を通じて共同研究の芽を用意するサマースクール（ESSLI、NASSLLI等）が毎年行われ、多くの成果を上げている。しかし、アジア太平洋地域では、研究者は自身の専門分野に籠もり、欧米のような共同の試みはあまり行われてこなかった。本サマースクールは、アジア太平洋地域の、論理学が専門ではない哲学の大学院生が多数参加する国際会議CCPEAのサテライトとして開催され、院生への最先端の論理学的手法等の紹介を通して、異分野同志の協業をスタートさせることを目指す。今回は、8月30日にブリストル大学のLeon Horsten教授に、公理的真理理論の論理学的、および哲学的意義（特に真理に関するデフレ主義との関連で）についてご講演頂く。 8月31日は、矢田部・秋吉が非古典論理上の素朴集合論や形式算術の順序数解析などの話題について、入門的な説明と最新の結果説明を同時に行う。また、夕方は、お茶の水女子大学の田中と叢が、言語学における論理学的・計算機科学的手法の最新の応用例について、発展的な解説を行う。参加費は無料、事前登録は不要です。講演は英語で行われます。問い合わせ先：CAPE(a)bun.kyoto-u.ac.jp ***************************************** The Kyoto Summer School in Logic, Language and Information (KSSLLI) The Kyoto Summer School in Logic, Language and Information (KSSLLI) is planned to be an annual event under the support of the Center for Applied Philosophy and Ethics, graduate school of letters, Kyoto University (CAPE) and brings together logicians, linguists, computer scientists, and philosophers to study language, logic, and information, and their interconnections. This is a satellite workshop of the 2nd conference on Contemporary Philosophy in East Asia (CCPEA). There will be about several courses at introductory and advanced invited lectures and a student session to foster interdisciplinary discussion among philosophers, logicians and computer scientists. Venue: The 7th lecture room, faculty of letters main building (the bulding no.8 of the map below), Kyoto University http://www.kyoto-u.ac.jp/en/access/campus/main.htm Conference url: http://www.cape.bun.kyoto-u.ac.jp/capes/ws/ Fee: free Submission: no submission is needed. Schedule: 30, August（Saturday） Mini lecture course on Axiomatic Truth Theories : Leon Horsten (University of Bristol) This is one day tutorial course on axiomatic truth theory (as FS) and deflationism for wide range audience. 10:00-12:00 Session 1 "Axiomatic approaches to truth" 12:00-14:00 Lunch 14:00-16:00 Session 2 "Implications for deflationism about truth" 31, August（Sunday） Short lectures and introductions of advanced results This session provides introductions to new results in philosophical logics 10:00-11:30 Session 1 Naive set theories on non-classical logics: Shunsuke Yatabe (Kyoto University) 11:30-13:30 Lunch 13:30-15:00 Session 2 An Introduction to Proof Theory of First-Order Arithmetic: Ryota Akiyoshi (JSPS) Talks on formal linguistics This session provides introductions to new results in formal linguistics 15:00-16:00 "A Proof-Theoretic Approach to Generalized Quantifiers in Dependent Type Semantics" Ribeka Tanaka (Ochanomizu University) 16:00-17:00 "Analysis and Implementation of Focus and Inverse Scope by Delimited Continuations" Youyou Cong (Ochanomizu University) Abstracts: Session 1 Naive set theories on non-classical logics: Shunsuke Yatabe (Kyoto University) It is well-known that naive set theories within many non-classical logics do not imply a contradiction. And, in these set theories, there are very different from classical set theories with respect to the concept of infinity because these theories are highly circular. In this lecture, we introduce these set theories and such difference. Session 2 An Introduction to Proof Theory of First-Order Arithmetic: Ryota Akiyoshi (JSPS) Gentzen proved the consistency of Peano arithmetic on 1936 after Goedel’s incompleteness theorems. Moreover, he showed that the epsilon_0 is the least ordinal for proving it. His fundamental work was the beginning of the modern proof theory called “ordinal analyais”. In 1951, Schuette used an infinitary inference called “the omega-rule” for obtaining a more perspicuous proof of Gentzen’s result. This approach is not only technically simpler and elegant, but historically (or philosophically) interesting for the following reason; Brouwer already suggested the possibility of using of infinitary inference for Hilbertian proof theory. In this talk, we explain the basic results of infinitary proof theory via the omega-rule for Peano arithmetic. Additionally, we discuss the relationship between finitary proof theory (Gentzen) and infinitary proof theory (Schuette). Talks on formal linguistics (1) A Proof-Theoretic Approach to Generalized Quantifiers in Dependent Type Semantics: Ribeka Tanaka (Ochanomizu University) The main aim of this study is to give semantic representations of generalized quanti fiers (GQs) in the framework of dependent type semantics (DTS), a proof-theoretic semantics for natural language. Quantifier "most" is known as a crucial example of GQs. In this talk, we introduce the framework of DTS, propose a definition of "most" that accounts for dynamic linguistic phenomena, and extend the definition to numerical quantifiers. We also show that the definitions satisfy logical properties of GQs, conservativity and monotonicity. (2) Analysis and Implementation of Focus and Inverse Scope by Delimited Continuations: Youyou Sou (Ochanomizu University) Focus and inverse scope are known as phenomena that require the context surrounding a particular lexical item for the semantic representation of the whole sentence. The context of a given lexical item in a natural language sentence can be regarded as its continuation. Continuation is a notion in programming languages that represents the rest of the computation. In this talk, we will present an analysis of focus and inverse scope by means of the control operators shift/reset (Danvy and Filinski 1990). We also discuss the interaction between these phenomena. For more information, please contact at CAPE(a)bun.kyoto-u.ac.jp

1 0

セミナー案内
by KASHIMA Ryo 25 Aug '14

25 Aug '14

数理論理学セミナーのお知らせ日時：8月28日(木) 16:00 から場所：東京工業大学大岡山西８号館Ｗ棟10階 W1008 話者：横山啓太（JAIST）題目：ヒルベルトは悪夢を見るか概要：ゲーデルの不完全性定理によれば、十分な自然数論を含む無矛盾かつ再帰的な公理系は必ず証明できない文を持つ。それでは、二つの（ゲーデルの不完全性定理の条件を満たすような）公理系T,T'を用意して次を成り立たせることは可能だろうか？全ての文 A に対して T が A で証明できるかまたは T が A で証明できないことが T' で証明できる。 6月にシンガポールで行われた研究集会において、Mingzhong Cai 氏が Hilbert's nightmare の名で上を一般化した問題を提示した。ここではその問題に対する Beklemishev/Vissar の答えを紹介し、さらなる一般化についても考える。 ------ 本セミナーは定期的に東工大で開催しているものです。初めて参加を希望される方はご一報ください。 ----- 鹿島亮東京工業大学大学院情報理工学研究科数理・計算科学専攻 kashima(a)is.titech.ac.jp

1 0

日本ソフトウェア科学会第31回大会参加募集案内
by Atsushi Igarashi 22 Aug '14

22 Aug '14

京都大学の五十嵐です．　9月7日(日)～10日(水)に名古屋大学東山キャンパスにて開催されます日本ソフトウェア科学会第31回大会の暫定プログラムを公開し，参加申し込みの受付も開始いたしましたのでご案内いたします．様々な企画と研究発表があり，特に9/7(日)に行われる FTD 2014 (Future Technology Design) は参加費無料ですので，ぜひ参加をご検討ください． -- 五十嵐淳 (IGARASHI Atsushi) E-mail: igarashi(a)kuis.kyoto-u.ac.jp url: http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/ ------------------------------------------------------------------------- 日本ソフトウェア科学会第 31 回大会開催案内・参加募集 ------------------------------------------------------------------------- 大会ホームページ： http://jssst2014.wordpress.com Twitter： @jssst2014 日時： 2014 年 9 月 7 日(日)～ 10 日(水) 会場：名古屋大学東山キャンパス IB電子情報館名古屋市営地下鉄名城線名古屋大学駅３番「西地区出口」１分参加申込ページ: http://jssst2014.wordpress.com/participation/ 本年も，2件の招待講演に加えて，著名な国際会議での発表論文を紹介していただくトップカンファレンス特別講演，未来につくるソフトウェアについて語る FTD，新たな知識を身に着けるためのチュートリアルなどの様々な企画が開催されます．また，一般セッション，研究会セッション，ソフトウェア論文セッション，デモ・ポスターセッションとしてソフトウェア科学全般に渡る多数の研究発表も行われますので，最新の研究成果についての議論と情報収集の場として，皆様の参加をお待ちしております． ------------------------------------------------------------------------- 大会ハイライト ------------------------------------------------------------------------- 招待講演 9/8(月) スマートステーションを実現する屋内空間情報サービス河口信夫（名古屋大学） 9/9(火) プログラム検証とインバリアント生成寺内多智弘（北陸先端科学技術大学院大学）トップカンファレンス特別講演 9/8(月)～9/10(水) ACM ICFP, ACM POPL, USENIX ATC, AAAI-14, AAMAS 2014 など 2013年から 2014年のトップカンファレンスで発表された論文について紹介していただきます．各講演はそれぞれ研究発表セッションにて実施されます． FTD 2014 (Future Technology Design) 9/7(日) ～未来をつくる素晴らしいソフトウェアのアイデアを世界に～「小学生」，「笑顔」，「命」，そして「飛行ロボット」，さまざまな分野でソフトウェアに関する素晴らしいアイデアをもっている７組の講演者たちが登場予定です．この講演者たちの記憶に残る１０分間のプレゼンを身近で経験してみませんか？ http://jssst2014.wordpress.com/events/ftd/ チュートリアル 9/7(日) (1) 定理証明支援系Coq入門講師：アフェルトレナルド（産業技術総合研究所） http://jssst2014.wordpress.com/events/coq-tutorial/ (2) ソフトウェア品質向上活動におけるプロダクトレビューの役割と効果講師：森崎修司（名古屋大学） http://jssst2014.wordpress.com/events/product-review-tutorial/ 併設企画・PPLサマースクール2014 9/7(日) 高性能計算のプログラミングの最前線講師：遠藤敏夫（東京工業大学） http://ppl.jssst.or.jp/index.php?ss2014 ------------------------------------------------------------------------- 参加申し込み方法 ------------------------------------------------------------------------- 参加申し込みページ http://jssst2014.wordpress.com/participation/ をご参照のうえ，お申し込みください．参加費については，9月4日（木）までに銀行振込にてお支払い下さるようにお願いいたします． ------------------------------------------------------------------------- プログラム（HTML版 http://jssst2014.wordpress.com/program/ ） ------------------------------------------------------------------------- [招待講演] (1) スマートステーションを実現する屋内空間情報サービス河口信夫（名古屋大学） 9月8日(月) 13:30-14:30 名古屋大学東山キャンパス IB電子情報館大講義室講演概要：屋外での位置情報サービスは広く普及しているが、屋内空間での位置情報サービスには、まだまだ発展の余地がある。本講演では、駅や地下街などの公共空間を対象として屋内空間のスマート化を目指す「スマートステーションなごや」プロジェクトを紹介する。 (2) プログラム検証とインバリアント生成寺内多智弘（北陸先端科学技術大学院大学） 9月9日(火) 14:00-15:00 名古屋大学東山キャンパス IB電子情報館大講義室講演概要： CEGAR によるソフトウェアモデル検査など多くの近年のプログラム検証において共通して使われる技術の一つが、有限の深さまで展開されたプログラムスライスを解析し（帰納的）インバリアント候補を推論する、というプロセスである。本講演では、この技術について基本的な解説を行い、またいくつかの課題についても述べる。特に、近年主流となりつつある「ホーン節制約解消」による手法に焦点を置き解説を行う。 [トップカンファレンス特別講演] 2013年から2014年のトップカンファレンスで発表された論文について紹介していただきます．各講演はそれぞれ研究発表セッションにて実施されます． (1) A Short Cut to Parallelization Theorems ○Akimasa Morihata （The University of Tokyo） (ACM ICFP 2013にて発表) 発表セッション：PPL (1) (2) Structural Recursion for Querying Ordered Graphs ○Soichiro Hidaka （National Institute of Informatics） Kazuyuki Asada （The University of Tokyo） Zhenjiang Hu （National Institute of Informatics） Hiroyuki Kato （National Institute of Informatics） Keisuke Nakano （University of Electro-Communications） (ACM ICFP 2013にて発表) 発表セッション：PPL (3) (3) Parametric Effect Monads and Semantics of Effect Systems ○Shin-ya Katsumata (Kyoto Univeristy) (ACM POPL 2014にて発表) 発表セッション：PPL (4) (4) GPUvm: Why Not Virtualizing GPUs at the Hypervisor? Yusuke Suzuki （Keio University） Shinpei Kato （Nagoya University） Hiroshi Yamada （Tokyo University of Agriculture and Technology） ○Kenji Kono （Keio University） (USENIX ATC ’14にて発表) 発表セッション：一般 (5) (5) SML# in Industry: A Practical ERP System Development ○Atsushi Ohori （Tohoku University） Katsuhiro Ueno （Tohoku University） Kazunori Hoshi （NEC Solution Innovators, Ltd.） Shinji Nozaki （NEC Solution Innovators, Ltd.） Takashi Sato （NEC Solution Innovators, Ltd.） Tasuku Makabe （NEC Solution Innovators, Ltd.） Yuki Ito （NEC Solution Innovators, Ltd.） (ACM ICFP 2014にて発表) 発表セッション：PPL (6) (6) Two Case Studies for Trading Multiple Indivisible Goods with Indifferences Akihisa Sonoda （Kyushu University） Etsushi Fujita （Kyushu University） ○Taiki Todo （Kyushu University） Makoto Yokoo （Kyushu University） (AAAI-14にて発表) 発表セッション：一般 (6) (7) Intelligence Arms Race: Delayed Reward Increases Complexity of Agent Strategies ○Hirotaka Osawa （University of Tsukuba） (AAMAS 2014にて発表) 発表セッション：一般 (6) [企画セッション] FTD2014 (Future Technology Design) ～未来をつくる素晴らしいソフトウェアのアイデアを世界に～ http://jssst2014.wordpress.com/events/ftd/ 9月7日(日) 13:20-17:00 名古屋大学東山キャンパス IB電子情報館 IB014 日本ソフトウェア科学会は、昨年創立３０周年を迎え、本学会で議論され生み出されてきたアイデアや、日本で生まれた広める価値のある素晴らしいソフトウェアのアイデアを広げる大会特別企画として、FTD (Future Technology Design)を実施しました。FTD 2013では、すばらしいアイデアを持った8名の講演があり、大盛況のもと改めてソフトウェアの面白さを再確認することができました。そして、FTD 特別企画から１年、未来につくるソフトウェアのアイデアをもっと広めたいという思いを再認識し、2014年の第３１回大会でもFTDを継続することにしました。FTD 2014では、映像、そして講演の両面からさらにパワーアップします。映像面では、講演の映像配信のさきがけ的コミュニティであるWISSとコラボし、リアルタイム映像合成+配信にチャレンジします。そして、講演面では、素晴らしいソフトウェアを産み出す人財を発掘する未踏事業とコラボレーションします。名付けてFTD 2014 ≒ FTD x WISS x 未踏。どうぞご期待ください。 [チュートリアル] (1) 定理証明支援系Coq入門講師：アフェルトレナルド（産業技術総合研究所） http://jssst2014.wordpress.com/events/coq-tutorial/ 9月7日(日) 14:00-18:00 名古屋大学東山キャンパス IB電子情報館 IB015 数学とソフトウェア科学の両方の分野において，定理証明支援系への関心が高まっています．なかでも，フランス国立情報学自動制御研究所（INRIA）で開発が進められている定理証明支援系Coqは，ACM SIGPLAN Programming Languages Software 2013 AwardとACM Software System 2013 Awardの受賞を契機に，より多くの研究者や技術者の注目を集めていす． Coqは，四色定理の証明に代表される数学分野での貢献だけでなく，ソフトウェア開発への応用においても大きな役割を果たしてきました．本チュートリアルでは，産業技術総合研究所のアフェルトレナルド氏をお招きし，モダンなCoq入門の観点から，Coqの拡張であるSSReflectを使った証明の初歩を紹介していただきます．SSReflectはタクティクスの表現力が向上し，数学の膨大な証明が可能になっただけでなく，プログラムの検証でも伝統的なCoqに代わって使われるようになっています．定理証明支援系を使った証明に関心を持つ研究者や学生の方，ソフトウェアの形式検証に関心を持つ研究者や技術者の方など，多くの方々の参加をお待ちしております．（本チュートリアルは日本語で行います） (2) ソフトウェア品質向上活動におけるプロダクトレビューの役割と効果講師：森崎修司（名古屋大学） http://jssst2014.wordpress.com/events/product-review-tutorial/ 9月7日(日) 13:00-16:00 名古屋大学東山キャンパス IB 電子情報館 IB014 ソフトウェア品質向上活動はプログラムの完成前に実施できる活動(静的解析技法を用いた活動)とプログラムの完成後に実施できる活動(動的解析技法を用いた活動)に大別できます。本チュートリアルでは、両方の品質向上活動を概観し、静的解析技法としてプロダクトレビューを紹介します。プロダクトレビューの技法を紹介した上で、ソフトウェアテストをはじめとする動的解析技法との役割分担やバランスを考えるヒントを紹介します。 [併設企画] PPLサマースクール2014 高性能計算のプログラミングの最前線講師：遠藤敏夫（東京工業大学） http://ppl.jssst.or.jp/index.php?ss2014 9月7日 (日) 10:00-13:00 名古屋大学東山キャンパス IB電子情報館 IB015 コンピュータの性能を最大限に活かすソフトウェアを作成するためには記憶階層や並列プログラミングの知識が必須であるが、学ぶべき知識は近年膨大となっている。古典的なOpenMPやMPIに加え、CUDA, OpenCL, OpenACC, Intel offload API, SSE/AVX…などである。その増大の多くは計算機アーキテクチャの複雑化・異種混合化に起因している。マルチコアや、 GPU・Xeon Phiなどのアクセラレータのアーキテクチャの動向も踏まえて、高性能計算のためのプログラミングの道具を概説する。 [研究発表プログラム（暫定版）] ◎一般セッション (1)：形式手法 9月8日（月） 10:00-12:00 （IB011）座長：田辺良則（国立情報学研究所） [一般1-1] 形式言語CSP#によるSysMLステートマシン図の形式化 ○安藤崇央（九州大学大学院システム情報科学研究院）谷津弘一（九州大学大学院システム情報科学研究院）孔維強（九州大学大学院システム情報科学研究院）久住憲嗣（九州大学システムLSI研究センター）福田晃（九州大学大学院システム情報科学研究院） [一般1-2] スマホ・アプリの電力消費振る舞いと検査性質の表現 ○中島震（国立情報学研究所） [一般1-3] 協調的リアクティブシステムの合成手法 ○冨田尭（東京工業大学大学院情報理工学研究科）上野篤史（東京工業大学大学院情報理工学研究科）萩原茂樹（東京工業大学大学院情報理工学研究科）米崎直樹（東京工業大学大学院情報理工学研究科） [一般1-4] 情報制御システムにおける段階的検査法を用いたモジュラ検証 ○宮島卓巳（茨城大学）小飼敬（茨城工業高等専門学校）上田賀一（茨城大学）山形知行（株式会社　日立製作所）武澤隆之（株式会社　日立製作所） ◎rePiTセッション (1) 9月8日（月） 10:30-12:00 （IB013）座長：楠本真二（大阪大学） [rePiT1-1] 女性IT技術者の育成を目指して―enPiT女性部会WiTの活動を中心に― ○櫻井浩子（大阪大学）森本千佳子（東京工業大学）渡辺知恵美（筑波大学）木塚あゆみ（公立はこだて未来大学）永瀬美穂（産業技術大学院大学）中島明日香（NTTセキュアプラットフォーム研究所） [rePiT1-2] RDFとユーザプロファイルを用いたPBL向け情報推薦手法 ○藤原哲（公立はこだて未来大学大学院）大場みち子（公立はこだて未来大学）山口琢（公立はこだて未来大学）奥野拓（公立はこだて未来大学）伊藤恵（公立はこだて未来大学） [rePiT1-3] IoTを題材としたPBLの実施と分析細合晋太郎（九州大学大学院システム情報科学研究院システム情報科学府高度ICT 人材教育開発センター）石田繁巳（九州大学大学院システム情報科学研究院システム情報科学府高度ICT 人材教育開発センター）亀井靖高（九州大学大学院システム情報科学研究院システム情報科学府高度ICT 人材教育開発センター） ○大迫周平（九州大学大学院システム情報科学研究院システム情報科学府高度ICT 人材教育開発センター）井垣宏（大阪大学）鵜林尚靖（九州大学大学院システム情報科学研究院システム情報科学府高度ICT 人材教育開発センター）福田晃（九州大学大学院システム情報科学研究院システム情報科学府高度ICT 人材教育開発センター） ◎PPLセッション (1)：並列処理 9月8日（月） 10:00-12:00 （IB014） [PPL1-1]（特別講演）A Short Cut to Parallelization Theorems 　　○Akimasa Morihata （The University of Tokyo）　　(ACM ICFP 2013にて発表) [PPL1-2] 限定継続演算子の拡張およびそれを用いた並列向け領域特化言語群の実現 ○山口洋（東京大学）千葉滋（東京大学） [PPL1-3] Locality-Aware Parallel Iterative Tree Traversal ○Shigeyuki Sato（The University of Electro-Communications） [PPL1-4] 依存関係をもった並列タスクのための動的グループバリア同期とその効率的な実装 ○夏澄彦（東京大学）佐藤芳樹（東京大学）千葉滋（東京大学） ◎一般セッション (2)：プログラミング学習 9月8日（月） 14:45-16:15 （IB011）座長：脇田建（東京工業大学） [一般2-1] LablGtk2を用いたuniverse teach packの実装 ○上原千裕（お茶の水女子大学理学部情報科学科）浅井健一（お茶の水女子大学理学部情報科学科） [一般2-2] プログラミング作業過程の動画を用いたプログラミング学習の試み ○杉本識吏（公立はこだて未来大学）伊藤恵（公立はこだて未来大学） [一般2-3] Schemeによる3D図形の構成的制作 ○古川孝太郎（京都大学大学院）坂東宜昭（京都大学大学院）糸山克寿（京都大学大学院）吉井和佳（京都大学大学院）奥乃博（京都大学大学院） ◎rePiTセッション (2) 9月8日（月） 14:45-16:15 （IB013）座長：粂野文洋（日本工業大学） [rePiT2-1] OJLによる実践的組込みシステム教育 ○舘　伸幸（名古屋大学）山本雅基（名古屋大学）吉田則裕（名古屋大学）高嶋博之（名古屋大学）海上智昭（名古屋大学）安藤友樹（名古屋大学）松原　豊（名古屋大学）本田晋也（名古屋大学）高田広章（名古屋大学） [rePiT2-2] ハイブリッド人材育成のための基礎学習に関する一考察 ○野尻梢（慶應義塾大学）廣瀬雅治（慶應義塾大学）山内正人（慶應義塾大学）砂原秀樹（慶應義塾大学） [rePiT2-3] モダンなソフトウエア開発者育成のための技術教育 ○中鉢欣秀（産業技術大学院大学） ◎PPLセッション (2)：文脈指向プログラミングと制約プログラミング 9月8日（月） 14:45-16:15 （IB014） [PPL2-1] Visibility of Context-oriented Behavior and State in L ○Robert Hirschfeld（Hasso-Plattner-Institute, University of Potsdam） Hidehiko Masuhara（Tokyo Institute of Technology） Atsushi Igarashi（Kyoto University） Tim Felgentreff（Hasso-Plattner-Institute, University of Potsdam） [PPL2-2] アクターモデルに基づく並行文脈指向プログラミング機構の実装と評価 ○竹野創平（東京工業大学）渡部卓雄（東京工業大学） [PPL2-3] 制約解集合プログラミングシステムの設計方式に関する考察 ○宋剛秀（神戸大学情報基盤センター）則武治樹（神戸大学大学院システム情報学研究科）番原睦則（神戸大学情報基盤センター）田村直之（神戸大学情報基盤センター）井上克巳（国立情報学研究所） ◎一般セッション (3)：ユーザ支援 9月8日（月） 16:30-18:00 （IB011）座長：丸山勝久（立命館大学） [一般3-1] コード生成を用いたフレームワーク向けWebアプリケーション開発支援ツールの作成 ○京谷和明（公立はこだて未来大学）伊藤恵（公立はこだて未来大学） [一般3-2] 研究エピソードネットワークに基づくスライド検索 ○加藤雄大（名古屋工業大学大学院工学研究科情報工学専攻）白松俊（名古屋工業大学大学院情報工学専攻）大囿忠親（名古屋工業大学大学院情報工学専攻）新谷虎松（名古屋工業大学大学院情報工学専攻） [一般3-3] ドキュメントレビュー結果を利用したテスト項目作成システムの開発 ○加藤武文（公立はこだて未来大学）大場みち子（公立はこだて未来大学）藤原哲（公立はこだて未来大学） ◎rePiTセッション (3) 9月8日（月） 16:30-18:00 （IB013）座長：井垣宏（大阪大学） [rePiT3-1] ハッカソン形式の実践的IT教育の実施報告 ○坂本一憲（国立情報学研究所）田辺良則（国立情報学研究所） [rePiT3-2] 筑波大学大学院におけるIT実践力育成の施策と評価 ○山戸昭三（筑波大学大学院システム情報工学研究科コンピュータサイエンス専攻）北川博之（筑波大学大学院システム情報工学研究科コンピュータサイエンス専攻）田中二郎（筑波大学大学院システム情報工学研究科コンピュータサイエンス専攻） [rePiT3-3] enPiT SecCap: Comparison of Japanese Practical Security Education with one of the US ○Takao Okubo（Institute of Information Security） ◎PPLセッション (3)：グラフ処理 9月8日（月） 16:30-18:00 （IB014） [PPL3-1]（特別講演）Structural Recursion for Querying Ordered Graphs 　　○Soichiro Hidaka （National Institute of Informatics）　　Kazuyuki Asada （The University of Tokyo）　　Zhenjiang Hu （National Institute of Informatics）　　Hiroyuki Kato （National Institute of Informatics）　　Keisuke Nakano （University of Electro-Communications）　　(ACM ICFP 2013にて発表) [PPL3-2] Engineering Shortest Regular Category-Path Queries ○Le-Duc Tung（The Graduate University for Advanced Studies (SOKENDAI)） Kento Emoto（Kyushu Institute of Technology） Zhenjiang Hu（National Institute of Informatics） [PPL3-3] パターン定義によるマッチングを導入したグラフ書換え言語とその実装 ○奈良耕太（早稲田大学理工学研究科）上田和紀（早稲田大学理工学術院） ◎ソフトウェア論文セッション (1) 9月9日（火） 10:30-12:00 （IB011）座長：馬谷誠二（京都大学） [ソフト1-1] Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール ○宋剛秀（神戸大学情報基盤センター）番原睦則（神戸大学情報基盤センター）田村直之（神戸大学情報基盤センター） [ソフト1-2] Code2Xml：ソースコードと構文木の相互変換を実現するパーサコレクション ○坂本一憲（国立情報学研究所） [ソフト1-3] まねっこダンス：真似て覚えるプログラミング学習ツール ○坂本一憲（国立情報学研究所）高野孝一（株式会社オービック）本田澄（早稲田大学）音森一輝（早稲田大学）山崎頌平（早稲田大学）鷲崎弘宣（早稲田大学）深澤良彰（早稲田大学） ◎rePiTセッション (4) 9月9日（火） 10:30-12:00 （IB013）座長：吉岡信和（国立情報学研究所） [rePiT4-1] 過去のPBLの開発履歴を活用したPBL運用支援 ○伊藤恵（公立はこだて未来大学）木塚あゆみ（公立はこだて未来大学）奥野拓（公立はこだて未来大学）大場みち子（公立はこだて未来大学） [rePiT4-2] テキストマイニングによるPBL発表会評価アンケート傾向分析 ○大迫周平（九州大学）孔維強（九州大学）亀井靖高（九州大学）細合晋太郎（九州大学）石田繁巳（九州大学）鵜林尚靖（九州大学）福田晃（九州大学） [rePiT4-3] enPiTにおける教育効果測定の実践と評価 ○山本雅基（名古屋大学）小林隆志（東京工業大学）宮地充子（北陸先端科学技術大学院大学）奥野拓（公立はこだて未来大学）粂野文洋（日本工業大学）櫻井浩子（大阪大学）海上智昭（名古屋大学）春名修介（大阪大学）井上克郎（大阪大学） ◎PPLセッション (4)：型システム 9月9日（火） 10:00-12:00 （IB014） [PPL4-1]（特別講演）Parametric Effect Monads and Semantics of Effect Systems 　　○Shin-ya Katsumata (Kyoto Univeristy) 　　(ACM POPL 2014にて発表) [PPL4-2] 分割できながら等価：型レベル・エイリアス ○Jacques Garrigue（名古屋大学） [PPL4-3] 代数的データ構造を扱う関数型プログラムの検証法 ○岡本大輔（筑波大学）海野広志（筑波大学） [PPL4-4] コード生成のための自然演繹 ○須藤悠斗（筑波大学コンピュータサイエンス専攻） Oleg Kiselyov（筑波大学コンピュータサイエンス専攻）亀山幸義（筑波大学コンピュータサイエンス専攻） ◎ソフトウェア論文セッション (2) 9月9日（火） 15:15-16:45 （IB011）座長：小宮常康 (電気通信大学) [ソフト2-1] REMViewer:複数回実行されたJavaメソッドの実行経路可視化ツール ○松村俊徳（大阪大学大学院情報科学研究科）石尾　隆（大阪大学大学院情報科学研究科）鹿島　悠（大阪大学大学院情報科学研究科）井上　克郎（大阪大学大学院情報科学研究科） [ソフト2-2] シーケンス図を用いたモデル検査支援ツール ○後藤隼弐（フェリカネットワークス株式会社）吉岡信和（国立情報学研究所） [ソフト2-3] RepositoryProbe: リポジトリマイニングのためのデータセット作成支援ツール ○高澤亮平（早稲田大学）坂本一憲（国立情報学研究所）鷲崎弘宜（早稲田大学）深澤良彰（早稲田大学） ◎一般セッション (4)：データ構造とプログラミング 9月9日（火） 15:15-16:45 （IB013）座長：南出靖彦（筑波大学） [一般4-1] Towards A Trace-based Approach to Increasing the Comprehensibility and Predictability of Bidirectional Graph Transformations ○Soichiro Hidaka（National Institute of Informatics） Martin Billes（Augsburg University） Quang Minh Tran（Daimler Center for IT Innovations, Technical University of Berlin） [一般4-2] RePair流高階圧縮アルゴリズムの最適化 ○武田広太郎（東京大学大学院情報理工学系研究科）小林直樹（東京大学大学院情報理工学系研究科）松田一孝（東京大学大学院情報理工学系研究科） [一般4-3] SGL Hierarchical Bridging Model for Parallel Programming ○LI Chong（National Institute of Informatics / Université Paris-Est, France） HAINS Gaétan（Université Paris-Est, France / INSA Centre, France） ◎PPLセッション (5)：非決定性とスケジューリング 9月9日（火） 15:15-16:45 （IB014） [PPL5-1] 公平な並列実行のためのゲーム意味論 ○西村進（京都大学大学院理学研究科） [PPL5-2] Observational Equivalence Using Schedulers for Quantum Processes Kazuya Yasuda（University of Tokyo） Takahiro Kubota（University of Tokyo） ○Yoshihiko Kakutani（University of Tokyo） [PPL5-3] Prolog再考: 急がないで推測 ○Oleg Kiselyov（Tsukuba）亀山幸義（Tsukuba） ◎一般セッション (5)：システムソフトウェア実装 9月10日（水） 10:00-12:00 （IB011）座長：光来健一（九州工業大学） [一般5-1]（特別講演）GPUvm: Why Not Virtualizing GPUs at the Hypervisor? 　　Yusuke Suzuki （Keio University）　　Shinpei Kato （Nagoya University）　　Hiroshi Yamada （Tokyo University of Agriculture and Technology）　　○Kenji Kono （Keio University）　　(USENIX ATC '14にて発表) [一般5-2] 仮想マシンモニタによるマルウェアプロセスの実行抑止 ○本田惇（電気通信大学情報理工学研究科総合情報学専攻）高橋一志（電気通信大学情報理工学研究科総合情報学専攻）大山恵弘（電気通信大学情報理工学研究科総合情報学専攻） [一般5-3] Silhouettes: ディスプレイ間を移動可能な人物の実像を用いた情報通知システムの試作 ○丹羽佑輔（名古屋工業大学大学院情報工学専攻）白松俊（名古屋工業大学大学院情報工学専攻）大囿忠親（名古屋工業大学大学院情報工学専攻）新谷虎松（名古屋工業大学大学院情報工学専攻） [一般5-4] 既存プレゼンテーション支援システムのWeb連携に基づく双方向プレゼンテーションの実現 ○井上良太（名古屋工業大学）丹羽佑輔（名古屋工業大学）白松俊（名古屋工業大学）大囿忠親（名古屋工業大学）新谷虎松（名古屋工業大学） ◎FOSEセッション 9月10日（水） 10:30-12:00 （IB013）座長：杉山安洋（日本大学） [FOSE-1] 過去のPBLの情報を用いた工数見積り支援ツールの開発 ○齋藤尊（公立はこだて未来大学）新美礼彦（公立はこだて未来大学）伊藤恵（公立はこだて未来大学） [FOSE-2] プログラム理解のためのコードリーディング支援ツールの提案と実装 ○大村裕（東京工業大学・大学院情報理工学研究科・計算工学専攻）渡部卓雄（東京工業大学・大学院情報理工学研究科・計算工学専攻） ◎PPLセッション (6)：言語実装 9月10日（水） 10:00-12:00 （IB014） [PPL6-1]（特別講演）SML# in Industry: A Practical ERP System Development 　　○Atsushi Ohori （Tohoku University）　　Katsuhiro Ueno （Tohoku University）　　Kazunori Hoshi （NEC Solution Innovators, Ltd.）　　Shinji Nozaki （NEC Solution Innovators, Ltd.）　　Takashi Sato （NEC Solution Innovators, Ltd.）　　Tasuku Makabe （NEC Solution Innovators, Ltd.）　　Yuki Ito （NEC Solution Innovators, Ltd.）　　(ACM ICFP 2014にて発表) [PPL6-2] Processingアプリケーション開発のための視覚的ドメイン特化言語の実装 ○栗原あずさ（法政大学大学院情報科学研究科）佐々木晃（法政大学情報科学部）脇田建（東京工業大学大学院情報理工学研究科）細部博史（法政大学情報科学部） [PPL6-3] 高レベルLLVMマクロとしてのMetaOCaml ○高島尚希（筑波大学コンピュータサイエンス専攻） Oleg Kiselyov（筑波大学コンピュータサイエンス専攻）亀山幸義（筑波大学コンピュータサイエンス専攻） [PPL6-4] Implementing a subset of Lambda Prolog in HyperLMNtal ○Alimujiang Yasen（Waseda University） Kazunori Ueda（Waseda University） ◎一般セッション (6)：知能，ユーザビリティ 9月10日（水） 13:15-15:15 （IB011）座長：櫻井祐子（九州大学） [一般6-1]（特別講演）Two Case Studies for Trading Multiple Indivisible Goods with Indifferences 　　Akihisa Sonoda （Kyushu University）　　Etsushi Fujita （Kyushu University）　　○Taiki Todo （Kyushu University）　　Makoto Yokoo （Kyushu University）　　(AAAI-14にて発表) [一般6-2]（特別講演）Intelligence Arms Race: Delayed Reward Increases Complexity of Agent Strategies 　　○Hirotaka Osawa （University of Tsukuba）　　(AAMAS 2014にて発表) [一般6-3] ASIRRAシステムに対する機械的な突破の検証 ○飯田貴章（東京電機大学）藤本衡（東京電機大学） [一般6-4] リモート・ユーザビリティテストの実施容易性と有効性の評価実験 ○西本光司（公立はこだて未来大学）南部美砂子（公立はこだて未来大学）伊藤恵（公立はこだて未来大学） ◎PPLセッション (7) 9月10日（水） 13:15-15:15 （IB014） [PPL7-1] 対話的修正と対象プログラムとの合成手法 ○森口　草介（関西学院大学）高橋　和子（関西学院大学） [PPL7-2] 検証済みのコードによるCoqからScalaへのコード抽出 ○逸見港（東京大学）田辺良則（国立情報学研究所）今井宜洋（有限会社ITプランニング）萩谷昌己（東京大学） [PPL7-3] Weak HOASを用いたFeatherweight JavaとFeatherweight GJのCoq上での形式化 ○奥村健太郎（京都大学大学院情報学研究科）五十嵐淳（京都大学大学院情報学研究科） [PPL7-4] Aπ計算のCoqによる形式化 ○安武祥平（東京工業大学）渡部卓雄（東京工業大学） ◎一般セッション (7)：分散システム，言語処理系 9月10日（水） 15:30-17:00 （IB011）座長：細部博史（法政大学） [一般7-1] 関数型言語SML#における64ビット対応への取り組み ○逢坂美冬（東北大学）佐々木智啓（東北大学） Charles Mejia Cruz（東北大学）上野雄大（東北大学）大堀淳（東北大学） [一般7-2] 通信制約を考慮した遠隔介護のための適応型コミュニケーション支援システムの実現 ○片山真也（名古屋工業大学）白松俊（名古屋工業大学）大囿忠親（名古屋工業大学）新谷虎松（名古屋工業大学） [一般7-3] 数式処理に基づくハイブリッドシステムシミュレータHyroseの大規模モデルシミュレーションに向けた拡張 ○河野文彦（早稲田大学大学院基幹理工学研究科）小林輝哉（早稲田大学大学院基幹理工学研究科）松本翔太（早稲田大学大学院基幹理工学研究科）上田和紀（早稲田大学理工学術院） ◎一般セッション (8)：ソフトウェア工学 9月10日（水） 15:30-17:00 （IB014）座長：花川典子（阪南大学） [一般8-1] BABOKを活用したチェックシートによるRFP評価の試み ○斉藤篤史（公立はこだて未来大学）伊藤恵（公立はこだて未来大学） [一般8-2] When Project Centralization and Random Testing Meet --Efficient Automatic Testing of Multiple Software Product Variants-- ○Lei Ma（The University of Tokyo） Cyrille Artho（AIST / RISEC） Cheng Zhang（The University of Waterloo） Hiroyuki Sato（The University of Tokyo） [一般8-3] 開発のためのCMMIの成熟度レベルごとの関連プロセス領域ネットワークの中心性可視化 ○日下部茂（九州大学）林信宏（九州大学）大森洋一（九州大学）荒木啓二郎（九州大学） ◎デモ・ポスターセッション 9月9日（火） 17:00-18:00 （講義室前プレゼンスペース） [ポスター-1] Coqを使ったライン型ネットワークトポロジー上でのCCNのモデル化と検証について森嶋崇（関西学院大学）後藤瑞貴（関西学院大学）高橋和子（関西学院大学） [ポスター-2] ページ回収によるOSノイズを削減するシステム高橋秀明（電気通信大学）高橋一志（電気通信大学 / JST, CREST）大山恵弘（電気通信大学 / JST, CREST） [ポスター-3] 拡張可能で安全な統合言語クエリ鈴木健一（筑波大学コンピュータサイエンス専攻）オレッグ・キセリョーヴ（筑波大学コンピュータサイエンス専攻）亀山幸義（筑波大学コンピュータサイエンス専攻） [ポスター-4] PBL向けフォーマル/インフォーマルをまたがる学習サービス大場　みち子（公立はこだて未来大学）山口　琢（公立はこだて未来大学） [ポスター-5] 妥当なPCLA表現の帰納的定義とその正当性について後藤瑞貴（関西学院大学）高橋和子（関西学院大学） [ポスター-6] FOSE2014の開催と目的尾花将輝（大阪工業大学）花川典子（阪南大学）杉山安洋（日本大学） [ポスター-7] Shiranui: テストフレンドリーなライブプログラミング言語環境今井朝貴（東京工業大学理学部情報科学科）増原英彦（東京工業大学大学院情報理工学研究科数理・計算科学専攻）青谷知幸（東京工業大学大学院情報理工学研究科数理・計算科学専攻） [ポスター-8] シェルコマンドを型安全に利用するための領域特化言語OCommand 朝倉泉（東京工業大学大学院情報理工学研究科数理・計算科学専攻）増原英彦（東京工業大学大学院情報理工学研究科数理・計算科学専攻）青谷知幸（東京工業大学大学院情報理工学研究科数理・計算科学専攻） [ポスター-9] LLVMを活用した例外処理の実現のためのコンパイラ基盤COINS の拡張産一傑（広島市立大学）川端英之（広島市立大学）北村俊明（広島市立大学） [ポスター-10] 分析・モニタリングのために作文活動を測定するシステムの設計山口琢（公立はこだて未来大学大学院）大場みち子（公立はこだて未来大学）高橋修（公立はこだて未来大学）

1 0

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml