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

homotopy type theory
by logic＠math.tsukuba.ac.jp 30 Oct '16

30 Oct '16

> 圏論に関して質問があります。 > 種々の圏の存在はどのようにして主張されますか？ > > 例えば、公理的集合論では、論理式f(x),集合Xに関して、Xの元xでf(x)を満たすもの > から成る集合{x \in X|f(x)}が存在することが分出公理によって言えますが、圏論に > おいても、圏の存在を主張する公理群が定められていますか？ > 上記のような質問をいただいていますが、これはこの質問者以外の広い範囲の方に関心があることと思われますので、ここにお答えします。質問者の名前等は削除してあります。まず質問を Homotopy type theoryはZFCにかわる数学の基礎づけになるという話であるが、集合論はたとえばComprehensionのような豊かな構成原理をもっているが、HTTはどうなのか？と変形させていただきます。まずHTTのなかではn-typeというHierarchyが定義されます。ｎは−２以上の整数です。これはHomotopy theoryから借用された概念で、n-typeというのはｎを越える次元ではhomotopicalにはtrivialであることを意味します。Homotopy theoryの言葉づかいで言うならば、ｎを越える次元のhomotopy groupsはすべてtrivialであることを意味します。０-typeがいわゆるsetで、ここに話を限定するならば comprehensionをはじめとする集合論的構成はだいたいそのまま行えます。一般にはdependent function typeやdependent pair typeという構成原理を最初から内臓していますが、これだけではもちろん足りません。HTTがもつ強力な構成原理はinductionで、特に higher inductionが重要な役割を演じます。計算機言語のCOQや AGDAは通常にinductionを組み込んでいますが、higher inductive typesはまだ持っておりません。少しslogan的な言い方を許していただければ、 inductive typesはfree monadsに、higher inductive typesはmonadsの表現に対応します。 Inductiveな構成のいい例はCauchy realsの構成です。自然数から有理数を作るのは、古典的な話とあまりかわりません。それで有理数から実数を作るには、Dedekindのやり方とCauchyのやり方がありますが、後者の構成をinductiveにやるとどうなるかが、 https://homotopytypetheory.org/book/ の１１．３節に縷説されています。あるいはcirclesやspheresやsuspensionsはどのようにinductiveに構成されるか、第６章に縷説されています。是非ご覧になってください。にしむら筑波大学数学追伸：オマケです。手持無沙汰な折にどうぞ。 https://www.youtube.com/watch?v=VY01dVHvlFE

2 2

Re: [logic-ml] [jssst-ppl] 上級研究員・研究員・RA・インターン募集のお知らせ
by koba＠kb.is.s.u-tokyo.ac.jp 28 Oct '16

28 Oct '16

皆様、東京大学の小林です。下記のアナウンスに便乗して宣伝させていただきます。科研費基盤S「高階モデル検査の深化と発展」でも特任研究員を募集しておりますので http://www-kb.is.s.u-tokyo.ac.jp/~koba/hmc/call-for-postdoc.txt ご検討ください。（こちらではRAは公募しておりません。博士課程に入っていただければ似た待遇でのRAの雇用は可能かと思います）小林直樹東京大学大学院情報理工学系研究科コンピュータ科学専攻〒113-0033 東京都文京区本郷7-3-1 Phone: 03-5841-4124 Fax: 03-5841-4124 email: koba(a)is.s.u-tokyo.ac.jp From: Ichiro Hasuo <i.hasuo(a)acm.org> Subject: [jssst-ppl] 上級研究員・研究員・RA・インターン募集のお知らせ Date: Fri, 28 Oct 2016 14:28:18 +0900 > みなさま（重複投稿ご容赦ください）， > > 今年の10月から開始した ERATO プロジェクトで，上級研究員・研究員・RA > およびインターンを募集しております．プロジェクトの研究内容，職務内容，および応募・問い合わせについては > http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ERATO_MMSD_JobDescr.html > をご覧ください．どうかよろしくお願いいたします． > > 蓮尾一郎 > http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ > _______________________________________________ > jssst-ppl mailing list > jssst-ppl(a)fos.kuis.kyoto-u.ac.jp > http://www.fos.kuis.kyoto-u.ac.jp/cgi-bin/mailman/listinfo/jssst-ppl

1 0

24th WoLLIC 2017 - Call for Papers
by 小野寛晰 24 Oct '16

24 Oct '16

WoLLIC 2017 24th Workshop on Logic, Language, Information and Computation July 18-21, 2017 University College London (UCL), London, UK SCIENTIFIC SPONSORSHIP Interest Group in Pure and Applied Logics (IGPL) The Association for Logic, Language and Information (FoLLI) Association for Symbolic Logic (ASL) European Association for Theoretical Computer Science (EATCS) European Association for Computer Science Logic (EACSL) ACM Special Interest Group on Logic and Computation (ACM-SIGLOG) (TBC) Sociedade Brasileira de Computação (SBC) Sociedade Brasileira de Lógica (SBL) ORGANISATION Department of Computer Science, University College London, London, UK School of Electronic Engineering and Computer Science, Queen Mary College, London, UK Centro de Informática, Universidade Federal de Pernambuco, Brazil HOSTED BY Department of Computer Science, University College London, London, UK CALL FOR PAPERS WoLLIC is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. Each meeting includes invited talks and tutorials as well as contributed papers. The twenty-fourth WoLLIC will be held at the School of Electronic Engineering and Computer Science, Queen Mary College, London, UK, from July 18th to 21st, 2017. It is sponsored by the Association for Symbolic Logic (ASL), the Interest Group in Pure and Applied Logics (IGPL), the The Association for Logic, Language and Information (FoLLI), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), the Sociedade Brasileira de Computação (SBC), and the Sociedade Brasileira de Lógica (SBL). PAPER SUBMISSION Contributions are invited on all pertinent subjects, with particular interest in cross-disciplinary topics. Typical but not exclusive areas of interest are: foundations of computing and programming; novel computation models and paradigms; broad notions of proof and belief; proof mining, type theory, effective learnability; formal methods in software and hardware development; logical approach to natural language and reasoning; logics of programs, actions and resources; foundational aspects of information organization, search, flow, sharing, and protection; foundations of mathematics; philosophy of mathematics; philosophical logic. Proposed contributions should be in English, and consist of a scholarly exposition accessible to the non-specialist, including motivation, background, and comparison with related works. Articles should be written in the LaTeX format of LNCS by Springer (see authors instructions at http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0 <http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0>). They must not exceed 12 pages, with up to 5 additional pages for references and technical appendices. The paper's main results must not be published or submitted for publication in refereed venues, including journals and other scientific meetings. It is expected that each accepted paper be presented at the meeting by one of its authors. Papers must be submitted electronically at the WoLLIC 2017 EasyChair website. (Please go to http://wollic.org/wollic2017/instructions.html <http://wollic.org/wollic2017/instructions.html> for instructions.) A title and single-paragraph abstract should be submitted by Mar 14, 2017, and the full paper by Mar 21, 2017 (firm date). Notifications are expected by Apr 22, 2017, and final papers for the proceedings will be due by May 6, 2017 (firm date). PROCEEDINGS The proceedings of WoLLIC 2017, including both invited and contributed papers, will be published in advance of the meeting as a volume in Springer's LNCS series. In addition, abstracts will be published in the Conference Report section of the Logic Journal of the IGPL, and selected contributions will be published as a special post-conference WoLLIC 2017 issue of a scientific journal (to be confirmed). INVITED SPEAKERS Hazel Brickhurst (Bristol) (TBC) Ofra Magidor <http://users.ox.ac.uk/~ball1646/> (Oxford University, UK) Peter O'Hearn (UCL) (TBC) Nicole Schweikardt (Humboldt) (TBC) Fan Yang <https://sites.google.com/site/fanyanghp/> (Delft University, The Netherlands) Boris Zilber <https://people.maths.ox.ac.uk/zilber/> (Oxford University, UK) STUDENT GRANTS ASL sponsorship of WoLLIC 2017 will permit ASL student members to apply for a modest travel grant (deadline: May 1st, 2017). See http://www.aslonline.org/studenttravelawards.html <http://www.aslonline.org/studenttravelawards.html> for details. IMPORTANT DATES Mar 14, 2017: Paper title and abstract deadline Mar 21, 2017: Full paper deadline Apr 22, 2017: Author notification May 6, 2017: Final version deadline (firm) PROGRAMME COMMITTEE Matthias Baaz <http://www.logic.tuwien.ac.at/staff/baaz/home.html> (University of Technology, Vienna, Austria) John Baldwin <http://homepages.math.uic.edu/~jbaldwin/> (University of Illinois at Chicago, USA) Dana Bartozová <http://www.math.toronto.edu/bartosov/> (Universidade de São Paulo, Brazil) Agata Ciabattoni <https://www.logic.at/staff/agata/> (University of Technology, Vienna, Austria) Walter Dean <http://www2.warwick.ac.uk/fac/soc/philosophy/people/dean/> (University of Warwick, UK) Erich Grädel <https://logic.rwth-aachen.de/~graedel/> (RWTH Aachen, Germany) Volker Halbach <http://users.ox.ac.uk/~sfop0114/> (University of Oxford, UK) Juliette Kennedy <http://www.math.helsinki.fi/logic/people/juliette.kennedy/> (Helsinki University, Finland) (Chair) Dexter Kozen <http://www.cs.cornell.edu/~kozen/> (Cornell University, USA) Janos Makowsky <http://www.cs.technion.ac.il/~janos/> (Technion - Israel Institute of Technology, Israel) Larry Moss <http://www.indiana.edu/~iulg/moss/> (indiana University, USA) Alessandra Palmigiano <http://www.appliedlogictudelft.nl/alessandra-palmigiano/> (Delft University, The Netherlands) Mehrnoosh Sadrzadeh <http://www.eecs.qmul.ac.uk/people/view/33472/dr-mehrnoosh-sadrzadeh> (Queen Mary, UK) Sonja Smets <http://sonja.tiddlyspot.com/#HOME> (Amsterdam University, The Netherlands) Asger Törnquist <http://www.math.ku.dk/~asgert/> (Københavns Universitet, Denmark) Rineke Verbrugge <http://www.rinekeverbrugge.nl/> (University of Groningen, The Netherlands) Andrés Villaveces <https://avillavecesn.net/> (Universidad Nacional, Colombia) Philip Welch <http://www.maths.bris.ac.uk/~mapdw/> (University of Bristol, UK) STEERING COMMITTEE Samson Abramksy, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid Hodges, Ulrich Kohlenbach, Daniel Leivant, Leonid Libkin, Angus Macintyre, Luke Ong, Hiroakira Ono, Valeria de Paiva, Ruy de Queiroz, Jouko Väänänen. ORGANISING COMMITTEE Alexandra Silva <http://www.alexandrasilva.org/#/main.html> (Univ College London, UK) (Local co-chair) Mehrnoosh Sadrzadeh <http://www.eecs.qmul.ac.uk/people/view/33472/dr-mehrnoosh-sadrzadeh> (Queen Mary, UK) (Local co-chair) Paulo Oliva <http://www.eecs.qmul.ac.uk/~pbo/> (Queen Mary, UK) James Brotherston <http://www0.cs.ucl.ac.uk/staff/J.Brotherston/> (Univ College London, UK) Anjolina G. de Oliveira <http://www.cin.ufpe.br/~ago> (U Fed Pernambuco) Ruy de Queiroz <http://www.cin.ufpe.br/~ruy> (U Fed Pernambuco) (co-chair) FURTHER INFORMATION Contact one of the Co-Chairs of the Organising Committee. WEB PAGE http://wollic.org/wollic2017/ <http://wollic.org/wollic2017/>

1 0

RIMS研究集会「無限組合せ論と強制法理論」
by Teruyuki YORIOKA 24 Oct '16

24 Oct '16

みなさま静岡大学の依岡です。 11月28日（月）から12月1日（木）まで京都大学数理解析研究所で開催されます RIMS研究集会「無限組合せ論と強制法理論」のプログラムを下記のウェブサイトで公開しています。 http://www.ipc.shizuoka.ac.jp/~styorio/rims16/ 11月30日（水）に懇親会などを予定しています。懇親会などの予定はウェブサイトで公開します。みなさまぜひご参加ください。

1 0

第51回MLG数理論理学研究集会（10/27-30箱根）
by Kazushige TERUI 21 Oct '16

21 Oct '16

みなさま第51回MLG数理論理学研究集会のプログラムが確定しましたのでご案内申し上げます。宿泊を伴わない参加は無料ですので、お気軽にお越しください。 Web Page: http://www.kurims.kyoto-u.ac.jp/~terui/mlg2016.html Program: http://www.kurims.kyoto-u.ac.jp/~terui/mlg2016.pdf 照井一成 ------------------------------------------ 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

PEPM 2017: Call for Posters
by Ryosuke SATO 21 Oct '16

21 Oct '16

皆様、（複数受け取られた場合はご容赦ください。）東京大学の佐藤亮介です。 PEPM 2017 のポスター募集のお知らせです．投稿の締め切りは11月8日（火）です．是非，投稿をご検討ください． -- 東京大学大学院情報理工学系研究科佐藤亮介 ryosuke(a)kb.is.s.u-tokyo.ac.jp ------------------------------------------------------------------- CALL FOR POSTERS Workshop on PARTIAL EVALUATION AND PROGRAM MANIPULATION (PEPM 2017) PEPM 2017 information: http://conf.researchr.org/home/PEPM-2017 Submissions: https://pepm17.hotcrp.com/ Paris, France, January 16th - 17th, 2017 (co-located with POPL 2017) PEPM is the premier forum for discussion of semantics-based program manipulation. The first ACM SIGPLAN PEPM symposium took place in 1991, and meetings have been held in affiliation with POPL every year since 2006. PEPM 2017 will be based on a broad interpretation of semantics-based program manipulation, reflecting the expanded scope of PEPM in recent years beyond the traditionally covered areas of partial evaluation and specialization. Posters ------- In order to maintain the dynamic and interactive nature of PEPM, we solicit submission of posters. Poster submissions are 2-page articles in ACM Proceedings style that present preliminary work (see "Submission guidelines" below for more details). If accepted, the work will be presented as part of an interactive poster session at PEPM. Scope ----- Topics of interest for PEPM 2017 include, but are not limited to: * Program and model manipulation techniques such as: supercompilation, partial evaluation, fusion, on-the-fly program adaptation, active libraries, program inversion, slicing, symbolic execution, refactoring, decompilation, and obfuscation. * Program analysis techniques that are used to drive program/model manipulation such as: abstract interpretation, termination checking, binding-time analysis, constraint solving, type systems, automated testing and test case generation. * Techniques that treat programs/models as data objects including metaprogramming, generative programming, embedded domain-specific languages, program synthesis by sketching and inductive programming, staged computation, and model-driven program generation and transformation. * Application of the above techniques including case studies of program manipulation in real-world (industrial, open-source) projects and software development processes, descriptions of robust tools capable of effectively handling realistic applications, benchmarking. Examples of application domains include legacy program understanding and transformation, DSL implementations, visual languages and end-user programming, scientific computing, middleware frameworks and infrastructure needed for distributed and web-based applications, embedded and resource-limited computation, and security. This list of categories is not exhaustive, and we encourage submissions describing applications of semantics-based program manipulation techniques in new domains. If you have a question as to whether a potential submission is within the scope of the workshop, please contact the programme chairs. Submission guidelines --------------------- * Posters should describe work relevant to the PEPM community, and must not exceed 2 pages in ACM Proceedings style. We invite poster submissions that present early work not yet ready for submission to a conference or journal, identify new research problems, showcase tools and technologies developed by the author(s), or describe student research projects. If accepted, the work will be presented as part of an interactive poster session at PEPM. At least one author of each accepted contribution must attend the workshop and present the work. Student participants with accepted poster papers can apply for a SIGPLAN PAC grant to help cover travel expenses and other support. PAC also offers other support, such as for child-care expenses during the meeting or for travel costs for companions of SIGPLAN members with physical disabilities, as well as for travel from locations outside of North America and Europe. For details on the PAC programme, see its web page. Publication ----------- Posters will appear along with accepted papers in formal proceedings published by ACM Press and in the ACM Digital Library. Keynote ------- Neil Jones (DIKU) will give the PEPM keynote talk, titled Compiling Untyped Lambda Calculus to Lower-level Code by Game Semantics and Partial Evaluation Submission ---------- Posters should be submitted electronically via HotCRP. https://pepm17.hotcrp.com/ Authors using LaTeX to prepare their submissions should use the new improved SIGPLAN proceedings style, and specifically the sigplanconf.cls 9pt template. Important Dates --------------- * Poster submission : Tuesday 8th November 2016 * Author notification : Friday 18th November 2016 * Camera ready : Monday 28th November 2016 * Workshop : Monday 16th - Tuesday 17th January 2017 The proceedings will be published 2 weeks pre-conference. AUTHORS TAKE NOTE: The official publication date is the date the proceedings are made available in the ACM Digital Library. This date may be up to two weeks prior to the first day of your conference. The official publication date affects the deadline for any patent filings related to published work. (For those rare conferences whose proceedings are published in the ACM Digital Library after the conference is over, the official publication date remains the first day of the conference.). PEPM'17 Programme Committee --------------------------- Elvira Albert (Complutense University of Madrid, Spain) Don Batory (University of Texas at Austin, USA) Martin Berger (University of Sussex, UK) Sebastian Erdweg (TU Delft, Netherlands) Andrew Farmer (Facebook, USA) Matthew Flatt (University of Utah, USA) John Gallagher (Roskilde University, Denmark) Robert Glück (DIKU, Denmark) Jurriaan Hage (Utrecht University, Netherlands) Zhenjiang Hu (National Institute of Informatics, Japan) Yukiyoshi Kameyama (University of Tsukuba, Japan) Ilya Klyuchnikov (Facebook, UK) Huiqing Li (EE, UK) Annie Liu (Stony Brook University, USA) Markus Püschel (ETH Zurich, Switzerland) Ryosuke SATO (University of Tokyo, Japan) Sven-Bodo Scholz (Heriot-Watt University, UK) Ulrik Schultz (co-chair) (University of Southern Denmark) Ilya Sergey (University College London, UK) Chung-chieh Shan (Indiana University, USA) Tijs van der Storm (Centrum Wiskunde & Informatica, Netherlands) Jeremy Yallop (co-chair) (University of Cambridge, UK)

1 0

Kobe Colloquium on Logic, Statistics and Informatics, October 13, 2016
by Hirotaka Kikyo 06 Oct '16

06 Oct '16

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。 (2重に受け取られた方はご容赦願います) 日時: 2016/10/13 (木) 3:00pm - 4:30pm 場所: 神戸大学六甲台第2キャンパス自然科学総合研究棟3号館421室講演者： Kaisa Kangas （神戸大・システム情報/Helsinki U.）題目： Group Configuration for Quasiminimal Classes 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/guid/access/rokko/rokkodai-dai2.html 連絡先：桔梗宏孝 kikyo(a)kobe-u.ac.jp

1 0

Talk by Adam Prenosil (13 Oct 11:00-)
by Tetsuya Sato 05 Oct '16

05 Oct '16

京都大学数理解析研究所の佐藤です。 10月13日11:00から、チェコ科学アカデミーのAdam Prenosil氏に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 13 Oct, 2016 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) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speaker: Adam Prenosil (Czech Academy of Sciences) Title: Classical proof theory, non-classically Abstract: We present an approach to cut elimination in classical logic which appeals to elimination rules.rather than to induction on cut rank and which works equally well for proofs from a non-empty set of sequential premises. As an illustration of the benefits of accepting elimination rules as an integral part of the sequent calculus for classical logic, we use the calculus with elimination rules to provide a particularly simple syntactic proof of a recent non-classical refinement of Craig's interpolation theorem due to Milne. This approach, while non-standard, is in fact natural when we view classical logic as part of the family of super-Belnap logics, that is, extensions of the four-valued Belnap-Dunn logic. We shall therefore start by introducing this family proof-theoretically as the logics which retain the structural and logical rules of classical logic, but relax Identity and Cut (as opposed to substructural logics, which retain Identity and Cut but relax the structural rules of classical logic).

1 0

ワークショップ「2階論理の意味論」
by Makoto Kikuchi 30 Sep '16

30 Sep '16

皆様，以下の要領でワークショップを開催しますのでお知らせします．神戸大学菊池誠日時：2016年11月5日（土）15:45〜17:45 場所：東京大学駒場キャンパス1号館1階108室題目：ワークショップ「 2階論理の意味論」　　科学基礎論学会2016年度秋の研究例会（非会員は参加費1,000円が必要です）　　科学基礎論学会 Web Page：http://phsc.jp オーガナイザ：菊池誠（神戸大学）提題者：　佐藤智哉　2階論理的妥当性の新しい意味論的特徴づけ　池上大祐（東京電機大学）2階論理とブール値2階論理　新井敏康（千葉大学）竹内の基本予想の意味論的証明ワークショップ趣旨：「すべて」や「存在」という量化の対象が「個物」に限定される形式的論理が 1階論理，「個物と概念」であるのが2階論理，そして「個物，概念，概念上の概念，…」のすべてであるのが高階論理である．1階論理が形式的論理の現在の事実上の標準理論である．ただし，BoolosやShapiro，Vaananenの哲学的な議論やFriedmanの逆数学の研究プログラムにも見られるように，今でも2階論理それ自身や2階論理の上で展開される公理系に関心が持たれている． 2階論理の意味論を考える際に問題になるのが「概念」を対象とする2階量化子の解釈である．2階量化子の解釈は「個物全体の集合」の部分集合族を与えることで定められる．最も自然な2階論理の意味論は2階量化子の解釈を与える部分集合族を「個物全体の集合」の冪集合とすることで定められるが，この意味論では通常の公理と推論規則で2階論理の完全性定理は成り立たない． Henkinは2階量化子の解釈を与える部分集合族を「個物全体の集合」の任意に選ばれた部分集合族とすれば，通常の公理と推論規則で2階論理の完全性定理が成り立つことを示した． Henkin流の意味論が2階論理の現在の事実上の標準的な意味論である．しかし，このHenkin流の意味論に基づく2階論理とは実質的には1階論理の特別な場合であり，他の意味論の可能性や必要性がない訳ではない．本ワークショップではHenkin流の意味論以外の2階論理の意味論について，佐藤智哉が哲学の立場から，池上大祐が集合論の立場から最近の研究を紹介し，新井敏康が証明論の立場から古典的な議論を紹介する．提題要旨：提題1：2階論理的妥当性の新しい意味論的特徴づけ　佐藤智哉二階述語論理の標準意味論に関する一つの問題は、標準意味論においては特定の集合の特定の性質に依存するような論証が妥当となることである。そのような集合論の結果に基づく論証は「集合論的妥当」とでも呼ばれるべきで、「論理的妥当」な論証とは区別されなければならない。標準意味論の中で妥当となる論証のうち、どの論証が真の意味での論理的妥当であり、どの論証が集合論的妥当なのか。二階述語言語の論理的妥当性を特徴づけるためには、標準意味論とは別の新しい意味論システムが必要である。本発表の主目的は、そのような標準意味論に代わる新しい意味論システムの紹介である。新しい意味論システムのための一つのアイデアは、論理定項とは何かという哲学的議論が、論理的妥当性と集合論的妥当性の区別に応用できるということである。Tarskiに始まる近年の論理定項研究を紹介した後で、それを使ってどのように二階論理的妥当性が参考文献 D. Bonnay, Logicality and invariance, The Bulletin of Symbolic Logic, 14, 29–68, 2008. S. Feferman, Logic, logics, and logicism, Notre Dame Journal of Formal Logic, 40, 31–54, 1999 G. Sher, The Bounds of Logic: A Generalized View Point, Cambridge, MA: MIT Press, (1991). T. Sato, A new semantic characterization of second-order logical validity (unpublished). A Tarski, What are logical notions? J. Corcoran (Ed.), History and Philosophy of Logic, 7, 143–154, 1986. 提題2：2階論理とブール値2階論理　池上大祐（東京電機大学）二階述語論理の代表的な意味論としてタルスキ意味論（完全意味論）とヘンキン意味論の二つがある。タルスキ意味論を用いると、一階述語論理で表現できない様々な性質を記述できるが、一階述語論理において成り立つ定理（完全性定理、コンパクト性定理など）がことごとく成り立たず、二階述語論理は非常に複雑になる。一方、ヘンキン意味論を用いると、一階述語論理において成り立つ多くの定理が成り立つが、論理の表現力は一階述語論理と全く同じで、一階述語論理と比べて二階述語論理に新しい現象は見られない。本講演では、二階述語論理の意味論としてブール値意味論を導入し、 1) V = L の下ではブール値意味論はタルスキ意味論と同じ複雑さを持つこと 2) 巨大基数とウディンのΩ論理についての適切な仮定をすると、ブール値意味論は、　タルスキ意味論より単純でヘンキン意味論より複雑な意味論になることの二点について論じる。本講演で述べる多くの研究成果は Jouko Vaananen 氏との共同研究によるものである。参考文献 D. Ikegami and J. Vaananen, Boolean-Valued Second-Order Logic, Notre Dame Journal of Formal Logic, 56 (1), 167–190, 2015. 提題3：基本予想の意味論的証明　新井敏康（千葉大学）竹内外史は1953に高階論理GLCを定め，GLCについてCut除去定理が成り立つという基本予想を提示した．GLCの部分体系である2階論理がG1LCであり，竹内外史はG1LCの部分体系で基本予想が成り立つことを構文論的に示した．意味論的には，まずCutを持たない体系の3値モデルに対する完全性がSchutteによって示され，その後，3値モデルを2値モデルに完備化する方法で，G1LCについてはTaitによって，GLCについては高橋元男とPrawitzによって独立に，竹内の基本予想が成り立つことが証明された．その意味論的な議論を紹介する．参考文献新井敏康「竹内の基本予想とは何か，何であるべきか」数理解析研究所講究録, 1442, 1-7, 2005.

1 0

Talk by Yoriyuki Yamagata (6 Oct 11:00-)
by Tetsuya Sato 29 Sep '16

29 Sep '16

京都大学数理解析研究所の佐藤です。 10月6日11:00から、産業技術総合研究所の山形頼之氏に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 6 Oct, 2016 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) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speaker: Yoriyuki Yamagata (National Institute of Advanced Industrial Science and Technology) (Website: http://staff.aist.go.jp/yoriyuki.yamagata/en/) Title: Consistency proof of an arithmetic with substitution inside a bounded arithmetic Abstract: Bounded arithmetics are systems of arithmetic in which induction is restricted to bounded formulas. Bounded formulas are formulas in which all quantifiers are bounded by some terms. Among many such systems, Buss's hierarchy of bounded arithmetics have particular interest, because their provably total functions exactly correspond polynomial-time hierarchy. A major open problem on bounded arithmetics is whether Buss's hierarchy collapses or not. If it collapses, for example, it implies P=NP. One strategy to differentiate the hierarchy is to use Gödel sentence of some theories. In this talk, we consider a theory PV by Cook and Urquhart and its restrictions. PV is an equational system, which has roughly the same strength to Buss's S12. Beckmann proved that when induction and substitution are removed from PV, the consistency of the system can be proved by S12. On the other hand, Buss and Ignjatović proved that S12 cannot prove the consistency of the system which obtained by removing just induction, but adding propositional logic and BASIC axioms, from PV. In this talk, we improve the Beckmann by proving that S22 can prove the consistency of the system which obtained by removing just induction from PV. By delineating bounded arithmetics which can prove consistency of various restrictions of PV, we hope to prove non-collapse of Buss's hierarchy, and relatedly, polynomial-time hierarchy.

1 0

締切延長：第51回MLG数理論理学研究集会（10/27-30箱根）
by Kazushige TERUI 26 Sep '16

26 Sep '16

みなさま先日来ご案内しているMLG研究集会についてですが、宿泊・講演ともまだ余裕がありますので、締切を９月２９日（木）まで延長したいと思います。なお今回はチェコ科学アカデミーから以下の方々が参加されます。 Petr Cintula（数理ファジィ論理・抽象代数論理など） Zuzana Hanikova（ファジィ集合論など） Rostislav Horcik（部分構造論理など） Carles Noguera（数理ファジィ論理・抽象代数論理など） Tommaso Moraschini, Adam Prenosil, Igor Sedlar, Amanda Vidal うち数名の方には入門的な講演をお願いする予定です。３泊４日ですが、部分参加も歓迎します。どうぞよろしくお願いします。照井 --------------------------------------------------- 第51回MLG数理論理学研究集会締切延長 MLG数理論理学研究集会は，1971年開始された，この分野の多くの研究者が参加している40年以上続く研究集会です。成果を発表し合ったり，アイデアを交換したりと，ザックバランな雰囲気で行われています。数学の他分野や，広く数理科学，情報科学，哲学の方々や，外国からの研究者を迎えるなど，オープンに運営されています。（昨年度の様子：http://www.kurims.kyoto-u.ac.jp/~terui/mlg2015.html ）日時：2016年10月27日（木）午後 − 30日（日）午前場所：四季の湯強羅静雲荘（ http://gora-seiunsou.jp/ ）参加費用：全参加の場合30,000円（3食つき、懇親会費は別途）参加・講演申し込み： 9月29日（木）までウェブページ：http://www.kurims.kyoto-u.ac.jp/~terui/mlg2016.html 詳細は上記Web Pageをご覧ください。みなさまの参加をお待ちしております。京都大学数理解析研究所照井　一成 ------------------------------------------ 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

correction again
by 吉信康夫 21 Sep '16

21 Sep '16

皆様：吉信＠名古屋大学大学院情報科学研究科です。すでに何人の方からご指摘いただきましたように、セミナーご案内の日時も誤っておりました。重ねてお詫びいたしますとともに、訂正したものを改めて投稿させていただきます。名古屋数学基礎論セミナーのご案内日時：9月23日(金) 15:30- 場所：名古屋大学大学院情報科学研究科棟 2F 206号室講演者：木原貴行 (University of California, Berkeley) タイトル：　多対一次数の一様Martin予想とWadge次数アブストラクト：　多対一次数は，決定問題の計算論的複雑性を測る指標の一つであり，Wadge次数は，ベール空間の部分集合の位相的複雑性を測る指標の一つである．両者の定義は酷似している一方，多対一次数構造は混沌として掴み所がなく，Wadge次数構造は美しく整然としており単純明快である．したがって，それらの酷似した定義とは対照的に，それらの構造は如何なる意味でも同型ではない．それにも関わらず，「自然」な多対一次数の構造と Wadge次数構造が同型であることを示す．　より正確には，Woodinによって提案された決定性公理の拡張であるAD+の下で，任意の better-quasi-order Q に対して，一様次数不変な Q 値多対一次数の構造と Q 値Wadge次数構造が同型であることを示す．

1 0

correction
by 吉信康夫 21 Sep '16

21 Sep '16

皆様：吉信康夫＠名古屋大学大学院情報科学研究科です。先ほどお送りしたセミナーのご案内で、講演者のお名前の字が誤っておりました。お詫びいたしますとともに、訂正したものを改めてお送りいたします。名古屋数学基礎論セミナーのご案内日時：9月13日(金) 15:30- 場所：名古屋大学大学院情報科学研究科棟 2F 206号室講演者：木原貴行 (University of California, Berkeley) タイトル：　多対一次数の一様Martin予想とWadge次数アブストラクト：　多対一次数は，決定問題の計算論的複雑性を測る指標の一つであり，Wadge次数は，ベール空間の部分集合の位相的複雑性を測る指標の一つである．両者の定義は酷似している一方，多対一次数構造は混沌として掴み所がなく，Wadge次数構造は美しく整然としており単純明快である．したがって，それらの酷似した定義とは対照的に，それらの構造は如何なる意味でも同型ではない．それにも関わらず，「自然」な多対一次数の構造と Wadge次数構造が同型であることを示す．　より正確には，Woodinによって提案された決定性公理の拡張であるAD+の下で，任意の better-quasi-order Q に対して，一様次数不変な Q 値多対一次数の構造と Q 値Wadge次数構造が同型であることを示す．

1 0

nagoya logic seminar
by 吉信康夫 21 Sep '16

21 Sep '16

皆様：吉信康夫＠名古屋大学大学院情報科学研究科です。以下の要領で名古屋数学基礎論セミナーを開催します。奮って御参加下さい。日時：9月13日(金) 15:30- 場所：名古屋大学大学院情報科学研究科棟 2F 206号室講演者：木原貴之 (University of California, Berkeley) タイトル：　多対一次数の一様Martin予想とWadge次数アブストラクト：　多対一次数は，決定問題の計算論的複雑性を測る指標の一つであり，Wadge次数は，ベール空間の部分集合の位相的複雑性を測る指標の一つである．両者の定義は酷似している一方，多対一次数構造は混沌として掴み所がなく，Wadge次数構造は美しく整然としており単純明快である．したがって，それらの酷似した定義とは対照的に，それらの構造は如何なる意味でも同型ではない．それにも関わらず，「自然」な多対一次数の構造と Wadge次数構造が同型であることを示す．　より正確には，Woodinによって提案された決定性公理の拡張であるAD+の下で，任意の better-quasi-order Q に対して，一様次数不変な Q 値多対一次数の構造と Q 値Wadge次数構造が同型であることを示す．

1 0

公募
by 泉英明 19 Sep '16

19 Sep '16

皆様千葉工業大学教育センター数学教室の泉です。現在、当数学教室では助教１名の公募を行っております。締切は 2016年10月20日(必着)となっております。詳細については http://www.it-chiba.ac.jp/institute/adoption/ をご覧ください

1 0

(no subject)
by 泉英明 19 Sep '16

19 Sep '16

皆様千葉工業大学教育センター数学教室の泉です。現在、当数学教室では助教１名の公募を行っております。締切は 2016年10月20日(必着)となっております。詳細については http://www.it-chiba.ac.jp/institute/adoption/ をご覧ください。

1 0

数学基礎論とその応用
by Makoto Kikuchi 17 Sep '16

17 Sep '16

皆様，以前にもご案内しましたが，2016年9月26日（月）から29日（木）まで， RIMS 研究集会「数学基礎論とその応用」を開催しますのでお知らせします． http://www2.kobe-u.ac.jp/~mkikuchi/mla2016.html 事前登録なしで参加できます．また，以下の要領で懇親会を開きます．日時：2016年9月28日（水）午後6時から会場：マーブルルーム https://www.hotpepper.jp/strJ000040535/ 場所：京都府京都市中京区先斗町通三条下ル橋下町135先斗町ビル4F 交通：京阪三条駅から徒歩5分，阪急河原町駅から徒歩10分内容：立食（飲み放題）会費：3,000円（当日会場で支払い） 8月に研究集会への参加申し込みをお送り下さった方で，懇親会への出欠の変更のない方はご連絡くださる必要はありません．出欠を変更される方，未定とお答えになられた方，また，参加申し込みをなさっていない方で懇親会への出席をご希望の方は，2016年9月24日（土）までに，研究代表者（菊池）宛に件名「mla2016」として e-mail でご連絡ください．なお，本研究集会は研究交流を目的とするものですが，学部学生を含む学生の方の研究集会および懇親会への参加を歓迎します．午前中の講演は全て日本語です．ご興味をお持ちの方はご遠慮なくご参加ください．菊池誠記 RIMS研究集会　数学基礎論とその応用日時：2016年9月26日(月)11:00 ~ 9月29日(木)15:00 場所：京都大学数理解析研究所111室研究代表者：菊池誠(神戸大)mkikuchi(a)kobe-u.ac.jp プログラム： 9月26日(月) 11:00-11:50 宮元忠敏(南山大) 集合論で試される構造と構成のいくつか 13:30-14:20 Joel David Hamkins(CUNY) The Modal Logic of Set-Theoretic Potentialism 14:30-15:20 樋口幸治郎(日大工) Computably Represented Structures 15:30-16:20 竹内耕太(筑波大) Properties Characterized by Generalized Indiscernible 9月27日(火) 10:00-10:50 新井敏康(千葉大) 角田先生, 証明論を分かって下さい 11:00-11:50 板井昌典(東海大) 1980年代半ば,米国中西部のモデル理論,そして未来-モデル理論賛歌 13:30-14:20 Frank Wager (Lion 大) Recent Interactions between Model Theory and Combinatorics 14:30-15:20 横山啓太(JAIST) On the Proof-Theoretic Strength of Ramsey's Theorem for Pairs 15:30-16:20 丸山善宏(京大) Dynamics of Duality: How Duality Emerges, Changes, and Breaks 9月28日(水) 10:00-10:50 向井国昭(慶応大) Barwiseのモデル論的意味論の周辺と抽象設計学 11:00-11:50 金井康雄(大和大) 公理的集合論の一角を彷徨って 13:30-14:20 Bakh Khoussainov(Auckland 大/京都大) Computably Enumerable Structures: Domain Dependence 14:30-15:20 星野直彦(京都大) Geometry of Interaction and Higher Order Functions 15:30-16:20 Diego Mejia(静岡大) Several Values in Cichon's Diagram 9月29日(木) 10:00-10:50 佐藤洋祐(東理大) 限量子記号消去アルゴリズムとその計算の現状について 11:00-11:50 隈部正博(放送大) Generic Sets の Turing Degrees について 13:30-14:20 Philip Welch(Bristol 大) Generalised Squares and Higher Stationarity

1 0

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

16 Sep '16

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

1 0

Talk by Quentin Heath, 29 Sept.
by koba＠kb.is.s.u-tokyo.ac.jp 16 Sep '16

16 Sep '16

皆様、東京大学の小林です。以下のとおり講演会を開催いたしますので、ご興味のある方はお集まりください。小林直樹東京大学大学院情報理工学系研究科コンピュータ科学専攻〒113-0033 東京都文京区本郷7-3-1 Phone: 03-5841-4124 Fax: 03-5841-4124 email: koba(a)is.s.u-tokyo.ac.jp ================== Time: 3:00pm, Thursday, the 29th September Place: Room 214, 7th Building of Faculty of Science （理学部7号館） Title: Proof certificates as proof theory for model checking Speaker: Quentin Heath (LIX, Ecole polytechnique) Abstract: Model checking has proved valuable on its own for locating errors in finite state computer models and specifications. However, model checkers can also be used to prove properties that will be consumed by other computational logic systems, such as theorem provers. In order for the model checker to be trusted by an external tool, we ask that it outputs its ``proof evidence'' as a formally defined document---a proof certificate---and that this document is checked by a trusted proof checker. We propose such a proof checker based on a first-order variant of linear logic, and justify why this logic is appealing as a foundation for model checking. We also provide a proof system for this logic, and tie in the notion of proof certificates in a way that makes proof checking sound for a minimal amount of work. As a result, a range of model checking computations can be imported in formal proofs and certified by a proof checker that is simple, non idiosyncratic, and easy to certify.

1 0

Nagoya Set Theory seminar
by 吉信康夫 15 Sep '16

15 Sep '16

名古屋集合論セミナーのご案内：(重複して受け取られた方はご容赦ください) 日時：2016年9月16日(金) 午後3時30分より場所：名古屋大学大学院情報科学研究科2階206号室講演者：薄葉季路(早稲田大学) 題目：Ground Axiomの変種について概要：Ground Axiomは「universeがforcing extensionになっていない」ことを主張する公理であるが、forcingをc.c.c., properなどに限定した Ground Axiomの編集について考察し、例えば「c.c.c. forcing extensionではないがproper forcing extensionになる」などのconsistencyを示す。多数のご参加をお待ちしております。名古屋大学大学院情報科学研究科吉信康夫

1 0

第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）論文募集/発表募集
by Isao Sasano 14 Sep '16

14 Sep '16

皆様第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）のご案内です。申込方法や詳細につきましては、webページにて確定次第お知らせします。是非ご投稿、ご参加をご検討ください。 ====================================================================== 第19回プログラミングおよびプログラミング言語ワークショップ (PPL2017) https://ppl2017.ipl-e.ai.kyutech.ac.jp/ 論文募集/発表募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2017年3月8日(水)～3月10日(金) 会場: 山梨県笛吹市石和温泉「華やぎの章慶山」 PPL2017は，プログラミングとプログラミング言語に関連する幅広い分野の研究者・技術者・学生が一堂に会し，最新の研究成果の発表や，新たな研究課題の提案・討論・アイディア交換を行うことを目的とした，合宿形式の研究集会です．プログラミング方法論，プログラミング言語の理論・設計・実装などに関する研究発表を，カテゴリ別に幅広く募集します．カテゴリ1 (国内外未発表論文) ---------------------------- 完成した理論やシステムの研究発表のみならず，萌芽的なアイディアや問題点の提示等も歓迎します．発展途上の研究内容も積極的に採録する方針です．また，カテゴリ1で発表された研究については，会場での討議や査読コメントをもとにその完成度を高め，将来の学術雑誌・国際会議等での業績に結び付けることを奨励しています．そのため，予稿集の配布は参加者のみへの限定的なものとします．投稿手続きは2段階です．発表申込締切: 2016年12月21日(水) 17:00 (JST) 論文提出締切: 2017年1月11日(水) 17:00 (JST) 採否通知：2017年2月3日(金) カテゴリ2 (国外既発表論文) -------------------------- 査読付の国際会議または学術雑誌等で既発表であるが国内では未発表である研究を紹介する場です．採録決定済みの研究も含みます．PPLへの関連をもとに採否を判定いたしますが，申し込み多数の場合はプログラム委員会で選考致します．発表申込締切: 2017年1月25日(水) 17:00 (JST) 採否通知：2017年2月6日(月) カテゴリ3 (ポスター・デモ発表) ------------------------------ 2時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採否を判定いたしますが，申し込み多数の場合はプログラム委員会で選考致します．発表申込締切: 2017年2月8日(水) 17:00 (JST) 採否通知：2017年2月15日(水) カテゴリ4 (サーベイ・チュートリアル発表) ---------------------------------------- 研究動向の紹介(発表者の研究も含む) や分野間の相互理解と参加者の知識の底上げとなる発表を募集します．既発表・未発表の別を問いません．PPLへの関連，著者の研究発表実績，トピックや切り口の興味深さをもとに，プログラム委員会で選考致します．発表申込締切: 2017年1月25日(水) 17:00 (JST) 採否通知：2017年2月6日(月) 申込方法や詳細につきましては，上記ウェブページにて確定次第お知らせ致します． ====================================================================== 問い合わせ先 ppl2017-oc(a)ipl-e.ai.kyutech.ac.xn--jp()-753c9gpa1b92cqcsg7jrh5d1ix122cxi0h ppl2017-pc-chairs(a)ipl-e.ai.kyutech.ac.xn--jp(/)-m53d8hra6b05cmntd6e6b1719ok76b ====================================================================== プログラム委員会青谷知幸 (東京工業大学) 浅田和之 (東京大学) Reynald Affeldt (産業技術総合研究所) 稲葉一浩 (Google) 上野雄大 (東北大学) 菊池健太郎 (東北大学) 小宮常康 (電気通信大学) 篠埜功 (芝浦工業大学) 佐藤亮介 (東京大学) 首藤一幸 (東京工業大学) 末永幸平 (京都大学) 宋剛秀 (神戸大学) 千葉滋 (東京大学) 土屋達弘 (大阪大学) 中野圭介 (電気通信大学) 鍋島英知 (山梨大学) 番原睦則 (神戸大学) 前田敦司 (筑波大学) 松田一孝 (東北大学) 森畑明昌 (東京大学) 八杉昌宏 (九州工業大学) 組織委員会江本健斗 (九州工業大学) [組織委員長] 平石拓 (京都大学) 佐藤重幸 (高知工科大学) 海野広志 (筑波大学) 対馬かなえ (国立情報学研究所) 塚田武志 (東京大学) 篠埜功 (芝浦工業大学) [プログラム共同委員長] 番原睦則 (神戸大学) [プログラム共同委員長] ====================================================================== 篠埜　功 -- Isao Sasano <sasano(a)sic.shibaura-it.ac.jp>

1 0

第51回MLG数理論理学研究集会参加・講演募集（10/27-30箱根）
by Kazushige TERUI 13 Sep '16

13 Sep '16

第51回MLG数理論理学研究集会参加・講演募集 MLG数理論理学研究集会は，1971年開始された，この分野の多くの研究者が参加している40年以上続く研究集会です。成果を発表し合ったり，アイデアを交換したりと，ザックバランな雰囲気で行われています。数学の他分野や，広く数理科学，情報科学，哲学の方々や，外国からの研究者を迎えるなど，オープンに運営されています。（昨年度の様子：http://www.kurims.kyoto-u.ac.jp/~terui/mlg2015.html ）今回は試験的な試みとして「未解決問題セッション」を設けたいと思います（詳細はHP）。どうぞ奮ってご参加ください。日時：2016年10月27日（木）午後 − 30日（日）午前場所：四季の湯強羅静雲荘（ http://gora-seiunsou.jp/ ）参加費用：全参加の場合30,000円（3食つき、懇親会費は別途）参加・講演申し込み： 9月25日（日）までウェブページ：http://www.kurims.kyoto-u.ac.jp/~terui/mlg2016.html 詳細は上記Web Pageをご覧ください。みなさまの参加をお待ちしております。京都大学数理解析研究所照井　一成 ------------------------------------------ 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/ ------------------------------------------ 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

第35回量子情報技術研究会(QIT35)のご案内
by NISHIMURA Harumichi 10 Sep '16

10 Sep '16

logic-mlの皆様 QIT35世話人に代わりまして第35回量子情報技術研究会(QIT35)の会告を以下の通り投稿させていただきます．どうぞよろしくお願いいたします．名古屋大学大学院情報科学研究科西村治道 --------------------------------------------------- 第35回量子情報技術研究会(QIT35)のお知らせ情報科学と量子力学を融合させた新しい分野、量子情報科学に関する研究会を下記のとおり開催いたします。ふるってご発表、ご参加ねがいます。 https://staff.aist.go.jp/s-kawabata/qit/qit35 ・日時：平成28年11月24日（木），25日（金）・会場：高エネルギー加速器研究機構（KEK）（〒305-0801 茨城県つくば市大穂1-1）・発表募集分野：量子情報，量子計算，量子暗号など広く量子情報技術に関わる理論的研究，実験的研究，計算機科学的研究，数学的研究，及びその他関連分野・申込締切： - 口頭講演：平成28年10月7日（金） - ポスター発表：平成28年10月21日（金） - 参加登録（事前）：平成28年10月28日（金）・招待講演： - 清水明（東大総合文化）「アンサンブルの等価性の量子破綻にともなう異常な量子状態」 - 長谷川祐司（ウィーン工科大・北大）「残留する確定性：混合状態でも有効な誤差と擾乱の不確定性関係」 - 横倉祐貴（理研）「ネーター不変量としての熱力学エントロピー」・チュートリアル講演 - 高柳匡（京大基研）「Emergent Spacetime from Qubits via Holography」・KEK加速器実験施設の見学ツアーも予定しています。・詳細については下記ウェブページをご覧ください： https://staff.aist.go.jp/s-kawabata/qit/qit35 ・参加費（事前振込）：一般2,500円，学生1,000円（当日払いは+1,000円）懇親会費（事前振込）：一般3,500円，学生2,000円（当日払いは+500円）・定員：200名程度・問合せ先：筒井泉（KEK）、磯暁（KEK）、鶴丸豊広（三菱電機） E-mail: qit35(a)ml.post.kek.jp ・主催：電子情報通信学会量子情報技術時限研究専門委員会共催：応用物理学会量子エレクトロニクス研究会 ---------------------------------------------------

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 09 Sep '16

09 Sep '16

皆様ルートヴィヒ・マクシミリアン大学ミュンヘンのChuangjie Xu博士の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学系 e-mail: ishihara(a)jaist.ac.jp ----------------------------------------------- * JAIST Logic Seminar Series * * The seminar below is held as a part of JSPS Core-to-Core Program, A. Advanced Research Networks, and EU FP7 Marie Curie Actions IRSES project CORCON. (http://www.jaist.ac.jp/logic/ja/core2core, https://corcon.net/) Date: Wednesday 28 September, 2016, 15:20-17:00 Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Chuangjie Xu (Ludwig-Maximilians-Universität München) Title: Continuity in Type Theory Abstract: If all functions (N -> N) -> N are continuous then 0 = 1. We establish this in intuitionistic type theory, with existence in the formulation of continuity expressed as a Sigma-type via the Curry-Howard interpretation. But with an intuitionistic notion of anonymous existence, defined as the propositional truncation of Sigma, it is consistent that all such functions are continuous. On the other hand, any of these two intuitionistic conceptions of existence give the same, consistent, notion of uniform continuity for functions (N -> 2) -> N. Moreover, we constructively develop a model of uniform continuity and implemented it within type theory using Agda.

1 0

Workshop 参加者募集のお知らせ
by Hideki Tsuiki 07 Sep '16

07 Sep '16

Workshop 参加者募集のお知らせ (再送) Second call for participation 日本学術振興会研究拠点形成事業「数理論理学とその応用に関するワークショップ」 JSPS Core-to-Core Program "Workshop on Mathematical Logic and its Application” http://www.i.h.kyoto-u.ac.jp/~matthew/core2core2016/index.html 2016 年 9月16,17日（金, 土曜日）京都大学、吉田南キャンパス、総合人間学部棟 1401 教室 September 16--17, 2016, Faculty of Integrated Human Studies Building, room 1401 Kyoto University 北陸先端科学技術大学院大学が内外の協力機関および協力者と実施しております日本学術振興会研究拠点形成事業「数理論理学とその応用の国際拠点形成」 (http://www.jaist.ac.jp/logic/core2core) の一環として、表記のワークショップを京都で開催いたします。本拠点形成事業参加研究者のためのワークショップですが、それ以外の方もご参加いただけます。プログラムなどの情報は、上記ホームページを御覧ください。両日とも、朝 9:00 から夕方 5:30 頃まで講演がある予定です。当日参加も可能ですが、本事業参加研究者以外で参加を予定されている方は、下記フォームにて、できるだけ事前にご連絡を頂けますようにお願い申し上げます。ご質問等がございましたら、core2core2016(a)jaist.ac.jp までお寄せください。多くの方のご参加をお待ちしております。オルガナイザー：石原哉立木秀樹照井一成 Matthew de Brecht 根元多佳子 --------------------------------------- 「数理論理学とその応用に関するワークショップ」に参加します。所属：名前：

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml