Logic-ml October 2016

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

8 participants
8 discussions

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 04 Oct '16

04 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

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml October 2016