Logic-ml June 2014

15 participants
16 discussions

セミナー案内
by KASHIMA Ryo 30 Jun '14

30 Jun '14

数理論理学セミナーのお知らせ日時：5月29日(木) 17:00 から場所：東京工業大学大岡山西８号館Ｗ棟10階 W1008 話者：Florian Pelupessy （東北大学）題目：Weak concrete mathematical independence. 概要： Since Gödels theorems it is known that Peano Arithmetic is incomplete, i.e. there exist sentences in the language of PA which cannot be proven, nor disproven using PA. We will discuss some examples of such statements which can be regarded as being natural, in the sense that they closely resemble theorems from mathematical practice and we will examine these statements, hoping to clarify what makes them independent of PA. ------ 本セミナーは定期的に東工大で開催しているものです。初めて参加を希望される方はご一報ください。なお，前日の水曜まで SLACS・超準解析合同シンポジウムが開催されています。そちらの詳細は下記をご覧下さい： http://www.jaist.ac.jp/~y-keita/2014SLACS-NSA/index.html ----- 鹿島亮東京工業大学大学院情報理工学研究科数理・計算科学専攻 kashima(a)is.titech.ac.jp

1 1

Nagoya Set Theory Seminar
by 吉信康夫 26 Jun '14

26 Jun '14

名古屋集合論セミナーのご案内：日時：2014年6月27日(金) 午後3時30分より場所：名古屋大学情報文化学部 SIS2 教室(全学教育棟) 名古屋市地下鉄名城線名古屋大学駅1番出口より徒歩数分、下記のキャンパスマップのB4(1)の建物です。 http://www.nagoya-u.ac.jp/access-map/index.html SIS2 教室は全学教育棟4階にあります。建物内の配置図は下記のページでみることができます。 http://www.ilas.nagoya-u.ac.jp/student/lectureroom/ 講演者：薄葉季路(神戸大学) 題目：Reflection of List-chromatic number of graphs 概要：単純グラフのList-chromatic numberの反映原理は巨大基数公理の元では無矛盾であることが知られている。一方、今回の話ではグラフの濃度を限定したbounded versionの反映原理はZFCとequuiconsistentであることの証明の概略を試みる。多数のご参加をお待ちしております。名古屋大学大学院情報科学研究科吉信康夫

1 0

CFP: HART'14
by Makoto Hamana 25 Jun '14

25 Jun '14

皆様、 Haskellと書換え系の境界領域、関係を議論するワークショップ HART'14 (Haskell And Rewriting Techniques)のご案内です。インフォーマルなワークショップですので、投稿はWork in progress な話題でも歓迎です。ぜひ関連研究者の皆様は投稿、参加をご検討ください。投稿〆切は7月2日と近いですが、興味がありましたらご相談にものれるかと思います。 -- 浜名誠群馬大学理工学府電子情報部門 ----------------------------------------------------------------- CALL FOR PAPERS Second Workshop on Haskell And Rewriting Techniques (HART 2014) http://www.program-transformation.org/HART14/ To be held on September 5, co-located with ICFP, the Haskell Symposium, etc., in Gothenburg. Haskell is an advanced purely-functional programming language. Pure functional programming is programming with equations, often defined by pattern-matching. Rewriting is the science of replacing equals by equals and thus a very powerful method for dealing with equations, often constructor-based. There are strong connections between Haskell (or generally, pure functional) programming and rewriting. The purpose of the HART workshop is to foster those connections. In addition to an invited talk by Oleg Kiselyov, we plan a half day of discussions, in an informal setting, on how Haskell (and related languages) and rewriting techniques and theories can cross-fertilize each other. Topics of interest are, for example: ==================================== - equational reasoning and other rewriting techniques for program verification and analysis; - lambda calculi and type systems for functional programs and higher-order rewrite systems; - rewriting of type expressions in the type checker; - rewriting of programs by refactoring tools, optimizers, code generators; - execution of programs as a form of graph rewriting (terms with sharing); - Template Haskell, generally introducing a rewriting-like macro language into the compilation process. This list of topics is non-exclusive. If you have a contribution that connects Haskell and rewriting, then submit. Also, the workshop is deliberately open for discussion of rewriting-related aspects of languages like Agda, Clean, ... When in doubt, please contact a member of the PC (see below). Dates: ====== July 2: deadline for submissions July 21: notification of acceptance September 5: workshop Submission and proceedings: =========================== We solicit two types of submissions: - Extended abstracts. Presenting original research, and also preliminary reports of work in progress. Will be included in the proceedings. - Presentation-only papers. Describing work recently published or submitted. Only abstract will be included in the proceedings. Papers should be at most 5 pages in length, and should use the easychair.cls style. Submission is electronically at https://www.easychair.org/conferences/?conf=hart2014 In line with the informal style of the workshop, the reviewing of submissions will be light. Proceedings will be made available electronically. Program committee: ================== Program Chairs Kristoffer Rose (Two Sigma Investments, LLC, USA) Janis Voigtlander (University of Bonn, Germany) Program Committee Members Bertram Felgenhauer (University of Innsbruck, Austria) Carsten Fuhs (University College London, UK) Andy Gill (University of Kansas, USA) Makoto Hamana (Gunma University, Japan) Bastiaan Heeren (Open Universiteit, Netherlands) Femke van Raamsdonk (VU University Amsterdam, Netherlands) Tiark Rompf (EPFL and Oracle Labs, Switzerland) Christian Sternagel (JAIST, Japan; University of Innsbruck, Austria) Johannes Waldmann (HTWK Leipzig, Germany)

1 0

モデル理論夏の学校2014＠筑波大学
by kota takeuchi 25 Jun '14

25 Jun '14

皆様、筑波大学の竹内耕太です。モデル理論夏の学校は毎年夏に開催されるモデル理論の研究集会です。今年は9月に筑波大学で開催されます。モデル理論ならびに関連分野に興味をお持ちの方はぜひご参加下さい。 (また講演希望者や学生を対象に一部旅費の援助も検討しています。必要に応じてご相談ください。) 竹内耕太 ------------------------------------------------------------------ モデル理論夏の学校2014 開催案内・参加募集ウェブページ：http://www.math.tsukuba.ac.jp/~kota/summerworkshop2014.html 日時：2014年9月14日（日）－16日（火）会場：筑波大学（つくばキャンパス）講演申込締切：8月31日（日）世話人連絡先：竹内耕太 kota(a)math.tsukuba.ac.jp 講演を希望される方は・タイトル・氏名・所属・希望時間（あれば）を竹内までメールにてお知らせください。参加に事前申し込みは必ずしも必要ありませんが、大まかな人数を把握するために事前に参加の旨連絡いただけるとうれしいです。竹内耕太（筑波大学）

1 0

第二十五回 ALGI（代数，論理，幾何と情報科学研究集会）の講演募集のお知らせ
by Koki Nishizawa 24 Jun '14

24 Jun '14

logic-mlメーリングリストの皆様，神奈川大学の西澤弘毅と申します。第二十五回 ALGI（代数，論理，幾何と情報科学研究集会）の開催のお知らせと講演の募集をさせていただきます。 **************************************************************** * 第二十五回 ALGI（代数，論理，幾何と情報科学研究集会） * * * * 2014年8月19日（火）午後〜20日（水） * * 神奈川大学　横浜キャンパス３号館２０６室（神奈川県横浜市） * * * * 開催のお知らせと講演の募集 * **************************************************************** < 重複してお受け取りの節はご容赦願います。> ALGI (Algebra, Logic, Geometry and Informatics) は、代数学や論理学、幾何学の情報科学への応用について、および情報科学の代数学や論理学、幾何学への応用についての研究集会で、年一回の頻度で開催されています。 ALGIの趣旨や過去の集会の情報がウェブページ http://sakura.imi.kyushu-u.ac.jp/algi/ にありますので、参考までに御覧ください。このたび、第二十五回ALGIを開催することになりました。開催期間及び開催場所は上記のとおりです。昨年度よりも開催時期が１ヶ月ほど早まっておりますのでご注意ください。初日の19日は午後から開催いたします。最終日20日の午後まで開催するかどうかは、講演の数によります。なお、神奈川大学横浜キャンパス３号館は今年度に立て替えられた建物のため、インターネット上の古い情報は誤っている可能性があります。こちらの地図が正確ですのでご利用ください。 http://www.kanagawa-u.ac.jp/aboutus/facilities/yokohama/ 講演を希望される方は、・題目・講演者名・e-mail address ・所属・梗概・希望時間・講演に必要な道具などの情報を nishizawa(a)kanagawa-u.ac.jp までお寄せください。「講演したいと思っている」程度の不完全情報でも結構です。時間の空きがある限り、開催直前まで講演申込を受け付けるつもりですが、申込順に発表時間を割り当てていきますので、講演をお考えの方は、なるべくお早めにお知らせいただけますようにお願い致します。申し込み不要で自由にご参加いただけます。ただし懇親会については事前に詳細を告知し参加申し込みを受け付けます。できるだけ多くの皆さんのご講演・ご参加をお待ちしております。西澤弘毅（神奈川大学工学部）古澤仁（鹿児島大学理学部） -- 西澤弘毅神奈川大学工学部情報システム創成学科〒221-8686 神奈川県横浜市神奈川区六角橋3-27-1 nishizawa(a)kanagawa-u.ac.jp TEL（代表）045-481-5661　（内線：3378）

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 23 Jun '14

23 Jun '14

皆様リーズ大学のJohn Stell先生の講演のお知らせです。ふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学研究科 e-mail: ishihara(a)jaist.ac.jp -------------------------------------------------- * JAIST Logic Seminar Series * * This seminar is held as a part of the EU FP7 Marie Curie Actions IRSES project CORCON (http://corcon.net/). Date: Friday 27 June, 2014, 15:30-17:00 Place: JAIST, 7F seminar room (I-75) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Dr. John Stell (University of Leeds, UK) Title: Bi-Intuitionistic Modal Logic and Hypergraphs Abstract: I will discuss motivations from spatial reasoning and mathematical morphology (as used in image processing) for the notion of a relation on a graph. I will show how the algebra of these relations is weaker than that of relations on a set. This leads to a generalization of relation algebras in which the Boolean algebra is replaced by a symmetric Heyting algebra. These relations can be used as the accessibility relations for a modal logic in which propositions are interpreted as subgraphs of a graph or more generally a hypergraph. --------------------------------------------------

1 0

CFP: 第31回日本ソフトウェア科学会大会
by Atsushi Igarashi 22 Jun '14

22 Jun '14

# 複数受け取られた場合はご容赦ください．京都大学の五十嵐です． 9月に名古屋大学で開催される日本ソフトウェア科学会第31回大会の開催案内・参加募集です．発表申込締切は今週末となっておりますが，予稿の締切はまだ一ヶ月先です．是非発表申込をご検討いただければ幸いです．どうぞよろしくお願いいたします． -- 五十嵐淳 (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 日(水) 会場：名古屋大学東山キャンパス登壇発表申込締切： 2014 年 6 月 27 日(金) 予稿原稿締切： 2014 年 7 月 22 日(火) デモ・ポスター発表申込締切： 2014 年 8 月 8 日(金) 今年も，一般セッションに加えて，研究会セッション，ソフトウェア論文セッション，デモ・ポスター発表という多様な研究発表の場が用意されています．予稿の共著者に会員が含まれていれば非会員でも登壇発表できますので，是非，発表をご検討ください．未来のソフトウェアとそれを支えるソフトウェア科学に関する活発な議論を期待しております．今大会のセッションは以下の通りです．いずれも対象分野はソフトウェア科学全般です．一般セッション：ソフトウェア科学全般について発表の場研究会セッション：研究会と連携した企画による発表の場ソフトウェア論文セッション：先進的なアイデアを実現したソフトウェアの成果発表の場デモ・ポスター発表：登壇発表に関するデモも歓迎します【投稿要領】・予稿の共著者 (デモ・ポスターセッションの場合は発表者) に少なくとも 1 名の正会員，学生会員または名誉会員が含まれている必要があります．ただし，発表申込時に入会手続中の場合も含みます．・大会ホームページから EasyChair にログインして発表タイトル，著者名，概要を登録してください．続いて，大会ホームページから，登壇発表予定者などの必要事項をフォームに記入してお送りください．・予稿はソフトウェア科学会の「大会論文用」スタイルファイルで作成してください． PDF のファイルサイズが 5 MB以下であれば，ページ数に通常は制限はありません（レター論文としての同時投稿の場合のみ６ページ）．詳しい方法については大会ホームページをご覧ください．【授賞】会員による優秀な登壇発表者には「高橋奨励賞」が授与されます．【学会誌への同時投稿】例年通り，発表論文の予稿を学会誌に同時投稿できます．査読の迅速化を特徴とするレター論文が選択できる他，大会発表で得られたコメントを反映した上での大会後の投稿も可能です．詳細は，大会ホームページをご覧ください．【大会組織】大会委員長：坂部俊樹 (名古屋大学) プログラム委員長：五十嵐淳 (京都大学) プログラム副委員長：大山恵弘 (電気通信大学) 運営委員長：結縁祥治 (名古屋大学) 広報委員長：石尾隆 (大阪大学) 【コンタクト先】プログラム委員長 (正・副)： jssst2014(a)easychair.org 大会組織： jssst2014-oc(a)fos.kuis.kyoto-u.ac.jp

1 0

Talks at UTokyo: Georgios Fainekos (Tue 17), Liang-Ting Chen (Wed 18)
by Ichiro Hasuo 16 Jun '14

16 Jun '14

Dear colleagues, It is my pleasure to announce two talks given by visitors to our group: Georgios Fainekos (tomorrow) on cyber-physical systems; and Liang-Ting Chen (Wed) on categorical and coalgebraic logic. No registration is needed; see you there! Best regards, Ichiro Hasuo Group MMM, University of Tokyo http://www-mmm.is.s.u-tokyo.ac.jp/?plain=false&lang=en&pos=seminar ------------------------------ Tue 17 Jun 2014, 13:00-14:00 Georgios Fainekos <http://www.public.asu.edu/~gfaineko/> (Arizona State University), Temporal Logic Testing and Verification for Cyber-Physical Systems 理学部7号館1階 102教室 Room 102, School of Science Bldg. No. 7 アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下） Access: http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom) One of the important challenges in the Model Based Development (MBD) of Cyber-Physical Systems (CPS) is the problem of verifying functional system properties. In its general form, the verification problem is undecidable due to the interplay between continuous and discrete system dynamics. In this talk, we present the bounded-time temporal logic testing and verification problem for CPS. Temporal logics can formally capture both state-space and real-time system requirements. For example, temporal logics can mathematically state requirements like "whenever the system switches to first gear, then it should not switch back to second gear within 2.5sec". Our approach in tackling this challenging problem is to convert the verification problem into an optimization problem through a notion of robustness for temporal logics. The robust interpretation of a temporal logic specification over a CPS trajectory quantifies "how much" the system trajectory satisfies or does not satisfy the specification. In general, the resulting optimization problem is non-convex and non-linear, the utility function is not known is closed-form and the search space is uncountable. Thus, stochastic search techniques are employed in order to solve the resulting optimization problem. We have implemented our testing and verification framework into a Matlab (TM) toolbox called S-TaLiRo (System's TemporAl LogIc Robustness). In this talk, we demonstrate that S-TaLiRo can provide answers to challenge problems from the automotive and medical device industries. Georgios Fainekos is an Assistant Professor at the School of Computing, Informatics and Decision Systems (SCIDSE) Engineering at Arizona State University (ASU). He is director of the Cyber-Physical Systems Lab and he is currently affiliated with the Center for Embedded Systems at ASU. He received his Ph.D. in Computer and Information Science from the University of Pennsylvania in 2008 where he was affiliated with the GRASP laboratory. He holds a Diploma degree (B.Sc. & M.Sc.) in Mechanical Engineering from the National Technical University of Athens and an M.Sc. degree in Computer and Information Science from the University of Pennsylvania. Before joining ASU he held a Postdoctoral Researcher position at NEC Laboratories America in the System Analysis & Verification Group. He is currently working in the area of Cyber-Physical Systems (CPS) with focus on formal methods, logic, optimization and control theory with applications to automotive systems, autonomous (ground and aerial) robots and human-robot interaction (HRI). In 2014, Dr. Fainekos received the NSF CAREER award. He was recipient of the 2008 Frank Anger Memorial ACM SIGBED/SIGSOFT Student Award, and the 2013 Best Researcher Junior Faculty award from SCIDSE. ------------------------------ Wed 18 Jun 2014, 16:30-18:00 Liang-Ting Chen <http://uk.linkedin.com/pub/liang-ting-chen/88/749/b5a> (Academia Sinica), On a Categorical Framework for Coalgebraic Modal Logic 理学部7号館1階 102教室 Room 102, School of Science Bldg. No. 7 アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下） Access: http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom) Two syntax-oriented approaches to coalgebraic modal logic ― Moss’ cover modality and Pattinson’s predicate liftings ― are successful in producing a wide range of modal logics parametric in a Set functor, including modal logics for Kripke frames, Markov chains, Markov processes, and their variants. Both of them can be presented abstractly in a form similar to mathematical SOS by Turi and Plokin, but this line of research was not well-understood yet. In this talk I will treat the abstract formation seriously, and introduce a category of abstract semantics parametric in a contravariant functor that assigns to the state space its collection of predicates with propositional connectives. Various classical notions are formulated categorically. For example, modular constructions are identified as colimits, limits, and compositions of one-step semantics. The compositions and the colimits of (one-step) expressiveness semantics remain (one-step) expressive. In addition, we investigate a canonically-defined logic by its fibres, and show that it is a terminal object for every fibre. By its very formulation, it is straightforward to show above results in this level of generality. In fact, I would like to suggest that it is the right level of abstraction for understanding coalgebraic modal logic. For further details, please see my MFPS paper, available in http://www.cs.cornell.edu/Conferences/MFPS30/MFPS30-prelim.pdf

1 0

Continuity, Computability, Constructivity 2014; extended deadline
by Hajime Ishihara 10 Jun '14

10 Jun '14

*Continuity, Computability, Constructivity -- From Logic to Algorithms (CCC 2014)* *University of Ljubljana, 15-19 September 2014* *Third call for papers* *Extended deadline* http://ccc2014.fmf.uni-lj.si/ CCC is a workshop series bringing together researchers from realanalysis, computability theory, and constructive mathematics. The overall aim is to apply logical methods in these disciplines to provide a sound foundation for obtaining exact and provably correctalgorithms for computations with real numbers and related analytical data, which are of increasing importance in safety critical applications and scientific computation. Previous workshops have been held in Cologne CCC 2009, Trier CCC 2012, and Gregynog 2013. One outcome of the 2009 workshop series is the creation of the EU funded research network COMPUTAL (Computable analysis -- theoretical and applied aspects) which supports research visits from Europe to Russia, South-Africa, and Japan and vice versa. This workshop also hosts the third COMPUTAL workshop, but is open to all researchers in the area. The workshop will take place in Ljubljana, Slovenia. *Scope: *The workshop specifically invites contributions in the areas of * exact real number computation, * effective topology, * Scott's domain theory, * Weihrauch's type two theory of effectivity, * category-theoretic approaches to computation on infinite data, * hierarchies of unsolvability, * and related areas. *Invited Speakers:* * Thierry Coquand (Gothenburg) * Dirk Pattinson (Canberra) * Paul Potgieter (Pretoria) * Robert Rettinger (Hagen) * Hideki Tsuiki (Kyoto) * … (tba) *Tutorial Speakers:* * Andrej Bauer (Ljubljana) * Martin Ziegler (Darmstadt) *Extended deadline for abstract submission:* *28 June 2014* ** *Upload your submission via EasyChair* https://www.easychair.org/conferences/?conf=ccc20140 <https://www.easychair.org/conferences/?conf=ccc20140> *Programme Committee:* * Andrej Bauer(Ljubljana) * Willem Fouche' (Pretoria) * Hajime Ishihara (Nomi, Ishikawa) * Margarita Korovina (Novosibirsk) * Davorin Lesnik (Darmstadt) * Norbert Mueller (Trier) * Robert Rettinger (Hagen) * Monika Seisenberger (Swansea) * Dieter Spreen (Siegen and Pretoria) (chair) * Martin Ziegler (Darmstadt). *Organizing Committee:* * Andrej Bauer (Ljubljana)

1 0

Fwd: Kobe Colloquium on Logic, Statistics and Informatics, June 10 (Dilip Raghavan)
by Joerg Brendle 09 Jun '14

09 Jun '14

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。日時：2014年6月10日（火）15:00-16:30 講演者：Dilip Raghavan （シンガポール国立大学）場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室） ============================================================ 題目： Two cardinal invariants of the continuum and Martin's axiom アブストラクト： we show the consistency of "MA for posets of size at most kappa + d = kappa^+ and a = kappa^{++}" for a measurable cardinal kappa. ============================================================ 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml June 2014