Logic-ml May 2024

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

16 participants
18 discussions

【参加案内】情報処理学会第149回プログラミング研究会（6/13）
by KAMINA Tetsuo 31 May '24

31 May '24

大分大学の紙名と申します。情報処理学会第149回プログラミング研究発表会（PRO-2024-1）の開催案内をさせていただきます。どなたでも無料でご参加いただけますが、参加者の把握のため、下記のURLから参加申込みをお願いします。 https://www.ipsj.or.jp/kenkyukai/event/pro149.html ================================================================= 日程：2024年6月13日(木) 会場：オンライン（参加申込み後に、ZoomのURLが案内されます）研究会：https://sigpro.ipsj.or.jp/pro2024-1/ # プログラム (6/13) * 1件あたり45分（発表25分，質疑・討論20分）（短い発表は発表20分, 質疑・討論10分） * ◯印が登壇者です． ## セッション1 (13:00–14:00) [座長：森畑明昌] 招待講演「Rust から広がるソフトウェア検証・テストの新展望」 ○松下祐介（京都大学） ## 休憩 (14:00–14:15) ## セッション2 (14:15–16:15) [座長：佐藤重幸] 2024-1-(1) (14:15–15:00) 「Rustにおけるトレイトの実装の衝突を避けるための新たなトレイト境界の構文の提案」 ○岡本祐希（芝浦工業大学），篠埜功（芝浦工業大学） 2024-1-(2) (15:00–15:45) 「曲線の定性的扱いと自己交差性の判定」 ○高橋和子（関西学院大学） 2024-1-(3) (15:45–16:15) [短い発表] 「深層学習モデルの形状不一致エラーを静的に検査するHaskellライブラリ」 ○須田太斗（東京工業大学），増原英彦（東京工業大学），叢悠悠（東京工業大学） ## 懇親会 (18:00–20:00) 問合せ先：ipsj-pro-2024-1-organizer(a)googlegroups.com 担当者：佐藤重幸（電気通信大学），紙名哲生（大分大学）

1 0

JAIST Logic Seminar Series - 講演のお知らせ (6月13日)
by Nao Hirokawa 27 May '24

27 May '24

皆様６月１３日（木）に北陸先端科学技術大学院大学で行われます Baaz 教授、Gamsakhurdia 氏（ウィーン工科大学）の講演のお知らせです。皆様、どうぞ奮ってご参加ください。廣川直 (JAIST) ----------------------------------------------------------------------- * JAIST Logic Seminar Series * Date: June 13 (Thu), 2024, 15:30 - 17:10 Place: I-57g (seminar room on 5F of IS Building III) at JAIST (Access: https://www.jaist.ac.jp/english/top/access/index.html) --------------------------------------------------------- Quantifier shifts M. Baaz, Vienna University of Technology (joint work with J. Aguilera, M. Gamsakhurdia, R. Jalali) --------------------------------------------------------- Abstract: In this lecture we analyze the operation of quantifier shifts, one of the oldest deduction formalism in logic. Quantifier shifts are orthogonal to usual deduction rules and have a considerable impact on the complexity of proofs. To understand them better a variant of sequent calculus with relaxed Eigenvariable conditions is developed, which is able to represent quantifier shifts in a cut-free format. There is a non-elementary speed-up of cut-free proofs in the new format vs cut free proofs in the usual format, a manifestation of the proof-theoretic power of quantifier shifts. The intuitionistic version of this calculus is applied to prove, that an intermediary logic admits Standard Skolemization iff it admits all classical quantifier shifts. -------------------------------------------------------- The Limits of Prenexation in First-order Gödel Logics Mariami Gamsakhurdia, Vienna University of Technology (joint work with Matthias Baaz) -------------------------------------------------------- Abstract: One of the first recognised characteristics of classical logic is the existence of a prenex form for each formula. The quantifier-shifting rules are used non-uniquely to construct these prenex forms. The expressive power of prenex fragments is easy to see in classical logic because it coincides with the whole logic, and in Intuitionistic logic since the prenex formulas are very weak (the validity of the prenex formula is decidable). However, because Gödel logics are intermediary logics, the expressibility of its prenex is relatively important. It is clear that prenex normal forms cannot be constructed in the usual sense in Gödel logics because some of the quantifier-shift rules may fail, but this does not imply that no prenex normal form exists. However, demonstrating that such prenex forms do not exist is more difficult. Prenexation does not work for $G_{[0,1]}$ when $0$ is not isolated, since the formula $(\neg \forall x A(x)\wedge \forall x \neg \neg A(x))$ does not allow a prenex normal form. To prove this fact, we use a glueing argument. This result can be extended to all Gödel logics where there is one accumulation point from above, even if it is not $0$. In this talk we provide the complete classification for the first-order Gödel logics with respect to the property that the formulas admit logically equivalent prenex normal forms. We show that the only first-order Gödel logics that admit such prenex forms are those with finite truth value sets since they allow all quantifier-shift rules and the logic $G_\uparrow$ with only one accumulation point at $1$. In all the other cases, there are, in general, no logically equivalent prenex normal forms. We will also see that $G_\uparrow$ is the intersection of all finite first-order Gödel logics. The second stage of our research investigates the existence of the validity equivalent prenex normal form. Gödel logics with a finite truth value set admit such prenex forms. Gödel logics with an uncountable truth value set have the prenex normal form if and only if every surrounding of $0$ is uncountable or $0$ is an isolated point. Otherwise, uncountable Gödel logics are incomplete, and the prenex fragment is always complete with respect to the uncountable truth value set. Therefore, there is no effective translation to the valid formula and the valid prenex form. The countable case, however, is still up for debate. References Matthias Baaz, Norbert Preining Gödel-Dummett logics, in: Petr Cintula, Petr Hájek, Carles Noguera (Eds.), Handbook of Mathematical Fuzzy Logic vol. 2, College Publications, (2011), pp. 585–626, chapter VII. Matthias Baaz, Norbert Preining, Richard Zach First-order Gödel logics, Annals of Pure and Applied Logic vol. 147. (2007) pp. 23–47.

1 0

数学基礎論若手の会2024開催のお知らせ
by 樋口幸治郎 24 May '24

24 May '24

皆様、日本大学の樋口幸治郎と申します。数学基礎論若手の会 2024 の開催 (対面で実施) をご案内いたします。数学基礎論若手の会は数学基礎論を専攻する学生および若手研究者の研究交流を目的とする研究集会です。講演はオリジナルの成果発表に限らず、研究の途中報告や研究内容の紹介など幅広く募集しております。また、これから数学基礎論を勉強したいと思っている方のご参加も歓迎します。 — 開催要領 — 日程：2024 / 10 / 12（土）～ 14（月, 祝日）会場：郡山市青少年会館（福島県郡山市大槻町字漆棒82番地）世話人：樋口幸治郎（日本大学）ウェブサイト： https://sites.google.com/view/mlwakatenokai2024/%E3%83%9B%E3%83%BC%E3%83%A0 参加申込み期限：2024 / 9 / 27 (金) 参加申込み(Googleフォーム)：https://forms.gle/kPSSzGkjNwH8RQE98 講演希望の方は、上記フォームの提出後、講演タイトル・アブストラクトのtexファイルを世話人へメールで送ってください。開催時期が近づきましたら、再度お知らせいたします。多くの皆様のご参加をお待ちしております。樋口幸治郎 (日本大学工学部)

1 0

Prof. Thomas Seillerの講義のご案内　５月２８日ハイブリッド形式
by Mitsu Okada 24 May '24

24 May '24

次のご案内をさせていただけると幸いです。慶應大岡田光弘峯島宏次ーーーーーーーーーーーーーーーーーーー論理―計A算―哲学セミナーLogic-Computation-Philosophy Seminar 「プログラム」「アルゴリズム」「計算モデル」を「定義する」ことに関する Prof. Thomas Seillerの講義をご案内させていただきます。ハイブリッド形式講義Title« Defining "program", "algorithm", and "model of computation" — including a discussion on how models of linear logic emerge by generalizing geometry of interaction and transcendental syntax constructions » We will put updated information in any, here.最新情報URL https://abelard.flet.keio.ac.jp/2024/seminar_talk_202405 <https://abelard.flet.keio.ac.jp/satellite-workshop_202406/poster_ja.pdf> 5月２８日火曜日１7:30-19:00 May 28 Thuesday 慶應義塾大学三田キャンパス東館（東門の建物）4階オープンラボ三田キャンパス：アクセス：[慶應義塾] (keio.ac.jp) <https://www.keio.ac.jp/ja/maps/mita.html> キャンパスマップ13番 At the Open-Lab, 4th floor of the East (Research) Building at the East Gate of Mita-Campus of Keio University Mita Campus: Keio University <https://www.keio.ac.jp/en/maps/mita.html> Building # 13 on the Campus Map 要事前登録・Preregistration required 登録用のリンク Hybrid Meeting https://forms.gle/cbPr2vQrJA4haVFW7 Speaker：Thomas Seiller -（CNRS-LIPN, IHPST） Title of the Talk « Defining "program", "algorithm", and "model of computation" — including a discussion on how models of linear logic emerge by generalizing geometry of interaction and transcendental syntax constructions » Abstract: What is a model of computation? What is a program, an algorithm? While theoretical computer science has been founded on computability theory, the latter does not answer these questions. Indeed, it is a mathematical theory of computable functions, and does not account for computation itself. A symptomatic consequence is the notion of Turing-completeness. This standard (sole?) equivalence between models of computation is purely extensional: it does only care about what is computed and not how, blind to complexity aspects and the question of algorithmic completeness. More importantly, the theory of computation is continuously growing further from how actual machines compute. I will present a proposal for alternative foundations more faithful to computer science practice and interests. This mathematisation of computer science is grounded within the theory of dynamical systems, focussing on *how* computation is performed rather than only on *what* is computed. I will argue that it generalises computability theory while still allowing to recover standard results. This point of view can be used to: provide a uniform account of several lower bounds from algebraic complexity and strengthen them define static analysis methods which can be implemented in usable tools define families of linear realisability models (realisability models for linear logic) lead to a semantic approach of implicit computational complexity propose a formal definition of the notion of algorithm In this talk, I will focus on two aspects from this list, namely points 3 and 5: First, I will explain how abstract programs give rise to models of (fragments of) linear logic, generalising Jean-Yves Girard’s geometry of interaction (or more recent transcendental syntax) constructions. I will also explain how these technical developments shed a new light on the question of defining logical constants. Second, I will present the formal definition of algorithm that stems from the approach, discuss its properties and provide a few examples. 問い合わせ先Logic-Computation-Philosophy Group, Dept. Philoophy Keio Univ logic[AT]abelard.flet.keio.ac.jp 岡田光弘峯島宏次

1 0

APLAS 2024: Final Call for Papers
by Mirai Ikebuchi 24 May '24

24 May '24

皆様，京都大学の池渕です．APLAS 2024のfinal CfPをお送りします． Submission deadlineが延期され，5/31(金)になりました． ====================================================== Final CFP: Deadline extended till May 31 APLAS 2024 -- The 22nd Asian Symposium on Programming Languages and Systems October 22-24, 2024, Kyoto, Japan https://conf.researchr.org/home/aplas-2024/ <https://conf.researchr.org/home/aplas-2024/> APLAS 2024 aims to bring together programming language researchers, practitioners and implementors *worldwide*, to present and discuss the latest results and exchange ideas in all areas of programming languages and systems. APLAS 2024 is co-located with the 22nd International Symposium on Automated Technology for Verification and Analysis (ATVA). We solicit submissions in the form of regular research papers describing original scientific research results, including system development and case studies. Among others, solicited topics include: programming paradigms and styles; methods and tools to specify and reason about programs and languages; programming language foundations; methods and tools for implementation; concurrency and distribution; applications, case studies and emerging topics. Submissions should not exceed 17 pages, excluding bibliography, in the Springer LNCS format. The reviewing process is light double-blind, with a rebuttal phase to address factual errors and minor misunderstandings. Proceedings of APLAS 2024 will be published by Springer as part of Lecture Notes in Computer Science (LNCS). https://link.springer.com/conference/aplas <https://link.springer.com/conference/aplas> APLAS 2024 continues the tradition of the best paper award. Submission deadline: Fri May 31 (EXTENDED, firm) Response period: Jul 24-26 Acceptance notification: Fri Aug 2 Camera-ready: Sat Aug 31 The submission website is now open: https://aplas24.hotcrp.com/ <https://aplas24.hotcrp.com/> General Chair: Jacques Garrigue (Nagoya U.) Publicity Chairs: Ryosuke Sato (TUAT U.), Mirai Ikebuchi (Kyoto U.) Program Committee: Beniamino Accattoli (Inria & Ecole Polytechnique) Pierre-Evariste Dagand (IRIF / CNRS) Silvia Ghilezan (University of Novi Sad, Mathematical Institute SASA) Fritz Henglein (DIKU and Deon Digital) Mirai Ikebuchi (Kyoto University) Patrik Jansson (Chalmers University of Technology and University of Gothenburg) Oleg Kiselyov (Tohoku University, PC Chair) Hsiang-Shang ‘Josh’ Ko (Academia Sinica) Daan Leijen (Microsoft Research) Martin Lester (University of Reading) Fredrik Nordvall Forsberg (University of Strathclyde) Matija Pretnar (University of Ljubljana) Peter Schachte (The University of Melbourne) Sven-Bodo Scholz (Radboud University) Philipp Schuster (University of Tübingen) Taro Sekiyama (NII) Amir Shaikhha (University of Edinburgh) Pavle Subotic (Fantom Foundation) Yong Kiam Tan (Institute for Infocomm Research, A*STAR) Kazunori Ueda (Waseda University) Yuting Wang (Shanghai Jiao Tong University) Ki Yung Ahn (Hannam University)

1 0

2024年度日本数学会秋季総合分科会（講演申込の受付開始）
by Takahiro Seki 23 May '24

23 May '24

みなさま（重複して受け取られた方は申しわけございません。）　日本数学会の数学基礎論および歴史分科会で連絡責任評議員を務めております新潟大学の関です。　今年の日本数学会秋季総合分科会は以下のとおり開催されますが（例年より開催時期が早いです）、本日から一般講演の申込受付を開始しました。　2024年度日本数学会秋季総合分科会　　https://www.mathsoc.jp/activity/meeting/osaka24sept/index.html 　日程：9月3日（火）～6日（金）　　　（数学基礎論および歴史分科会は 5日（木）、6日（金）の予定）　会場：大阪大学豊中キャンパス　講演申込期間：5月24日（金）～6月14日（金）　みなさまのご参加とご講演をお待ちしております。　よろしくお願いいたします。 --- 関　隆宏新潟大学経営戦略本部評価センター

1 0

第7回ステアラボソフトウェア技術セミナー「Programming Language with Versions」のご案内
by 安部達也 23 May '24

23 May '24

皆様、千葉工業大学の安部達也です。東京工業大学の田辺裕大さん（https://yudaitnb.github.io/）に Programming with Versions (PWV) における最新の結果についてお話しいただけることになりました。初めてこの話を聴くという方々だけでなく、PPL'24 で時間の制約上十分に話を聴けなかった・議論したかったのに、と残念に思っていた皆様にもまた大変よい機会であると思います。ぜひご参加ください。日時：2024年5月24日（金）15:00〜16:00 場所：オンライン参加費：無料参加方法：https://stair-st.connpass.com/ 講師：田辺裕大様演題：Programming Language with Versions 概要：更新作業は現代で最も忌避される開発タスクの一つである。現代のソフトウェア開発は外部パッケージの使用に強く依存しており、外部パッケージの更新はソフトウェアの既存の振舞を破壊することがある。現代的な開発支援ツールはパッケージの依存性解析に基づいた更新支援を提供するが、コードベースの更新作業中には同一パッケージの複数バージョンへの同時依存が不可避的に生じ、実装を無視した解析を行う開発支援ツールではこの問題に有効な解決策を与えることができない。 Programming with Versions (PWV) は、この問題を解決するために近年提案された言語設計である。PWV 言語ではバージョンの概念を言語意味論に持ち込むことにより、単一のモジュールの新旧バージョンの機能を選択的に使用可能である。また、一貫した仕様に基づいたデータフローで計算が行われることを保証する。これらの機能は、膨大な作業コストを要していた更新作業の漸進化を可能にする。本講演では、APLAS'23 及び PPL'24 カテゴリ2で発表された論文 "Compilation Semantics for a Programming Language with Versions" に基づき、実験的な関数型 PWV 言語 VL 及びそのコア計算 λVL を通して、PWV の言語設計を解説する。特に、PPL'24 では時間の制約で紹介できなかった技術的詳細（安全性の原理・型システム設計・バージョン推論・コンパイル手法）や予備評価、関連する更新支援技術、将来の課題についても紹介する。問合せ先：安部達也 <abe.tatsuya(a)it-chiba.ac.jp>

1 1

助教公募(愛媛大学数理科学講座)締切R6/7/22
by FUJITA Hiroshi 23 May '24

23 May '24

Logic-MLの皆様、愛媛大学の藤田と申します。愛媛大学の数理科学講座では、下記の通り助教の公募を行うこととなりました。関係者にご周知いただくと共に、適任者をご存知の場合にはぜひ応募をお勧めいただきますようお願い申し上げます。募集人員: 助教１名所属部門: 愛媛大学大学院理工学研究科理工学専攻数理科学講座専門分野: 数学（分野は問わないがデータサイエンスに関心がある方が望ましい）担当科目: 理学部理学科数学・数理情報コースの専門科目等参考： https://www.math.sci.ehime-u.ac.jp/ 着任時期: 令和６年１２月１日以降、令和７年４月１日までのできるだけ早い時期公募締切: 令和６年７月２２日（月）必着詳細につきましては, 以下のページをご覧ください。 https://www.ehime-u.ac.jp/tp_20240522_jin02/ このお知らせを重複して受け取られた方はご容赦ください。よろしくお願い申し上げます。愛媛大学大学院理工学研究科理工学専攻数理科学講座藤田博司 fujita.hiroshi.mh(a)ehime-u.ac.jp<mailto:fujita.hiroshi.mh@ehime-u.ac.jp>

1 0

SAML 2024 の参加登録
by SAKAI Hiroshi 21 May '24

21 May '24

皆様：東京大学の酒井と申します． Symposium on Advances in Mathematical Logic (SAML) 2024 の参加登録を開始しましたので，アナウンスさせていただきます． SAML 2024 日程：7月9日(火) -- 12日(金) 形式：ハイブリッド形式対面会場：京都大学数理解析研究所ホームページ：https://sites.google.com/view/saml2024 上記ホームページにあるフォームから参加登録をしていただけます．不明な点がありましたら，下記連絡先にお問い合わせください．連絡先：酒井拓史 hrshsakai(a)gmail.com 皆様のご参加をお待ちしています．酒井拓史

1 0

第2回「若手による数理論理学研究集会」開催のお知らせ
by 西村祐輝 21 May '24

21 May '24

logic-ml のみなさま、東京工業大学の西村です。昨年開催しました『若手による数理論理学研究集会』について、第2回開催の告知をいたします。さしあたり、現在決定している事項は次の通りです。 - 日時：2024年8月7日-9日 - 場所：神奈川大学横浜キャンパス続報がありましたら、こちらのメーリスでお知らせします。また、こちらの公式サイトにも情報を掲載いたします。 https://sites.google.com/view/yorukai-2nd ご参加を検討いただけると幸いです。また、お近くに数理論理学に興味のある学生がいらっしゃる場合には、宣伝いただけるとありがたいです。どうぞよろしくお願いいたします。 -- 西村祐輝東京工業大学情報理工学院数理・計算科学系 mail: nishimura.y.as(a)m.titech.ac.jp

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml May 2024