Logic-ml September 2011

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

14 participants
21 discussions

Workshop on linear logic
by Kazushige TERUI 26 Sep '11

26 Sep '11

(English version below) 10月中旬より京都大学客員教授としてJean-Yves Girard氏が京都に滞在されます。またフランス・イタリアの線型論理グループから若手研究者・学生の訪問が予定されております。それに伴いまして、下記の要領にて線型論理ワークショップを開催したいと思います。どうぞ参加・講演をご検討いただければと思います。 * 旅費援助を希望の方は10月3日（月）まで　講演希望の方は10月17日（月）までに下記のフォームを　お送りください。日時：2011年11月7日（月）−11日（金）（ただし11日はディスカッション・学生セッションの予定）場所：京都大学理学部3号館110号室内容：Girard氏による4回の講義および　　　一般参加者の講演・ディスカッションテーマ：＊相互作用の幾何＊トレース付きモノイダル圏＊陰計算量理論＊その他線型論理および周辺の話題フランス・イタリアからの参加者： Ugo Dal Lago (Bologne) Etienne Duchesne (Marseille) Claudia Faggian (Paris) Marco Gaboardi (Bologne) Jean-Yves Girard (Marseille) Stefano Guerrini (Paris) Damiano Mazza (Paris) Michele Pagani (Paris)、他参加費：無料旅費：若干の旅費援助が可能です。ご相談ください。 ※必ずしもご希望に添えない場合があることをご了承ください。名称：RIMS共同研究集会「相互作用の幾何・トレース付きモノイダル圏・非明示的計算量」参加ご希望の方は下記のフォームを terui(a)kurims.kyoto-u.ac.jp までお送りください。 ------------------------------------- １．お名前・所属・身分２．参加日程：11月?日から〜11月?日まで３．講演を希望する・しない講演希望の場合、時間（30分・45分）４．旅費補助を希望する・しない　　旅費希望の場合、滞在日程 -------------------------------------- Workshop on Linear Logic On occasion of Dr. Jean-Yves Girard's visit to Kyoto (as well as other researchers from Europe), we plan to organize an informal workshop on linear logic (including 4 lectures by J.-Y. Girard) in the coming November. Your participation and talk contribution would be welcome. Dates: 7th - 11th November, 2011 (11th is reserved for free discussion and student session) Location: Department of Mathematics, Kyoto University Topics: Geometroy of interaction, traced monoidal categories, implicit computational complexity and any other topics related to linear logic and associated fields. Participants from Europe: Ugo Dal Lago (Bologne) Etienne Duchesne (Marseille) Claudia Faggian (Paris) Marco Gaboardi (Bologne) Jean-Yves Girard (Marseille) Stefano Guerrini (Paris) Damiano Mazza (Paris) Michele Pagani (Paris), and others. * Some limited amount of travel support is available. If you want to participate in the workshop, please send the form below to terui(a)kurims.kyoto-u.ac.jp by: 3rd October (if you wish financial support) 17th October (if you contribute a talk). ----- Registration form 1. Name, Affiliation, Position 2. Period of your participation: ?th - ?th November 3. Do you want to give a talk? If so, how long (30min or 45min)? 4. Do you wish financial support for your travel? If so, tell us your arrival and departure dates. ------------------------------------------ Kazushige TERUI Research Institute for Mathematical Sciences, Kyoto University. Kitashirakawa Oiwakecho, Sakyo-ku, Kyoto 606-8502, JAPAN. Phone: +81-75-753-7235 Fax: +81-75-753-7276 terui(a)kurims.kyoto-u.ac.jp http://www.kurims.kyoto-u.ac.jp/~terui/

1 0

Sendai Logic Seminar (Sep. 26)
by Naohi Eguchi 21 Sep '11

21 Sep '11

Logic-ml の皆様，東北大学の江口と申します．下記の要領で東北大学ロジックセミナー(田中一之研究室)を開催いたします．興味のある方は参加をご検討ください．日時：9月26日(月)，16時から．場所：東北大学北青葉山キャンパス理学総合棟1201号室発表者：Florian Pelupessy (Ghent University, Belgium) タイトル：Phase transitions for unprovability アブストラクト： The talk will be an introduction to phase transitions for unprovability: theorems with a parameter function change from provable to unprovable with a change in that parameter. Additionally we will present a transition for a Ramsey-like statement and for a theorem by Maclagan on monomial ideals. 東北大学ロジックセミナーの詳細につきましては下記をご参照ください． https://sites.google.com/site/sendailogichomepage/ 江口直日 -- Naohi Eguchi Mathematical Institute, Tohoku University 6-3, Aramaki Aza-Aoba, Aoba-ku, Sendai 980-8578, Japan E-mail: eguchi(a)math.tohoku.ac.jp

1 0

直前のお知らせ：Jouannaud氏Talk; Sept 22nd (木曜夕方)Mita Logic Seminar, on completion methods
by Mitsu Okada 21 Sep '11

21 Sep '11

****MITA LOGIC SEMINAR; PROF. J- P JOUANNAUD'S TALK and a discussion session**** ******************************************************************************* (The meeting is open to everyone without any preregistration) Theme "Completion methods, in Logic, algebra and Computer science" The Knuth-style completion procedure bridges Logic, Algebra and Computation. The aim of this meeting is to discuss the completion issue from the logical, algebraic, computer-scientific, historical and philosophical points of view. Date/Time Sept 22 Thursday 16:30pm-18:00pm Place: Meeting Room number 1, Basement of North Building (Hita-Kan), Mita Campus of Keio University; 5 minutes walking distance from JR-Tamachi, Subway-Mita or Subway-Akabanebashi. we recommend to you to use the East Gate where you find a security guard to ask the exact direction to the Meeting Room, if it is not clear for you with the campus map on our university's homepage. Main Speaker: Prof. Jean-Pierre Jouannaud, Professor of l'Ecole polytechnique and of INRIA, (French National Instutute of Computer Science) as well as the Ｓｏｆｔｗａｒｅ Chair of :INRIA- Tsinghua(精華大学) Beijing. Title: A complete tour of completion methods After the talk, we plan to have a discussion session on Knuth-Huet completions and some ther completion issues from the historical, mathematical, computer-scientific and philosophical view points.Af Abstract We shall present a unified view of completion methods in abstract algebras (Knuth and Bendix ; Peterson and Stickel; Huet; Jouannaud and Kirchner; Bachmair Dershowitz and Hsiang; Marché; Jouannaud Liu and Luo) and polynomial rings (Janet, Hironaka, Buchberger, Mora). Indeed, there are two quite different completion methods: Janet's methods, based on maintaining an inter-reduced system as a completion invariant, and all the others, based on reaching an inter-reduced system in the limit. As a result, we derive a new completion algorithm for abstract algebras. We conclude with a set of open problems when using an ill-founded completion order (inspired from Hironaka's local ring computation technique). Profile of the guest speaker: Jean-Pierre Jouannaud graduated from Ecole Polytechnique de Paris and obtained his doctorate from University Paris 6 in 1978. He was then a professor at the universities of Nancy, Paris-Sud, and at Ecole Polytechnique successively, as well as an invited professor at a number of places, including Stanford Research Institute and Stanford University in US, the University of Barcelona in Spain, Keio University in Japan and National Taiwan University in Taiwan. He is now a visiting chair professor at Tsinghua University in Beijing, China, holding a joint appointment with INRIA, the French research institute in ICT. His current research interests are at the interplay between deduction rules, rewrite rules, decision procedures and type theory, in the development of proof assistants (in particular, Coq, a leading open source proof assistant), and in their application to the formal proof of systems. He is the head of FORmal Methods for Embedded Systems, a joint project of LIAMA, the french-chinese consortium hosting their collaborative research in ICT of which he is the current french director. He published over 100 papers, among which 10 have over one hundred citations each. He won several awards during his career, including the "Prix Montpetit" of the french "Academie des Sciences" and the price for international scientific collaboration delivered by the "Academie des Sciences" and the National Research Council of Taiwan. He was on the program committee of a number of major international conferences including LICS (chair in 2011), ICALP, CSL, MFCS, FPLCA, RTA, CADE, etc. He created the International Conference on Rewriting Techniques and Applications, the International Conference on Constraints in Computational Logics which later merged with "Constraints" , the international workshops UNIF and CTRS, and the international conference on Certified Proofs and Programs to be held for the first time in 2011 in Kenting, Taiwan. He has been or is a member of the editorial boards of the Journal of Symbolic Computation, Information and Computation, Constraints, Progress in Theoretical Computer Science, and the International Journal of Softare and Informatics. He has been a member of the scientific council of the European Association for Computer Science Logic and of the European Association for Theoretical Computer Science. He has also been a member of the "Fachbeirat" of the Max Planck Institute for Computer Science, and is now on the scientific visiting committee of Academia Sinica, Taiwan. He chaired the jury of the Goedel prize awarded jointly by the EATCS and ACM-SIGACT in 2010, was a member of the jury of the Goedel prize (2008, 2009, 2010), of the LICS "test of time award" 2010, of the Kleene Price 2010, and of the Ackerman price 2011 ご不明な点がございましたら、logic(a)abelard.flet.keio.ac.jp (論理とオントロジーオープンリサーチセンター事務局まで、ご連絡ください。　岡田光弘、慶応大 ------------------------------- .

1 1

Kobe Colloquium
by Makoto Kikuchi 21 Sep '11

21 Sep '11

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領で神戸情報数理コロキウムを開催します。【１】（日程が変更になりました）日時：2011年9月22日（木）15:00 ～ 16:00 場所：神戸大学自然科学総合研究棟3号館4階421室（渕野グループ内プレゼンテーション室）講演者：Florian Pelupessy（Ghent 大学）題目：Phase transitions for unprovability アブストラクト： The talk will be an introduction to phase transitions for unprovability: theorems with a parameter function change from provable to unprovable with a change in that parameter. Additionally we will present a transitiona for a Ramsey-like statement and for a theorem by Maclagan on monomial ideals. 【２】日時：2011年10月18日（火）14:00 ～ 15:00 場所：神戸大学自然科学総合研究棟3号館4階421室（渕野グループ内プレゼンテーション室）講演者：Sam Sanders（東北大学，Ghent 大学）題目：Reverse-engineering (Constructive) Reverse Mathematics アブストラクト： Constructive Analysis was introduced by Erret Bishop to identify the `computational meaning' of Mathematics. In the spirit of intuitionistic mathematics, notions like `algorithm', `explicit computation' and `finite procedure' are central. The exact meaning of these vague terms was left open, to ensure the compatibility of Constructive Analysis with several traditions in Mathematics. Bishop did explicitly identity many non-algorithmic principles, thus implicitly defining `algorithm'. One of the goals of Constructive Reverse Mathematics (CRM) is to analyze the role of these non-algorithmic principles in Mathematics. Bishop famously derided Nonstandard Analysis for its lack of computational meaning. In this talk, we introduce `$\Omega$-invariance' : a simple and elegant definition of `finite procedure' in (classical) Nonstandard Analysis. Using an intuitive interpretation, we obtain many results from CRM, thus showing that $\Omega$-invariance is quite close to Bishop's notion of `algorithm'. 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm 連絡先：菊池誠　mkikuchi(a)kobe-u.ac.jp

1 0

Sendai Logic Seminar (Sep. 26)
by Naohi Eguchi 20 Sep '11

20 Sep '11

Logic-ml の皆様，東北大学の江口と申します．下記の要領で東北大学ロジックセミナー(田中一之研究室)を開催いたします．興味のある方は参加をご検討ください．日時：9月26日(月)，16時から．場所：東北大学北青葉山キャンパス理学総合棟1201号室発表者：Florian Pelupessy (Ghent University, Belgium) タイトル：Phase transitions for unprovability アブストラクト： The talk will be an introduction to phase transitions for unprovability: theorems with a parameter function change from provable to unprovable with a change in that parameter. Additionally we will present a transition for a Ramsey-like statement and for a theorem by Maclagan on monomial ideals. 東北大学ロジックセミナーの詳細につきましては下記をご参照ください． https://sites.google.com/site/sendailogichomepage/ -- 江口直日東北大学理学研究科数学専攻 980-8578 宮城県仙台市青葉区荒巻字青葉6ー3 E-mail: eguchi(a)math.tohoku.ac.jp

1 0

秋季総合分科会
by KASHIMA Ryo 20 Sep '11

20 Sep '11

【先週 kisoron-ml に下記メールを送ったのですが配信されないようなので再送します。念のため logic-ml にも送ります。】日本数学会数学基礎論および歴史分科会会員の皆様、分科会連絡責任評議員の鹿島です。 28日(水)から信州大学（松本）にて秋の学会が開催されます。今回は当分科会から推薦の企画特別講演　新井敏康先生「はじめての数学基礎論」（28日(水)13:00 第I会場）があります。その他の分科会行事は第II会場で　28日(水)：一般講演，歴史部門懇談会．　29日(木)：一般講演，特別講演，分科会総会．となっています。皆様のご参加をお待ちしています。 ----- 鹿島亮東京工業大学大学院情報理工学研究科数理・計算科学専攻 kashima(a)is.titech.ac.jp

1 0

Kobe Colloquium
by Makoto Kikuchi 19 Sep '11

19 Sep '11

Kobe Colloquium on Logic, Statistics and Informatics 本日，予定していました神戸情報数理コロキウムですが，台風の影響で神戸市に大雨洪水警報が発令されていますので延期します．新たな日程は改めてご連絡いたしますが，今のところ22日（木）の午後を予定しています．よろしくお願いします．菊池誠

1 0

Final Call for Papers: PEPM 2012 (論文投稿締め切り：2011年10月11日 08:59, JST)
by Kohei SUENAGA 17 Sep '11

17 Sep '11

皆様、 (重複して受け取られた方はどうぞご容赦下さい。) 京都大学の末永幸平と申します。来年1月にアメリカ合衆国フィラデルフィアで開催される PEPM 2012 の final CFP をお送りします。論文投稿締め切りはGMTで2011年10月10日23:59 日本時間で10月10日午前08:59です。部分評価に関するトピックのみならず、プログラム変換・解析等に関する話題を広く扱っております。また、ツールのプレゼンテーションや萌芽的な話題をターゲットとしたショートペーパーも受け付けております。どうぞ投稿をご検討ください。末永幸平京都大学大学院情報学研究科日本学術振興会特別研究員(PD) -- ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation January 23-24, 2012. Philadelphia, Pennsylvania, USA (co-located with POPL'12) Call For Papers http://www.program-transformation.org/PEPM12 The PEPM Symposium/Workshop series aims to bring together researchers and practitioners working in the broad area of program transformation, which spans from refactoring, partial evaluation, supercompilation, fusion and other metaprogramming to model-driven development, program analyses including termination, inductive programming, program generation and applications of machine learning and probabilistic search. PEPM focuses on techniques, supporting theory, tools, and applications of the analysis and manipulation of programs. Each technique or tool of program manipulation should have a clear, although perhaps informal, statement of desired properties, along with an argument how these properties could be achieved. Topics of interest for PEPM'12 include, but are not limited to: - Program and model manipulation techniques such as: supercompilation, partial evaluation, fusion, on-the-fly program adaptation, active libraries, program inversion, slicing, symbolic execution, refactoring, decompilation, and obfuscation. - Program analysis techniques that are used to drive program/model manipulation such as: abstract interpretation, termination checking, binding-time analysis, constraint solving, type systems, automated testing and test case generation. - Techniques that treat programs/models as data objects including metaprogramming, generative programming, embedded domain-specific languages, program synthesis by sketching and inductive programming, staged computation, and model-driven program generation and transformation. - Application of the above techniques including case studies of program manipulation in real-world (industrial, open-source) projects and software development processes, descriptions of robust tools capable of effectively handling realistic applications, benchmarking. Examples of application domains include legacy program understanding and transformation, DSL implementations, visual languages and end-user programming, scientific computing, middleware frameworks and infrastructure needed for distributed and web-based applications, resource-limited computation, and security. To maintain the dynamic and interactive nature of PEPM, we will continue the category of `short papers' for tool demonstrations and for presentations of exciting if not fully polished research, and of interesting academic, industrial and open-source applications that are new or unfamiliar. Student attendants with accepted papers can apply for a SIGPLAN PAC grant to help cover travel expenses and other support. All accepted papers, short papers included, will appear in formal proceedings published by ACM Press. In addition to printed proceedings, accepted papers will be included in the ACM Digital Library. Selected papers may later on be invited for a journal special issue dedicated to PEPM'12. The SIGPLAN Republication Policy and ACM's Policy and Procedures on Plagiarism apply. Submission Categories and Guidelines Authors are strongly encouraged to consult the advice for authoring research papers and tool papers before submitting. The PC Chairs welcome any inquiries about the authoring advice. Regular research papers must not exceed 10 pages in ACM Proceedings style. Short papers are up to 4 pages in ACM Proceedings style. Authors of tool demonstration proposals are expected to present a live demonstration of the described tool at the workshop (tool papers should include an additional appendix of up to 6 extra pages giving the outline, screenshots, examples, etc. to indicate the content of the proposed live demo at the workshop). Important Dates - Paper submission: Mon, October 10, 2011, 23:59, GMT - Author notification: Tue, November 8, 2011 - Workshop: Mon-Tue, January 23-24, 2012 Invited Speakers - Markus Pueschel (ETH Zurich, Switzerland) - Martin Berger (University of Sussex, UK) Program Chairs - Oleg Kiselyov (Monterey, CA, USA) - Simon Thompson (University of Kent, UK) Program Committee Members - Emilie Balland (INRIA, France) - Ewen Denney (NASA Ames Research Center, USA) - Martin Erwig (Oregon State University, USA) - Sebastian Fischer (National Institute of Informatics, Japan) - Lidia Fuentes (Universidad de Malaga, Spain) - John Gallagher (Roskilde University, Denmark and IMDEA Software, Spain) - Dave Herman (Mozilla Research, USA) - Stefan Holdermans (Vector Fabrics, the Netherlands) - Christian Kaestner (University of Marburg, Germany) - Emanuel Kitzelmann (International Computer Science Institute, USA) - Andrei Klimov (Keldysh Institute of Applied Mathematics, Russian Academy of Sciences) - Shin-Cheng Mu (Academia Sinica, Taiwan) - Alberto Pardo (Universidad de la Repu'blica, Uruguay) - Kostis Sagonas (Uppsala University, Sweden and National Technical University of Athens, Greece) - Anthony M. Sloane (Macquarie University, Australia) - Armando Solar-Lezama (MIT, USA) - Aaron Stump (The University of Iowa, USA) - Kohei Suenaga (University of Kyoto, Japan) - Eric Van Wyk (University of Minnesota, USA) - Kwangkeun Yi (Seoul National University, Korea)

1 0

Kobe Colloquium
by Makoto Kikuchi 16 Sep '11

16 Sep '11

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領で神戸情報数理コロキウムを開催します。【１】日時：2011年9月20日（火）15:20 ～ 16:20 場所：神戸大学自然科学総合研究棟3号館4階421室（渕野グループ内プレゼンテーション室）講演者：Florian Pelupessy（Ghent 大学）題目：Phase transitions for unprovability アブストラクト： The talk will be an introduction to phase transitions for unprovability: theorems with a parameter function change from provable to unprovable with a change in that parameter. Additionally we will present a transitiona for a Ramsey-like statement and for a theorem by Maclagan on monomial ideals. 【２】日時：2011年10月18日（火）14:00 ～ 15:00 場所：神戸大学自然科学総合研究棟3号館4階421室（渕野グループ内プレゼンテーション室）講演者：Sam Sanders（東北大学，Ghent 大学）題目：Reverse-engineering (Constructive) Reverse Mathematics アブストラクト： Constructive Analysis was introduced by Erret Bishop to identify the `computational meaning' of Mathematics. In the spirit of intuitionistic mathematics, notions like `algorithm', `explicit computation' and `finite procedure' are central. The exact meaning of these vague terms was left open, to ensure the compatibility of Constructive Analysis with several traditions in Mathematics. Bishop did explicitly identity many non-algorithmic principles, thus implicitly defining `algorithm'. One of the goals of Constructive Reverse Mathematics (CRM) is to analyze the role of these non-algorithmic principles in Mathematics. Bishop famously derided Nonstandard Analysis for its lack of computational meaning. In this talk, we introduce `$\Omega$-invariance' : a simple and elegant definition of `finite procedure' in (classical) Nonstandard Analysis. Using an intuitive interpretation, we obtain many results from CRM, thus showing that $\Omega$-invariance is quite close to Bishop's notion of `algorithm'. 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm 連絡先：菊池誠　mkikuchi(a)kobe-u.ac.jp

1 0

Kobe Colloquium
by Makoto Kikuchi 12 Sep '11

12 Sep '11

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。【１】日時：2011年9月14日（水）14:00 ～ 15:00 場所：神戸大学自然科学総合研究棟3号館4階421室（渕野グループ内プレゼンテーション室）講演者：西晃央（佐賀大学）題目：Weyl の一様分布定理の対数計算への応用について【２】日時：2011年9月20日（水）15:20 ～ 16:20 場所：神戸大学自然科学総合研究棟3号館4階421室（渕野グループ内プレゼンテーション室）講演者：Florian Pelupessy（Ghent 大学）題目：Phase transitions for unprovability アブストラクト： The talk will be an introduction to phase transitions for unprovability: theorems with a parameter function change from provable to unprovable with a change in that parameter. Additionally we will present a transitiona for a Ramsey-like statement and for a theorem by Maclagan on monomial ideals. 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm 連絡先：菊池誠　mkikuchi(a)kobe-u.ac.jp

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml September 2011