Logic-ml

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

7 participants
1772 discussions

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

22 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 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/ -- 江口直日東北大学理学研究科数学専攻 980-8578 宮城県仙台市青葉区荒巻字青葉6ー3 E-mail: eguchi(a)math.tohoku.ac.jp

1 0

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

21 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 20 Sep '11

20 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 18 Sep '11

18 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 17 Sep '11

17 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 13 Sep '11

13 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

RIMS研究集会「体のモデル理論とその応用」（11/２８〜11/30）のご案内
by 福崎賢治 13 Sep '11

13 Sep '11

皆様、モデル理論分野のRIMS研究集会は毎年11月ごろに京都大学数理解析研究所で開催されております。今年のモデル理論分野のRIMS研究集会は、「体のモデル理論とその応用」(Model Theory and its Applications)という表題のもと、　　日時：2011年11月28日（月）午後より11月30日（水）午前まで　　会場：京都大学数理解析研究所110号室にて開催されます。（はっきりした時刻はのちほどWebサイトでお知らせします。） ●Webサイト：http://www.iuk.ac.jp/~fukuzaki/rims.html ●講演募集：広い意味でモデル理論に関連する諸分野の講演を募ります。講演していただける方は、　　お名前と所属と職名　　講演タイトルを9月中をめどに、　　福崎賢治（鹿児島国際大学）　　e-mail:fukuzaki@int.iuk.ac.jp までお知らせください。世話役　福崎賢治

1 0

The 46th MLG Meeting
by Takahiro Seki 12 Sep '11

12 Sep '11

第46回 MLG 数理論理学研究集会のご案内 (重複してお受け取りの際はご容赦ください。) 　新潟大学の関と申します。　2011年度MLG数理論理学研究集会（第46回）を下記の要領で開催いたします。 =============================== 　第46回 MLG 研究集会開催要領 =============================== 　期間: 2011 年 10 月 23 日(日)〜 10 月 25 日(火) 　場所: KKR湯沢ゆきぐに（ＪＲ上越新幹線越後湯沢駅西口より徒歩約8分）　　　　〒949-6101 新潟県南魚沼郡湯沢町湯沢2574 　　　　URL : http://www.kkryuzawa.com/ 　講演・宿泊申込締め切り: 2011 年 10 月 13 日（木）　世話人：関　隆宏（新潟大学）　ホームページ：　http://math2.ed.niigata-u.ac.jp/~seki/MLG46/ ============ 　参加募集 ============ ・講演時間は原則40分を予定しています。・10月24日（月）の夜に懇親会を行います。・全日程参加の場合，参加費（宿泊代・食事代・会場代）は22,000円前後になる予定です。また，10月24日（月）の昼食を外で食べることも可能です。・ご講演をなさらなくても参加いただけます。KKR湯沢ゆきぐにで宿泊および食事をなさらない場合，事前の申し込みは不要ですが，参加費（会場代）1,500円をいただきます。・講演・宿泊を希望される方は，10月13日(木)までに下記の形式で電子メールにて世話人（tseki(a)adm.niigata-u.ac.xn--jp)-u63b4bubm7eycb4w4io072fiwzc.xn--,-d8t9d650nogb 申し込みを含むMLGに関するメールには， Subjectのはじめに MLG46 とご記載ください。 ----------------------------------- 第46回 MLG 研究集会講演・宿泊申込フォーム氏名：所属・身分：所属機関住所：〒電話番号：メールアドレス：講演について：　講演：　する / しない　講演題目：　使用機材：　白板 / プロジェクタ　　希望日時：　なし / あり　　ありの場合：　23日(午後) / 24日(午前/午後) / 25日(午前) 宿泊・食事について：　KKR湯沢ゆきぐにでの宿泊・食事：　する / しない　する場合：　23日(夕食/宿泊) / 24日(朝食/昼食/夕食/宿泊) / 25日(朝食) その他：（講演時間の変更や講演日時の希望等） ----------------------------------- --- 関　隆宏新潟大学企画戦略本部評価センター Tel : 025-262-6088 Fax : 025-262-6248 E-mail : tseki(a)adm.niigata-u.ac.jp

1 1

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml