Logic-ml

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

1792 discussions

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

ワークショップ「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 吉信康夫 20 Sep '16

20 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 吉信康夫 20 Sep '16

20 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

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml