Logic-ml

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

1792 discussions

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

← Newer
1
...
4
5
6
7
8
9
10
...
180
Older →

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml