Logic-ml December 2017

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

9 participants
12 discussions

セミナー案内
by KASHIMA Ryo 06 Sep '19

06 Sep '19

数理論理学セミナーのお知らせ東工大大岡山キャンパスで定期的に開催しているセミナー（普段はlogic-mlには流していません）の特別版を　　９月８日（金）と１５日（金）に開催します。以下に「話者（所属）題目」の一覧を載せました。どなたでも参加できますが、普段のセミナー案内を受け取っていない方の場合はご一報ください。 ----- 鹿島亮東京工業大学情報理工学院数理・計算科学系 kashima(a)is.titech.ac.jp ＝＝＝＝＝＝＝＝【８日（金）】西牟田祐樹（慶應大）一般化乗法的論理結合子のシーケント化定理とdecomposabilityについて藤原誠（早大）Bar induction and restricted classical logic 武原直紀（東工大）直観主義二階命題論理と論理式完備ハイティング代数について松田直祐（神奈川大）Curry's last problemへの弱い解答中村誠希（東工大）関係Kleene代数におけるatomic negationについて（仮題）新屋良磨（東大）論文紹介 Cyclic Arithmetic Is Equivalent to Peano Arithmetic 【１５日（金）】池上貴大（東工大）様相命題論理におけるツリーシークエント計算（仮題）河野友亮（東工大）Quantum logic の implication algebra と restricted negation について（仮題）鹿島亮（東工大）２階の関数記号を持つ１階述語論理について山﨑紗紀子（首都大）ゲーデル・マッキンゼイ・タルスキの定理の証明論的証明ー後件複数な直観主義論理のG3-style sequent calculus を用いてー大森仁（京大）Jaskowskiのdiscussive logicの周辺金沢誠（国立情報学研）Context-Free Languages with Finite Context and Kernel Properties 高橋正子 Grzegorczyk階層について＝＝＝＝以上＝＝＝＝

1 8

特任研究員の募集
by koba＠kb.is.s.u-tokyo.ac.jp 28 May '18

28 May '18

＃複数受け取られましたらご容赦ください．東京大学の小林と申します．当研究室では現在，高階モデル検査（高階再帰スキームのモデル検査）とそのプログラム検証などへの応用をテーマとした研究を精力的に進めており，プロジェクトに携わる特任研究員を探しております．身近にご興味のある方がいらっしゃいましたら，10月20日までに小林 (koba(a)is.s.u-tokyo.ac.jp) までメールでお知らせいただければ幸いです。その際、できれば略歴および論文リスト（フォーマット自由）もメールに添えるかまたは郵送でお送りください。（後日、さらに詳細な資料をお願いする可能性があります）．募集の条件は概ね以下のとおりです。 ================ 着任時期：2018年4月（数ヵ月の前後は応相談）任期：年度単位の更新で、業績により最長2020年3月まで延長可能給与：月額38～45万円　　（大学の規定および本人の実績による．細かい条件は応相談.）研究テーマ：高階モデル検査（高階再帰スキームのモデル検査）および、そのプログラム検証やデータ圧縮、知識発見などへの応用。高階モデル検査については，プロジェクトのページ　　　http://www-kb.is.s.u-tokyo.ac.jp/~koba/hmc/ および下の参考文献をご覧ください。　　本プロジェクトは科学研究費補助金基盤研究(S)：　　　課題名：高階モデル検査の深化と発展　　　研究代表者：小林直樹（東京大学）　　　研究分担者：五十嵐淳（京都大学）、篠原歩（東北大学）　　の支援をいただいており、その補助金で研究員を雇用する予定です。条件： - 着任時に博士号を取得していること - 理論計算機科学全般に明るいこと． - 以下の中の１つ以上のトピックに詳しくプログラミング能力が高いか、　　　２つ以上のトピックに詳しいことモデル検査（特にソフトウェアモデル検査）型システムプログラム意味論プログラム解析・検証・変換オートマトンと形式言語理論自動定理証明　　　　　計算量理論 (可逆)データ圧縮技術自然言語処理ゲノムデータ解析問い合わせ先：　　小林直樹　　東京大学大学院情報理工学系研究科コンピュータ科学専攻　　〒113-0033 東京都文京区本郷7-3-1 　　Phone: 03-5841-4124 　　Fax: 03-5841-4114 　　email: koba(a)is.s.u-tokyo.ac.jp 参考文献の抜粋 ------------- 高階モデル検査の概要： Naoki Kobayashi, "Model Checking Higher-Order Programs", Journal of the ACM, 60(3), 2013. Naoki Kobayashi, "Higher-Order Model Checking: From Theory to Practice", Invited paper in Proceedings of LICS 2011. (A very brief survery of the field) 高階モデル検査/高階言語の理論： Naoki Kobayashi, Etienne Lozes, Florian Bruse, "On the relationship between higher-order recursion schemes and higher-order fixpoint logic", POPL 2017, pp.246-259, 2017 Kazuyuki Asada, Naoki Kobayashi, "Pumping Lemma for Higher-order Languages", ICALP 2017, 97:1-97:14, 2017. Ryoma Sinya, Kazuyuki Asada, Naoki Kobayashi, Takeshi Tsukada, "Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence", FoSSaCS 2017, pp.53-68 プログラム検証への応用: Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno, "Predicate Abstraction and CEGAR for Higher-Order Model Checking", Proceedings of PLDI 2011, pp.222-233, 2011. Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno, "Temporal verification of higher-order functional programs", POPL 2016, pp.57-68 データ圧縮への応用: Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, Kazuya Yaguchi, "Functional Programs as Compressed Data", Higher-Order and Symbolic Computation, 2(1), pp.39-84, 2012.

1 1

組合せ論・モデル理論セミナー(2018.1.15)
by Hirotaka Kikyo 28 Dec '17

28 Dec '17

組合せ論・モデル理論セミナーを下記のように開催いたしますので、ご案内さしあげます。よろしくお願い致します。 -- ・日時: 2018年1月15日(月) 14:30～・場所: 神戸大学六甲台第2 <https://maps.google.com/?q=%E5%85%AD%E7%94%B2%E5%8F%B0%E7%AC%AC2&entry=gmai…>キャンパス自然科学総合研究棟3号館 421室 (予定) ・講演者・プログラム: 14:30-16:00 坪井明人氏 (筑波大学,モデル理論) "A proof of Hales-Jewett theorem using a nonstandard method" 16:15-17:45 Qing Xiang 氏 (University of Delaware,組合せ論) "Applications of Linear Algebraic Methods in Combinatorics and Finite Geometry" ・HP: https://sites.google.com/site/kcmseminar/ ・世話人岡部峻典 (神戸大学) 桔梗宏孝 (神戸大学) 佐竹翔平 (神戸大学) 澤正憲 (神戸大学) --

1 0

WIAS Top Runners’ Lecture Collection “Proof Theory and Computation"(2018年3月16, 17日)のご案内
by Makoto Fujiwara 27 Dec '17

27 Dec '17

皆様早稲田大学の藤原誠です．以下の通り，3月16日-17日(日本数学会2018年度年会@東京大学の直前)に早稲田大学早稲田キャンパスにてLMU MunchenのHelmut Schwichtenberg先生にチュートリアル講演をしていただく予定です．日程：2018年3月16日(金)16:00-18:00, 3月17日(土)16:00-18:00 場所：早稲田大学早稲田キャンパス(教室未定) 講演者：Helmut Schwichtenberg (LMU Munchen, Emeritus Professor) 講演題目：Proof Theory and Computation 詳細につきましては日程が近づきましたら再度ご案内をさせていただきます．どうぞよろしくお願いいたします． ============================================ 藤原誠 (Makoto Fujiwara) 早稲田大学高等研究所 (Waseda Institute for Advanced Study, Waseda University) E-mail: makoto_fujiwara(a)aoni.waseda.jp ============================================

1 0

1月19日20日:日仏“論理と数学の哲学：証明と計算の哲学と歴史”ワークショップ(慶応大)
by Mitsu Okada 25 Dec '17

25 Dec '17

２０１８年１月１９日・２０日に開催される次のワークショップを案内させていただきます。慶応大文学部哲学専攻　岡田光弘 -------- 日仏“論理と数学の哲学：証明と計算の哲学・歴史”ワークショップ(1/19-20, Keio U) Workshop on Philosophy and History of Proofs and Computation, Jan.19-20,2018 (https://abelard.flet.keio.ac.jp/seminar/frjp18jan.html for updated information) 論理と数学の哲学及び歴史研究に関する日仏ワークショップを開催します。毎年このワークショップシリーズでは、論証・証明について、論理学・哲学・計算論的観点から議論し、本分野の日仏連携・協力を進めています。フランスから４人、国内から３人の招待講演者を迎えて本年度の会を開催します。(今年度は特にユークリッド原論の歴史・言語分析・証明の研究者３人をお呼びしています。) 日時:Jan 19th Friday-20th Saturday, 2018 / 2018年1月19日(金)-20日(土) 10:00 - 18:00場所:Distance Learning Room (B4F), South Building, Mita Campus of Keio University / 慶應義塾大学三田キャンパス南館地下4階ディスタンスラーニングルーム https://www.keio.ac.jp/en/maps/ Building #12 on this map. / キャンパスマップ12番の建物です。プログラムは「ユークリッド原論の歴史・言語分析・哲学」「現代論理学史とオントロー」「論理と証明の哲学」「計算と証明」などのセッションから構成されます。プログラム詳細については近日中に次のページに掲載します。 https://abelard.flet.keio.ac.jp/seminar/frjp18jan.html 招待講演者と講演テーマ/ Guest Speakers and Titles Andrew Arana (Univ. Paris-1 and IHPST)Logical Purity and Normalization .Jean-Baptiste Joinet (Univ. Lyon-3 and Inst. Jean Cavaillès (ENS-Paris)) Logic and ontology .Marco Panza (Univ. Paris-1 and IHPST)What Universality Could Have Been for Euclid .斎藤憲Ken Saito　(Osaka Prefecture Univ.)Syntax Analysis of the Whole Text of Euclid’s Elements .Nathan Camillo Sidoli (Waseda Univ.)Euclid’s Postulates and Problems .Pierre Wagner (Univ. Paris-1 and IHPST)Logical Commitment 伊藤遼Ryo Ito (Univ. of Kyoto)The Unity of the Proposition and Russell's Theories of Truth Japanese group speakers 秋吉亮太Ryota Akiyoshi (Waseda Univ.)Proof-Theoretic Studies of Parameter-Free Subsystems of Girard's System F (tentative) Daniel Said Monteiro (Univ. Paris 7 and Keio Univ.)Explaining the movements of qi: Nishikawa Joken (1648-1724) and the understanding of extraordinary phenomena in early modern Japan 岡田光弘Mitsuhiro Okada (Keio Univ.)　Norm, Commitment and Normalization of Proof (tentative) .小関健太郎Kentaro Ozeki (Keio Univ.)Meinongian Incomplete Objects and Negation .西牟田祐樹Yuki Nishimuta (Keio Univ.)Non-decomposability Preservation of Generalized Connectives and Cut Elimination (preliminary report) そのほかAnd others to be announced. ---------------------------------------------------------------------------------------------------------- なおこの集会とは別に、１月２５日に、Andre Scedrov、金沢誠/Makoto Kanazawa、Jean-Baptiste Joinetの３氏をお招きして、Lambek CalculusとLinear Logicに関する集会を開催する予定です。追ってお知らせします。 ------------------------------------------------------- ----------------------------------------------- 共催慶應義塾大学論理と感性のグローバル研究センター及び•次世代研究推進プロジェクト CNRS(フランス) 連絡先慶應義塾大学文学部岡田光弘研究室東京都港区三田２−１５−４５ Email: logic [AT] abelard.flet.keio.ac.jp https://abelard.flet.keio.ac.jp/seminar/frjp18jan.html

1 0

CFP: SetVR 2018 @ Diagrams 2018
by Yuri Sato 16 Dec '17

16 Dec '17

Logic MLの皆様、国際ワークショップSetVR 2018の論文募集についてご案内致します。 **************************************************************************** Call for Papers SetVR 2018: International Workshop on Set Visualization and Reasoning 2018 https://sites.google.com/site/setvr2kn/current-workshop Conference dates: 18th-22nd June, 2018 Location: Edinburgh, UK Deadline for submission: 5th February, 2018 **************************************************************************** SetVR 2018 will be the 6th meeting, with the first one held in 2004, previously called the Euler Diagrams Workshop. It aims to promote theoretical, empirical, applied research on visualization and diagrammatic reasoning, especially, about sets (set-theoretical and grouped data). SetVR 2018 welcomes submissions of types: full papers (16 pages) and short papers (8 pages; at least 5 pages). Accepted papers are expected to be published on-line by CEUR Workshop Proceedings (CEUR-WS.org). SetVR 2018 will run as part of Diagrams 2018 conference, which will be held from June 18th to 22nd in 2018, and is expected to occupy one day during this period. http://www.diagrams-conference.org/2018/ Topics include (but not limited to): • Information Visualization: diagram/graph drawing and layout, data visualization, ontology visualization, human-computer interaction • Diagrammatic Logic: formalization, inference system, expressiveness, decidability, computational complexity, automated reasoning, history of notation • Cognitive Science: efficacy evaluation, cognitive process, cognitive model, educational outcome • Application of Diagrams: visual modeling, real world reasoning, ontology engineering, data exploration Organizers Yuri Sato (University of Brighton, UK) Zohreh Shams (University of Cambridge, UK) Program Committee Bilal Alsallakh (Bosch Research and Technology Center, USA) Jim Burton (University of Brighton, UK) Peter Chapman (Edinburgh Napier University, UK) Renata De Freitas (Universidade Federal Fluminense, Brasil) Mateja Jamnik (University of Cambridge, UK) Sven Linker (University of Liverpool, UK) Luana Micallef (Helsinki Institute for Information Technology HIIT, Finland) Peter Rodgers (University of Kent, UK) Gem Stapleton (University of Brighton, UK)

1 0

[2nd CFP] Bx 2018: 7th International Workshop on Bidirectional Transformations
by Kazutaka Matsuda 15 Dec '17

15 Dec '17

皆様，東北大学の松田です．来たる2018年4月10日に，<Programming> 2018に併設して開催されるワークショップ， Bx 2018 の論文募集の案内を再度お送りいたします．前回お送りした投稿〆切日時が誤っておりましたことをお詫びいたします．誤 Feb. 18, 2018 正 Feb. 19, 2018 Bx 2018では，”Experience Report"という投稿カテゴリを新設いたしました．もしlens等の双方向変換システムを研究/教育/開発プロジェクト等に使用されたことがある方がいらっしゃいましたら，ぜひともその経験の投稿をご検討くださいませ．その他のカテゴリについても，ご投稿を検討いただければ幸いです． ---------------------------------------------------------------------- SECOND CALL FOR PAPERS ======================= Bx 2018: 7th International Workshop on Bidirectional Transformations Nice, France (co-located with <Programming> 2018) https://2018.programming-conference.org/track/bx-2018-papers ---------------------------------------------------------------------- Bidirectional transformations (bx) are a mechanism for maintaining the consistency of at least two related sources of information. Such sources can be relational databases, software models and code, or any other document following standard or ad-hoc formats. Bx are an emerging topic in a wide range of research areas, with prominent presence at top conferences in several different fields (namely databases, programming languages, software engineering, and graph transformation), but with results in one field often getting limited exposure in the others. Bx 2018 is a dedicated venue for bx in all relevant fields, and is part of a workshop series that was created in order to promote cross-disciplinary research and awareness in the area. As such, since its beginning in 2012, the workshop has rotated between venues in different fields. IMPORTANT DATES --------------- - Paper submission: Jan. 19, 2018 - Author notification: Feb. 17, 2018 - Workshop: Apr. 10, 2018 AIM & TOPICS ------------ The aim of the workshop is to bring together researchers and practitioners, established and new, interested in bx from different perspectives, including but not limited to: - bidirectional programming languages and frameworks - data and model synchronization - view updating - inter-model consistency analysis and repair - data/schema (or model/metamodel) co-evolution - coupled software/model transformations - inversion of transformations and data exchange mappings - domain-specific languages for bx - analysis and classification of requirements for bx - bridging the gap between formal concepts and application scenarios - analysis of efficiency of transformation algorithms and benchmarks - survey and comparison of bx technologies - case studies and tool support PAPER CATEGORIES ---------------- The BX 2018 program committee considers five categories of submissions: - Full Research Papers (up to 10 pages) * in-depth presentations of novel concepts and results * applications of bx to new domains * survey papers providing novel comparisons between existing bx technologies and approaches case studies - Tool Papers (up to 6 pages) * guideline papers presenting best practices for employing a specific bx approach (with a specific tool) * presentation of new tools or substantial improvements to existing ones * qualitative and/or quantitative comparisons of applying different bx approaches and tools - Experience Report (up to 4 pages) * sharing experiences and lessons learned with bx tools/frameworks/languages * how bx is used in (research/industrial/educational) projects - Extended Abstracts (up to 3 pages) * work in progress * small focused contributions * position papers and research perspectives * critical questions and challenges for bx - Talk Proposals (up to 2 pages) * proposed lectures about topics of interest for bx * existing work representing relevant contributions for bx * promising contributions that are not mature enough to be proposed as papers of the other categories All papers are expected to be self-contained and well-written. Tool papers are not expected to present novel scientific results, but to document artifacts of interest and share bx experience/best practices with the community. Experience papers are expected to report on lessons learnt from applying bx approaches, languages, tools and theories to practical application case studies. Extended abstracts should primarily provoke interesting discussion at the workshop and will not be held to the same standard of maturity as regular papers. Talk proposals are expected to present works of particular interest for the community and that are worth a talk slot at the workshop. We strongly encourage authors to ensure that any (variants of) examples are present in the bx example repository at the time of submission, and for tool papers, to allow for reproducibility with minimal effort, either via a virtual machine (e.g. via Share - http://share20.eu) or a dedicated website with relevant artifacts and tool access. All papers will be peer-reviewed by at least three members of the program committee. PROCEEDINGS ----------- The workshop proceedings, including all accepted papers (except talk proposals), will be published as International Conference Proceedings Series in the ACM Digital Library before the workshop. SUBMISSION GUIDELINE -------------------- Submission site: https://easychair.org/conferences/?conf=bx2018 Submissions should use the ACM Conference acmart Format with the ‘sigconf’ option (http://www.acm.org/publications/proceedings-template) with a font size of 10 point and the font family Times New Roman. All submissions should be in PDF format. If you use LaTeX or Word, please use the provided ACM acmart templates. Otherwise, please follow the ACM author instructions. If you are formatting your paper using LaTeX, you will need to set the 10pt option in the \documentclass command. If you are formatting your paper using Word, you may wish to use the provided Word template that supports this font size. Please include page numbers in your submission for review using the LaTeX command \settopmatter{printfolios=true} (see examples in template). Please also ensure that your submission is legible when printed on a black and white printer. In particular, please check that colors remain distinct and font sizes are legible. Submissions not complying with the above guidelines may be excluded from the reviewing process without further notice. If a paper is accepted, at least one author of the paper is expected to participate in the workshop to present it. Authors of accepted tool papers are also expected to be available to demonstrate their tool at the event. PROGRAM COMMITTEE MEMBERS ------------------------- Jens Weber (University of Victoria, co-chair) Kazutaka Matsuda (Tohoku Universiy, co-chair) Anthony Anjorin (University of Paderborn) James Cheney (University of Edinburgh) Anthony Cleve (University of Namur) Alcino Cunha (University of Minho and INESC TEC) Zinovy Diskin (McMaster University) Romina Eramo (University of L’Aquila) Jeremy Gibbons (University of Oxford) Holger Giese (Potsdam University) Boris Glavic (Illinois Institute of Technology) Martin Gogolla (University of Bremen) Soichiro Hidaka (Hosei University) Zhenjiang Hu (National Institute of Informatics) Michael Johnson (Macquarie University) Ekkart Kindler (Technical University of Denmark) Erhan Leblebici (TU Darmstadt) Fernando Orejas (Universitat Politècnica de Catalunya) Hugo Pacheco (University of Minho) Richard Paige (University of York) Arend Rensink (University of Twente) Andy Schürr (TU Darmstadt) Perdita Stevens (University of Edinburgh) James Terwilliger Janis Voigtländer (University of Duisburg-Essen) Meng Wang (University of Bristol) Bernhard Westfechtel (University of Bayreuth)

1 0

「論理学の哲学」ワークショップ：意味，証明，推論　のご案内です。
by 秋吉亮太 09 Dec '17

09 Dec '17

みなさま，早稲田大学高等研究所の秋吉と申します．以下の要領で論理学の哲学に関するワークショップを開催いたします．参加自由ですので，皆さまのご参加をお待ちしております．早稲田大学高等研究所主催「論理学の哲学」ワークショップ：意味，証明，推論 WIAS Event “Philosophy of Logic” Workshop: Meaning, Proof, and Inference 日時：2017年12月12日（火）15:00 - 18:15 Date: December 12, 2017 (Tue.) Time: 15:00 - 18:15 場所：早稲田大学早稲田キャンパス　11号館4階第一会議室 Venue: Meeting Room #1, 4th floor, Bldg. 11, Waseda Campus, Waseda University URL: https://www.waseda.jp/inst/wias/news/2017/11/14/4733/ <https://www.waseda.jp/inst/wias/news/2017/11/14/4733/> プログラム/Program： 15:00 - 16:00 西牟田祐樹（慶應義塾大学）/ Yuki Nishimuta (Keio University) 乗法的論理結合子の導入規則とスイッチングの関係 Relationship between the Introduction Rules of the Multiplicative Connectives and the Switching 16:00 - 16:30 ディスカッション/ Discussion 16:30 - 16:45 休憩/ Break 16:45 - 17:45 大西琢朗（京都大学）/ Takuro Onishi (Kyoto University) 　　　　　　　　　関係意味論を推論主義的に理解する Understanding Relational Semantics from the Viewpoint of Inferentialism 17:45 - 18:15 ディスカッション/ Discussion 使用言語/ Language：日本語（必要に応じて英語）/ Japanese (and English, if necessary) 司会/ Moderator：秋吉亮太（早稲田大学高等研究所）/ Ryota Akiyoshi (WIAS, Waseda University) 問い合わせ先/ Contact E-mail：秋吉亮太（早稲田大学高等研究所 ) georg.logic(a)gmail.com <mailto:georg.logic@gmail.com> 早稲田大学高等研究所/ Waseda Institute for Advanced Study, Waseda University

1 0

超準解析と数学基礎論のシンポジウム
by YOKOYAMA Keita 08 Dec '17

08 Dec '17

みなさま、北陸先端科学技術大学院大学の横山です。超準解析と数学基礎論のシンポジウムについて、プログラムができましたので再度ご案内いたします。詳しくは下記ホームページをご覧ください。 http://www.jaist.ac.jp/~y-keita/2017NSA/index.html 今回の会議では、江田勝哉先生にチュートリアル、木更津高専の倉橋太志先生に招待講演をお願いしております。（前回のメールで倉橋先生のお名前が間違っておりました。お詫びして訂正いたします。）超準解析を勉強したことのない学生の方等の参加も歓迎です。ご参加をご検討いただければ幸いです。 ********************** 超準解析と数学基礎論のシンポジウム http://www.jaist.ac.jp/~y-keita/2017NSA/index.html 日時：12月15,16日(金,土) 場所：早稲田大学早稲田キャンパス懇親会：12月15日 (5000円程度の予定です) 世話人：横山啓太(JAIST), 藤原誠(早稲田大学高等研究所) ※この会議は超準解析シンポジウム http://www.jaist.ac.jp/~y-keita/2014SLACS-NSA/ の後継になりますが、今回は超準解析分野を始め、超準構造や超準手法及び関連する数学基礎論の話題を広く募集致します。参加は登録無しでも可能ですが、できましたら以下のフォームに記入の上、 y-keita[at]jaist.ac.jp までメールにて事前にご連絡をいただけると幸いです。 (懇親会に参加希望の方はできるだけ早くご連絡ください。) ===以下フォーム=== １．お名前２．所属・身分３．メールアドレス４．懇親会に参加希望/希望しない (あまり直前ですと参加希望に添えないかもしれません) ５．その他 ===以上フォーム=== ********************** どうぞよろしくお願い致します。横山啓太 -- Keita Yokoyama y-keita(a)jaist.ac.jp

1 0

Talk by Amar Hadzihasanovic (07 Dec 11.00-)
by Kazushige TERUI 06 Dec '17

06 Dec '17

皆様直前のご案内で申し訳ありません。明日京都大学にて、新しくポスドクとして来られた Amar Hadzihasanovicさんによる講演があります。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 07 Dec, 2017 Place: Rm 478, Research Building 2, Main Campus, Kyoto University 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34) Speaker: Amar Hadzihasanovic (RIMS, Kyoto University) Title: Units without degeneracies, from higher categories to sequent calculi In a polycategory or multicategory, the existence of poly-cells or multi-cells satisfying certain universal properties induces coherent algebraic structures on the category of single-input, single-output cells (Cockett-Seely 1997, Hermida 2000). This was used by Hermida to produce an abstract proof of the strictification theorem for monoidal categories, and more generally bicategories. While the basic strategy seems generalisable, by a result by C. Simpson in 1998, no full strictification is possible for higher-dimensional categories. This seems to be due to problems with the combinatorics of cells with degenerate boundaries, that is, “0-ary” inputs or outputs, which were previously used to obtain units. We show that it is possible to obtain coherent units without degenerate boundaries, by deriving them from “equivalence” cells which satisfy lower-dimensional universal properties. This leads to a weaker semi-strictification theorem, which, however, we hope to generalise to arbitrary dimensions. Since the work of Cockett and Seely on linearly distributive categories, it is known that there is a deep connection between universal properties of cells in polycategories, and the rules of sequent calculi; in this context, units are also notorious for increasing the complexity of proof equivalence. In the last part of this talk, we pose some questions on the logical and computational aspects of our notion of unit, and the non-degeneracy constraint. ------------------------------------------ Kazushige TERUI Research Institute for Mathematical Sciences, Kyoto University. Kitashirakawa Oiwakecho, Sakyo-ku, Kyoto 606-8502, JAPAN. Phone: +81-75-753-7235 Fax: +81-75-753-7276 terui(a)kurims.kyoto-u.ac.jp http://www.kurims.kyoto-u.ac.jp/~terui/

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml December 2017