- Logic-ml - fos.kuis.kyoto-u.ac.jp

【重要】東北大ロジックセミナーの開催形式の訂正とお詫び
by 竹田侑人 19 Jul '24

19 Jul '24

皆様, 先ほどご案内いたしましたセミナーですが, 開催形式に誤りがございました. (誤) 場所：東北大学理学研究科合同A棟801号室 (zoom配信あり) (正) 場所：zoom配信開催形式は完全オンラインとなっております. ご迷惑をおかけし, 大変申し訳ございません. 参加を希望される方は竹田(yuto.takeda.t8(a)dc.tohoku.ac.xn--jp)-u63baam6azav5czbevh0gij9rvoja5sb4j6736j2rvgn34dhb1b. 竹田侑人 yuto.takeda.t8(a)dc.tohoku.ac.jp

1 0

東北大ロジックセミナーのご案内
by 竹田侑人 19 Jul '24

19 Jul '24

皆様，東北大学の竹田です．以下の通りセミナーを開催いたしますのでご案内いたします． https://sites.google.com/view/sendai-logic/ 日時：7月26日(金)15:00〜場所：東北大学理学研究科合同A棟801号室 (zoom配信あり) 講演者：織田幸弘 (東北大学情報) 題目帰納的定義付き一階述語論理の循環証明体系におけるカット除去の反例概要循環証明体系とは証明図にサイクル（循環）の存在を許容した証明体系である．このような体系は無限降下法の形式化とみなせる場合がある．そのため，循環証明体系は帰納法を使う証明体系の代替手段として証明探索の観点から注目されている．その一方で，循環証明体系の証明論的な性質についてはまだわかっていないことが多い．本講演では帰納的定義付き一階述語論理に対する循環証明体系のカット除去の反例を与える．反例の存在から帰納的定義付き一階述語論理に対する循環証明体系においてはカット除去性という基本的な性質が成り立たないことがわかる．オンライン参加を希望される方は竹田(yuto.takeda.t8(a)dc.tohoku.ac.xn--jp)-u63baam6azav5czbevh0gij9rvoja5sb4j6736j2rvgn34dhb1b どうぞよろしくお願いいたします．竹田侑人 yuto.takeda.t8(a)dc.tohoku.ac.jp

1 0

『第二回若手による数理論理学研究集会』の告知
by 西村祐輝 18 Jul '24

18 Jul '24

logic-ml のみなさま、『第二回若手による数理論理学研究集会』運営の西村です。本会の参加申し込み・ならびに講演申し込みの締め切りは、【7/21（日）】までとなります。発表枠にもまだまだ空きがございますので、ぜひ前向きに検討をいただければと思います。また、スタッフ間で協議の上、現在オンライン形式での配信も予定をしております。詳細が決まり次第 logic-ml にも告知いたしますので、今しばらくお待ちください。詳細はこちらのホームページもご覧ください。 https://sites.google.com/view/yorukai-2nd どうぞよろしくお願いいたします。 -- 西村祐輝東京工業大学情報理工学院数理・計算科学系 mail: nishimura.y.as(a)m.titech.ac.jp

1 0

教員公募：早稲田大学情報理工学科 (女性限定)
by Tachio Terauchi 12 Jul '24

12 Jul '24

皆様、早稲田大学の寺内です。下記のように教員を公募しておりますので、ぜひ応募をご検討下さい。また、関心のある方にご周知頂けますと幸いです。どうぞよろしくお願い致します。寺内 ====================================================================== 早稲田大学情報理工学科専任教員公募（女性限定）募集人数：1名（女性限定）勤務形態：常勤（任期なし）採用資格：教授、准教授または専任講師（いずれも任期なし） ※職位は、教育・研究歴、年齢などに応じて早稲田大学が決定し、最終面接までに提示します。 ※着任時に 61 歳以上の方は特任教授としての嘱任となり、待遇は本学の「特任教授給規程」によります。 ※資格に関わらず満 70 歳に達する年度を超えて契約を更新することはできません。教育・研究領域の分野：情報理工学分野学内所属：業務を行っていただく主な学部、大学院は理工学術院です。所属（主本属）は、本学の取扱い上、基幹理工学部情報理工学科となります。採用年月日：2025年9月1日、またはそれ以降のできるだけ早い時期業務内容： (1) 募集領域に関する科目などの授業担当、その他教育に関する業務情報理工学科における講義、実験科目、および情報理工・情報通信専攻における講義科目等を複数担当していただきます。なお、相談の上、応募者の研究内容と直接的に関連しない科目もご担当いただく可能性があります。また、これらは日本語による場合も英語による場合もあります。 (2) 独立した研究室としての個別研究活動、組織的研究活動への参画、その他研究に関する業務 (3) 教授会や各種委員会への参画、入試業務、その他大学運営に関する業務 (4) 社会活動への参画、その他社会貢献に関する業務 (5) その他本学規程に定めた業務就業場所：主として早稲田大学西早稲田キャンパス、早稲田大学各キャンパス、他勤務時間：所定労働日および勤務時間（始業・終業時刻、休憩時間）等は、本学規程によります。なお、専門業務型裁量労働制みなし労働 1 日8時間を適用し、研究業務の性質上、業務遂行の手段および時間配分の決定等については本人の裁量に委ねるものとします。休日：土曜日、日曜日、年末年始、国民の祝日、国民の祝日の一部に授業を実施することにより設ける臨時の休業日および大学創立記念日とします。ただし、大学があらかじめ授業を実施すると定めた日を除きます。休暇：労働基準法等法令に定められた休暇および，大学が特に定めた日とします。給与：本学規程によります。諸手当・通勤費：本学規程によります。退職金：本学規程によります。社会保険・労働保険：厚生年金、健康保険、労災保険、雇用保険にご加入いただきます。応募資格：以下のすべての条件を満たす方。 (1) 博士の学位を有する方 (2) 日本語に加えて英語による学部・大学院での講義および研究指導ができること。海外留学もしくは海外勤務経験を持つことが望ましい。特に日本語を母国語としない場合は、日本語能力試験JLPTでN1認定程度以上の日本語力を持つこと。 (3) 学科、専攻等の運営に積極的に携われる方応募方法：応募書類はすべて電子的に提出してください（郵送による送付は受け付けません）。「応募書類」に指定の書類(1)から(6)を1つのPDFファイルとしてまとめてください。このPDFファイルと、(7)エントリーデータファイルを合わせて1つのzipファイルとし、zipファイルのみ送付してください。ファイル名はいずれもローマ字氏名としてください。（例︓Waseda_Hanako.pdf Waseda_Hanako.xlsx Waseda_Hanako.zip） zip ファイルを、JREC-IN Portal サイトから「Web 応募」によりご提出ください。 https://jrecin.jst.go.jp/seek/SeekJorDetail?&id=D124071009 ※JREC-INのWeb応募では、ファイルサイズの制限 (20MB) にご注意ください。制限内に収めるのが困難である場合は、問い合わせ先のメールアドレス宛にご相談ください。応募書類： (1) 履歴書（指定フォーマットをお使いください） (2) 研究教育業績（指定フォーマットをお使いください） (3) 主要論文3編以内を順位付けすると共に、主要論文に選んだ理由を書いてください。（フリーフォーマット） (4) 上記で挙げた主要論文3編以内の電子ファイル (5) 着任後の抱負（フリーフォーマット）：任用された場合の教育活動計画、研究活動に関する展望や考え方などを記載してください。 (6) 応募者を良く知る方からの推薦状2通以上（推薦状にはご所属、電話番号、電子メールアドレスを記載頂くよう、依頼してください）。応募時に推薦状が揃わない場合は、応募者について問い合わせ可能な方2名以上の氏名と所属、連絡先（住所、電話番号、電子メールアドレス）を記載してください。 (7) エントリーデータファイル（指定フォーマット） ※追加書類の提出を求めることがあります。 ※応募書類等の個人情報につきましては、本学の規程に従って適切に管理し、教員採用のための選考以外に使用することはありません。選考終了後、責任をもって処分します。応募期限：2024年11月17日（日）23時日本時間（必着） ※電子データの提出のみ受け付けます。 ※期限後の提出は、理由に関わらず認めません。選考方法：選考は書類選考と面接選考（模擬講義を含む）により実施します（面接選考は書類選考を通過した方のみ）。面接選考実施日は2月7日（金）あるいは2月8日（土）を予定していますが（どちらか1日となります）、応募者の都合等に合わせて変更する可能性があります。 ※適任者がいない場合、本公募での採用を見送る場合もあります。 ※面接の日時等は、対象者のみ別途通知します。 ※面接等にかかる交通費・宿泊費等は応募者自身の自己負担とします。選考結果通知：書類選考結果：2024年12月下旬（予定）面接選考結果：2025年3月下旬（予定）最終選考結果通知：2025年7月（予定）通知方法：選考結果は、エントリーデータファイルに記載された電子メールアドレス宛に通知します。 ※選考内容・結果に対するお問合せには応じることができません。その他：・面接選考は対面を想定していますが、海外在住者や国内遠隔地在住者については、オンラインで行う選択も可能とします。・出産・育児・介護による研究中断期間に対して考慮を希望される場合、履歴書に記載して下さい。・早稲田大学は、教員採用・昇進の人事審査において、性別、障がい、性的指向・性自認、国籍、エスニシティ、信条、年齢を理由とするいかなる差別も行わないことを申し合わせております。今回の女性に限定した公募は、「男女雇用機会均等法」第 8 条（女性労働者に係る措置に関する特例）の規定により、当機関の女性教員比が低い現状を積極的に改善するための経過措置として実施するものです。問い合わせ先：〒169-8555 東京都新宿区大久保3-4-1 早稲田大学基幹理工学部情報理工学科学科主任清水佳奈 E-mail：shimizu.kana-ａｔ-waseda.jp <http://shimizu.kana-at-waseda.jp> （-ａｔ-を@に置き換えてください）

1 0

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

08 Jul '24

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

1 0

日本ソフトウェア科学会第41回大会発表募集
by Tsuneyasu KOMIYA 04 Jul '24

04 Jul '24

皆様， # 重複してお受取になった場合はご容赦ください．電気通信大学の小宮と申します．日本ソフトウェア科学会第41回大会の発表募集をご案内させていただきます． # 今年の大会は，対面開催を予定しているとのことです．ご発表をご検討いただけましたら幸いです． ---------------------------------------------------------------------- 日本ソフトウェア科学会第41回大会発表募集 - 開催日時： - 併設イベント：2024年9月9日（月） - 大会：2024年9月10日（火）～12日（木） - 会場：立命館大学大阪いばらきキャンパス - Webページ URL：https://jssst2024.wordpress.com/cfp/ - 登壇発表申込締切：2024年7月26日（金） - 講演論文原稿締切：2024年8月9日（金） - デモ・ポスター発表：2024年8月9日（金） # ご発表のお誘い登壇発表とデモ・ポスター発表の場が用意されています．登壇発表は一般論文もソフトウェア論文も歓迎します．萌芽的な研究の発表の場としてもご検討ください．講演論文の共著者に会員が含まれていれば非会員でも登壇発表できます．未来のソフトウェアとそれを支えるソフトウェア科学に関する活発な議論を期待します．今年の大会は，対面開催を予定しております． # ご注意今年の大会では、発表および聴講のためのオンライン配信の準備予定はありません # 締切 - 登壇発表申込締切：2024年7月26日（金） - 講演論文原稿締切：2024年8月9日（金） - デモ・ポスター発表：2024年8月9日（金） # トラックおよびセッション今大会では以下のトラックおよびセッションを設けます． - 登壇発表トラック - 一般セッション：ソフトウェア科学全般についての発表の場です．一昨年度まで「研究会セッション」での発表として募集していた論文はこのセッションでの発表として募集します．プログラムはトピックに応じて編成する予定です． - ソフトウェア論文セッション：先進的なアイデアを実現したソフトウェアの成果発表の場です．ソフトウェア論文特集号への投稿を前提としたメンタリングを受けることもできます．詳細はホームページをご覧ください． - デモ・ポスター発表トラック研究アイデアやそれを実現したソフトウェアの紹介と議論の場です．講演論文なしで発表することができます． # 発表申し込み要領 - 講演論文の著者 (デモ・ポスターセッションの場合は発表者) に正会員，学生会員または名誉会員が含まれている必要があります．ただし，発表申込時に入会手続中の場合も含みます．会場で登壇する人，会場で説明を行う人は非会員でも構いません． - 講演論文は EasyChair システム (https://easychair.org/my/conference?conf=jssst2024) を使って PDF ファイルで提出してください．詳しい講演論文作成要領は https://jssst2024.wordpress.com/submission/ をご参照ください． - 講演論文を収録した講演論文集は学会ウェブサイトで大会終了後に公開予定です． # 授賞特に優秀な登壇発表を行った本会会員には「高橋奨励賞」が授与されます．また優秀な登壇発表を行った学生には「学生奨励賞」が，聴衆から多くの支持を集めた登壇発表を行った発表者には「優秀発表賞」が授与されます．優秀なデモ・ポスター発表には「優秀デモ・ポスター賞」が授与されます． # 学会誌への同時投稿講演論文は通常論文あるいはレター論文として学会誌に同時投稿できます．大会発表で得られたコメントを反映した上での大会後投稿も可能です．詳細は，ホームページをご覧ください． # お問合せ先 jssst2024 at fun.ac.jp このアドレスへの特定電子メール（広告・宣伝メール）の送信は拒否いたします． ----------------------------------------------------------------------

1 0

『第2回若手による数理論理学研究集会』のご連絡
by 西村祐輝 03 Jul '24

03 Jul '24

logic-ml の皆様、『第2回若手による数理論理学研究集会』運営の西村です。本研究集会について、いくつか告知をいたします。 1. 旅費支援お問い合わせフォームを作成しました。「旅費支援を申し込みたい」「旅費支援によっては参加したい」という方は、こちらのフォームに記入をお願いいたします。事務処理の都合上、締め切りは参加登録フォームより早く、【7/15】とさせていただきます。すでに参加登録フォームにて旅費支援についてお問い合わせをいただいた方も、お手数ですが再度お問い合わせフォームにご記入いただければと思います。 2. 懇親会の詳細が確定しました。 - 日時：8月8日 19:00-21:00 - 会場：神奈川大学 1号館 806室 - 参加費：4,500円懇親会参加の締め切りは、参加締切と同じく 7/22 です。 3. 今回の研究集会では、発表される方に予稿集への寄稿をお願いしています（原稿の提出は集会後を予定）。集会後の予稿集は、神奈川大情報学研究所からオンラインで公開される予定です。ご承知おきください。また、対外的にアピールできる発表実績ともなりますので、とくに学生の方々は積極的に検討していただけると幸いです。 4. アルバイトの参加条件を、「学部生のみ」から「学部生・修士課程学生」に変更しました。修士課程学生の方で、当日の運営を手伝っていただける方は、アルバイト申し込みフォームかに必要事項を記入してください。各種フォームや会の詳細については、ウェブサイトをご覧ください。 https://sites.google.com/view/yorukai-2nd/%E3%83%9B%E3%83%BC%E3%83%A0 発表枠、参加枠ともに、十分に空きがございます。みなさまのご参加をお待ちしています。 -- 西村祐輝東京工業大学情報理工学院数理・計算科学系 mail: nishimura.y.as(a)m.titech.ac.jp

1 0

SLACS 2024（8月21日-22日）講演・参加募集のお知らせ
by Kazuyuki Asada 02 Jul '24

02 Jul '24

皆様，（重複して受け取られた場合はご容赦ください．）第41回記号論理と情報科学研究集会（SLACS 2024）幹事の東北大学の浅田です． SLACS 2024は，2024年8月21日（水）～22日（木）に，東北大学電気通信研究所にて現地開催いたします．発表・参加のご検討のほど，どうぞよろしくお願いいたします． ==== SLACS 2024 開催要領 ==== 詳細：https://sites.google.com/view/slacs-2024 日程：2024年8月21日（水）～22日（木）の二日間形式：現地開催会場：東北大学電気通信研究所本館 1階 M153室（〒980-0812 宮城県仙台市青葉区片平２丁目１−１）講演申込： https://forms.gle/ZYdY1yV9RoZn1g649 参加申込： https://forms.gle/LnLKNrW1KNt5UUgB6 費用：参加費無料（懇親会費は別途徴収）幹事：浅田和之（東北大学電気通信研究所, E-mail: asada(a)riec.tohoku.ac.jp) ============================= 講演申し込み期限は 2024年8月14日（水）といたしますが，発表する意思がある方はお早めにお申し込みいただけると幸いです．研究集会への参加申し込みは開催当日まで受け付けます．以上，奮ってご参加ください．

1 0

第7回セキュアシステムのためのソフトウェア、アーキテクチャ、理論に関するワークショップ参加募集
by Taro Sekiyama 18 Jun '24

18 Jun '24

皆様 (複数お受け取りの場合はご容赦ください) 国立情報学研究所の関山です。 7月1日に開催される「第7回セキュアシステムのためのソフトウェア、アーキテクチャ、理論に関するワークショップ」の参加募集のご案内です。第7回の開催情報は以下の通りです。詳しくはワークショップの案内ページ：https://sc-sys.github.io/ もあわせてご覧ください。講演内容：コンフィデンシャル・コンピューティングの基盤技術と期待される TEE (Trusted Execution Environment) に関連する3つの講演を予定しています。 1. "CTR: Checkpoint, Transfer, and Restore for Secure Enclaves" Yoshimichi Nakatsuka (ETH Zurich) 2. "TDOS: Trustworthy Heterogeneous Disaggregated Architectures" Atsushi Koshiba (Technical University of Munich) 3. "OP-TEEの利用事例：OP-TEEを用いたIoTのための安全な階層鍵管理機構" 竹房あつ子 (NII) 開催日時：7月1日 14:00〜17:00 開催場所：早稲田大学グリーン・コンピューティング・システム研究開発センター (40号館) 1階プレゼンテーションルーム (https://www.waseda.jp/inst/gcs/access/) 参加方法： Google form https://forms.gle/G8jYDktBZJRYTnYk7 から申し込み (登録締切は 6/28(金) 17:00 です) ワークショップについて：本ワークショップ「セキュアシステムのためのソフトウェア、アーキテクチャ、理論に関するワークショップ (SATSS)」は、新しい（特にセキュアな）計算機システムに関する原理を理論研究と共に計算機ハードウェアからソフトウェアのレイヤまで研究・開発するために必要な知識の獲得と議論の場を提供することを目的として開催しています。また議論を大事にするという観点から、現地参加を推奨しています。(リモート参加も可能です）それでは皆様の参加をお待ち申し上げます。また、お知り合いの方で興味のございます方がいらっしゃいましたら周知いただけますと幸いです。 -- 関山太朗国立情報学研究所 sekiyama(a)nii.ac.jp

1 0

『若手による数理論理学研究集会』参加者募集
by 西村祐輝 13 Jun '24

13 Jun '24

logic-ml の皆様、東京工業大学の西村です。先日告知しました『若手による数理論理学研究集会』について、参加者の募集を開始しましたので告知いたします。詳細については、こちらの公式ページをご覧ください。 https://sites.google.com/view/yorukai-2nd また、学部生以下の方を対象に、当日運営の手伝いをしていただくアルバイトを募集しています。こちらも公式サイトに詳細がありますので、ぜひご覧ください。若手の方々の出席をお待ちしています。また、先生方におかれましては、研究室の学生のみなさんや、ご興味のある学生さんに周知していただけると幸いです。 -- 西村祐輝東京工業大学情報理工学院数理・計算科学系 mail: nishimura.y.as(a)m.titech.ac.jp

1 0

東北大ロジックセミナーのご案内
by 竹田侑人 07 Jun '24

07 Jun '24

皆様，東北大学の竹田です．以下の通りセミナーを開催いたしますのでご案内いたします． https://sites.google.com/view/sendai-logic/ 日時：6月14日(金)15:00〜場所：東北大学理学研究科合同A棟801号室 (zoom配信あり) 講演者：中田哲 (京都大学数理解析研究所) 題目準古典的算術における冠頭標準形定理と部分トポス構造概要論理式の形に関する冠頭標準形定理は、直観主義論理上では一般には成り立たないことがよく知られている。とりわけ準古典的算術における冠頭標準形定理の成否については、藤原氏と倉橋氏により精密に調べられている[1]。彼らは証明論的議論に基づき次の否定的結果を示していた: HA + Sigma_1-DNEにおいてSigma_1に関する冠頭標準形定理は成立しない。本講演では、この結果のトポス理論的議論に基づく別証明を与え、その一般化について考察する。 [1] Makoto Fujiwara and Taishi Kurahashi. Prenex normal form theorems in semi-classical arithmetic. Journal of Symbolic Logic, 86(3):1124--1153, 2021. オンライン参加を希望される方は竹田(yuto.takeda.t8(a)dc.tohoku.ac.xn--jp)-u63baam6azav5czbevh0gij9rvoja5sb4j6736j2rvgn34dhb1b どうぞよろしくお願いいたします．竹田侑人 yuto.takeda.t8(a)dc.tohoku.ac.jp

1 0

准教授（鹿児島大学）公募
by Hitoshi Furusawa 06 Jun '24

06 Jun '24

logic-ml の皆さま鹿児島大学の古澤と申します。本学学術研究院理工学域理学系では、以下の公募を行っております。募集人員：准教授１名（任期の定めなし）所　　属：鹿児島大学学術研究院理工学域理学系（理学部理学科／数理情報科学プログラム担当）専門分野：情報科学または情報科学に関連する数理科学着任時期：令和７年４月１日応募締切：令和６年８月２０日（火）必着詳細につきましては下記のURLをご覧ください。 https://jrecin.jst.go.jp/seek/SeekJorDetail?id=D124060260 https://www.kagoshima-u.ac.jp//about/saiyou.html ご興味をお持ちの方がいらっしゃいましたら応募をご検討ください。また、お近くに適任の方がいらっしゃいましたらお勧めいただけますと幸いです。 ----- 鹿児島大学古澤仁

1 0

教員の公募
by AOKI Kunimasa 04 Jun '24

04 Jun '24

logic-ml の皆様水産大学校にいる青木と申します。水産大学校では情報科学分野で教員の公募を行なっております。 https://www.fish-u.ac.jp/shokuin/files/r5-7.pdf お近くに興味のお有りの方がいらっしゃいましたらご紹介いただけると幸いです。よろしくお願いいたします。 — AOKI Kunimasa

1 0

【参加案内】情報処理学会第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

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 24 May '24

24 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 22 May '24

22 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 西村祐輝 22 May '24

22 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

東北大ロジックセミナーのご案内
by yuto.takeda.t8＠dc.tohoku.ac.jp 21 May '24

21 May '24

皆様，東北大学の竹田です．以下の通りセミナーを開催いたしますのでご案内いたします． https://sites.google.com/view/sendai-logic/ 日時：5月24日(金)15:00〜場所：東北大学理学研究科合同A棟801号室 (zoom配信あり) 講演者：鈴木悠大 (国立沖縄高専) 題目　 On the Pi^1_2, Sigma^1_2 and Boole(Pi^1_2) sentences provable from Pi^1_1-CA_0 概要　In [1], we introduced some characterizations of the set of Pi^1_2 sentences provable from Pi^1_1-CA_0 and a hierarchy dividing it. For a detailed study of the properties of this hierarchy, it was important to focus on the statements of the form [every coded beta-model satisfies sigma] for some specific sentences sigma. In this talk, we summarize a part of [1]. Then we give a characterization of the set of Sigma^1_2 or Boole(Pi^1_2) sentences provable from Pi^1_1-CA_0 by statements of the form [every coded beta-model satisfies sigma]. Here, Boole(Pi^1_2) is the class of formulas generated by disjunction, conjunction and negation starting from Pi^1_2. This is joint work with J. Aguilera and K. Yokoyama. [1] Suzuki, Y., & Yokoyama, K. (2024). On the $\Pi^ 1_2 $ consequences of $\Pi^ 1_1 $-$\mathsf {CA} _0$. arXiv preprint arXiv:2402.07136. オンライン参加を希望される方は竹田(yuto.takeda.t8(a)dc.tohoku.ac.xn--jp)-u63baam6azav5czbevh0gij9rvoja5sb4j6736j2rvgn34dhb1b どうぞよろしくお願いいたします．竹田侑人 yuto.takeda.t8(a)dc.tohoku.ac.jp

1 0

事務連絡: moderation について
by Atsushi Igarashi 16 May '24

16 May '24

logic-ml のみなさま， logic-ml 管理人の五十嵐です．本MLは，投稿は moderation が必要な状態で登録されます．これまで， moderation 待ちのメールがあることが管理人のところに通知されていたのですが，昨年末に mailman3 に切り替えて以来，通知がうまく受け取れないでおります．ついでがあった時に moderation 待ちがないか見るのですが，今回は間があいてしまってひと月も待ちになっておりました．投稿者の方には大変ご迷惑をおかけし申し訳ありません．投稿しても流れてないぞ，と思った時は遠慮なく，五十嵐までご連絡ください．通知が受け取れない問題など根本的な解決をしたいのですが時間が取れないでおります．ベストエフォート運営ということでご理解ください．一切合財引受けていただける方がいらっしゃると一番よいのですが… -- 五十嵐淳 (IGARASHI Atsushi) E-mail: igarashi(a)kuis.kyoto-u.ac.jp url: http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/

1 1

准教授の公募
by SAKAI Hiroshi 15 May '24

15 May '24

皆様：東京大学の酒井です．東京大学数理科学研究科で准教授の公募をしております． https://www.ms.u-tokyo.ac.jp/news/kobojunkyoju20240630j.pdf ご興味のある方はご応募ください．よろしくお願いいたします．酒井拓史

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml