Logic-ml April 2018

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

9 participants
11 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

国際会議AQIS18投稿のご案内
by NISHIMURA Harumichi 27 Apr '18

27 Apr '18

logic-mlの皆様量子情報科学におけるアジア最大の国際会議AQISが今年度は名古屋大学で開催されます．つきましては以下にCFPを送付させていただきます．皆様の積極的な投稿や参加をお待ちしております．名古屋大学大学院情報学研究科西村治道 ******************************* 18th Asian Conference on Quantum Information Science (AQIS'18) http://aqis-conf.org/2018/ 8-12 September 2018 Nagoya University, Nagoya, Japan Apologies if you receive this multiple times. Please forward to interested colleagues. We would like to draw your attention, and that of the quantum information community, to the 18th edition of the Asian Conference on Quantum Information Science (AQIS'18). AQIS is the leading conference in the subject in Asia and one of the longest-running worldwide, its highly successful predecessors having been EQIS'01-05 and AQIS'06-17. The topics covered include (but are not limited to) quantum computing, quantum information processing, quantum communication and cryptography, and foundations of quantum mechanics. This year, the conference goes for the first time to Nagoya. It will be organized by Nagoya University and will take place at the Noyori Conference Hall of Nagoya University, 8-12 September 2018. Details about the conference are to be found on the website http://aqis-conf.org/2018/ . Please check repeatedly as the information there will be updated regularly. Like its previous editions, AQIS'18 will consist of tutorials, invited talk, as well as oral and poster presentations, selected by a high-profile international program committee. Invited speakers are: Ignacio Cirac (MPQ, Garching) Keisuke Fujii (Kyoto U) Nicolas Gisin (U of Geneva) Barbara Kraus (U of Innsbruck) Yasunobu Nakamura (U of Tokyo) Sandu Popescu (U of Bristol) Robert Raussendorf (U of British Columbia) Pascale Senellart (C2N-CNRS) Wolfgang Tittel (Calgary U) Thomas Vidick (Caltech) Howard Wiseman (Griffith U) The submission deadline is 9 June 2018, 23:59 Anywhere on Earth (AoE). All submissions should follow the guidelines specified on the web site: http://aqis-conf.org/2018/submission/ We are looking forward to seeing you in Nagoya! Steering Committee Chairs: Hiroshi Imai (chair, University of Tokyo), Jaewan Kim (co-chair, KIAS) Program Committee Chairs: Antonio Acin (chair, ICFO), Jaewan Kim (co-chair, KIAS), Akihisa Tomita (co-chair, Hokkaido University) Organizing Committee Chairs: Francesco Buscemi and Harumichi Nishimura (co-chairs, Nagoya University) *************************************************

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 21 Apr '18

21 Apr '18

皆様ウィーン工科大学のMatthias Baaz先生の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学系 e-mail: ishihara(a)jaist.ac.jp ----------------------------------------------- * JAIST Logic Seminar Series * Date: Thursday 26, April, 2018, 11:00-12:30 Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Matthias Baaz (Vienna University of Technology) Title: The concept of proof Abstract: The concept of proof is one of the most fundamental building blocks of mathematics. The Hilbertian revolution at the beginning of the 20th century is based on an atomic notion of proof which is the foundation of the axiomatic method: "A proof is a finite sequence of formulas A1,..,An such that each Ai is instance of an axiom or follows by direct application of a rule from Ai1,..,Aik with all ij<i." No scientific revolution is however total, but there is a trend to disregard all alternatives to the successful method. In this lecture we discuss more global notions of proof, where subproofs are not necessarily proofs themselves. Examples are among others 1.protoproofs in the sense of Euler's famous solution to the Basel problem, which uses analogical reasoning and where additional external justifications are necessary. 2.circular notions of proof, where the concept of proof itself incooperates induction 3.sound proofs based on locally unsound rules 4.proofs based on abstract proof descriptions prominent e.g. in Bourbaki, where only the choice of a suitable result makes a verification possible. We discuss the benefits of these alternative concepts and the possibility that innovative concepts of proof adapted to the problems in question might lead to strong mathematical results and constitute a novel area of Proof Theory.

1 0

Call for Participation: FLOPS 2018 (deadline extended to April 25th)
by Koji Nakazawa 20 Apr '18

20 Apr '18

みなさま，（重複してお受取りの際は御容赦ください） 5月に名大で開催されるFLOPS 2018参加募集です． early registrationの締切が4/25 (水) まで延長されました．みなさまの御参加をお待ちしております． -- 中澤巧爾 ======================= Call For Participation ======================= FLOPS 2018: 14th International Symposium on Functional and Logic Programming In-Cooperation with ACM SIGPLAN =============================== 9-11 May, 2018, Nagoya, Japan Deadline for early registration is extended to 25 April, 2018. Registration for FLOPS 2018 is open. http://www.sqlab.jp/FLOPS2018/#registration FLOPS aims to bring together practitioners, researchers and implementors of the declarative programming, to discuss mutually interesting results and common problems: theoretical advances, their implementations in language systems and tools, and applications of these systems in practice. The scope includes all aspects of the design, semantics, theory, applications, implementations, and teaching of declarative programming. FLOPS specifically aims to promote cross-fertilization between theory and practice and among different styles of declarative programming. The list of accepted papers is at http://www.sqlab.jp/FLOPS2018/accepted.html Invited Speakers William E. Byrd (University of Alabama at Birmingham, USA) Zhenjiang Hu (National Institute of Informatics, SOKENDAI, Japan) Cédric Fournet (Microsoft) Program Committee Andreas Rossberg Google, Germany Atsushi Ohori Tohoku University, Japan Bruno C. D. S. Oliveira The University of Hong Kong, China Carsten Fuhs Birkbeck, University of London, UK Chung-chieh Shan Indiana University, USA Didier Remy INRIA, France Harald Søndergaard The University of Melbourne, Australia Jacques Garrigue Nagoya University, Japan Jan Midtgaard University of Southern Denmark, Denmark Joachim Breitner University of Pennsylvania, USA John Gallagher Roskilde University, Denmark and IMDEA Software Institute, Spain (PC co-chair) Jorge A Navas SRI International, USA Kazunori Ueda Waseda University, Japan Kenny Zhuo Ming Lu School of Information Technology, Nanyang Polytechnic, Singapore María Alpuente Universitat Politécnica de Valéncia, Spain María Garcia De La Banda Monash University, Australia Martin Sulzmann Karlsruhe University of Applied Sciences, Germany (PC co-chair) Meng Wang University of Kent, UK Michael Codish Ben-Gurion University of the Negev, Israel Michael Leuschel University of Düsseldorf, Germany Naoki Kobayashi University of Tokyo, Japan Nikolaj Bjørner Microsoft Research, USA Robert Glück University of Copenhagen, Denmark Samir Genaim Universidad Complutense de Madrid, Spain Siau Cheng Khoo National University of Singapore, Singapore Organizers Martin Sulzmann Karlsruhe University of Applied Sciences (PC co-chair) John Gallagher Roskilde University and IMDEA Software Institute (PC co-chair) Makoto Tatsuta National Institute of Informatics, Japan (General Chair) Koji Nakazawa Nagoya University, Japan (Local Chair)

1 0

Project colloquium talk by Ichiro Hasuo on 25 April
by urabenatsuki＠is.s.u-tokyo.ac.jp 19 Apr '18

19 Apr '18

[Apologies for multiple copies] Dear all, Let me advertise our next ERATO MMSD project colloquium talk by Ichiro Hasuo on 25th April, 16:00-. Please find the title and the abstract below. You are all invited. Sincerely, -- Natsuki Urabe urabenatsuki(a)is.s.u-tokyo.ac.jp The University of Tokyo, ERATO MMSD ----- Wed 25 April 2018, 16:00–17:00 ERATO MMSD Takebashi Site Common Room 3 http://group-mmm.org/eratommsd/access.html Ichiro Hasuo (National Institute of Informatics <http://www.nii.ac.jp/>), Approximating Reachability Probabilities by (Super-)Martingales Reachability is a fundamental problem in the analysis of probabilistic systems. It is well-known that reachability probabilities are efficiently computed for finite-state systems by linear programming. However, this LP method does not apply to systems that have infinitely many configurations, such as probabilistic programs and parametric systems. In such a case, we have to rely on a parametric witness (i.e. a function) for over- or under-approximating reachability probabilities. A well-studied class of such witnesses is that of supermartingales. In this talk I will talk about our recent results that refine existing supermartingale-based methods. The technical keys to those results are: choice of a suitable martingale concentration lemma for over-approximation; and a categorical axiomatization of supermartingales by coalgebras and corecursive algebras. The talk is based on my joint work with Natsuki Urabe, Masaki Hara, Bart Jacobs, Toru Takisaka and Yuichiro Oyabu.

1 0

IWC 2018: Final CfP
by KIKUCHI Kentaro 14 Apr '18

14 Apr '18

皆様、 7月にOxfordで開催される合流性に関する国際ワークショップIWC 2018 の締切が4/22まで延長されましたのでご案内をさせていただきます。ぜひご投稿をご検討ください。菊池健太郎 ----- (* Apologies for any cross-postings. *) ===================================================================== Call for Papers IWC 2018 7th International Workshop on Confluence July 7th, 2018, Oxford, United Kingdom Collocated with FSCD 2018 Part of FLoC 2018 http://cl-informatik.uibk.ac.at/events/iwc-2018/ ===================================================================== Confluence provides a general notion of determinism and is widely viewed as one of the central properties of rewriting. Confluence relates to many topics of rewriting (completion, modularity, termination, commutation, etc.) and has been investigated in many formalisms of rewriting such as first-order rewriting, lambda-calculi, higher-order rewriting, constrained rewriting, conditional rewriting, etc. Recently there is a renewed interest in confluence research, resulting in new techniques, tool support, certification as well as new applications. The International Workshop on Confluence (IWC) aims at promoting further research in confluence and related properties. IWC 2018 is collocated with FSCD 2018. Previous editions of the workshop were held in Nagoya (2012), Eindhoven (2013), Vienna (2014), Berlin (2015), Obergurgl (2016), and Oxford (2017). IMPORTANT DATES: * submission (abstract) Friday, April 20th, 2018 (extended) * submission (paper) Sunday, April 22nd, 2018 (extended) * notification Tuesday, May 15th, 2018 * final version Friday, May 25th, 2018 * workshop Saturday, July 7th, 2018 (deadlines are AoE) TOPICS: Specific topics of interest include: * confluence and related properties (unique normal forms, commutation, ground confluence) * completion * critical pair criteria * decidability issues * complexity issues * system descriptions * certification * applications of confluence INVITED SPEAKERS: * Henning Christiansen and Maja H. Kirkeby (Roskilde University, Denmark) PROGRAM COMMITTEE: * Bertram Felgenhauer (University of Innsbruck) * Jeroen Ketema (TNO-ESI) * Kentaro Kikuchi (Tohoku University) * Samuel Mimram (LIX laboratory, École Polytechnique) * Julian Nagele (Queen Mary University of London) * Jakob Grue Simonsen (University of Copenhagen) SUBMISSION: We solicit short papers or extended abstracts of at most five pages. There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers submitted elsewhere. The program committee checks relevance and may provide additional feedback. The accepted papers will be made available electronically before the workshop. The page limit for papers is 5 pages in EasyChair style. Short papers or extended abstracts must be submitted electronically through the EasyChair system at: https://www.easychair.org/conferences/?conf=iwc2018 EasyChair style: http://easychair.org/publications/for_authors

1 0

Kobe Colloquium on Logic: a talk by Prof. Philip Welch (18 April, 2018)
by Sakae Fuchino 13 Apr '18

13 Apr '18

----------------------------------------------------- Kobe Colloquium on Logic, Statistics and Informatics: ----------------------------------------------------- 以下の講演を予定しております．奮ってご参加ください． ------------------------------------------------------------------------- 日時: 2018/04/18 (水) 16.00 - 17:30 場所: 神戸大学六甲台第2キャンパス自然科学総合研究棟3号館421室講演者 Professor Philip Welch (University of Bristol) 講演題目: Global Reflection Principles 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/guid/access/rokko/rokkodai-dai2.html 連絡先：渕野昌 fuchino(a)diamond.kobe-u.ac.jp --------- Abstract: --------- This talk is based on a paper with Leon Horsten in a recent J.of Phil. and a talk in the Harvard EFI series. We reflect on the ineffability of the Cantorian Absolute. If this is done in the style of Levy and Montague in a first order manner, or Bernays using second or higher order methods this has only resulted in principles that can justify large cardinals that are `intra-constructible', that is they do not contradict the assumption that V, the universe of sets of mathematical discourse, is Gödel's universe of constructible sets, namely L. Peter Koellner has advanced reasons that this style of reflection will only have this rather limited strength. However set theorists would dearly like to have much stronger axioms of infinity. We propose a widened `Global Reflection Principle' that is based on a view of sets and Cantorian absolute infinities that delivers a proper class of Woodin cardinals (and more). A mereological view of classes is used to differentiate between sets and classes. Once allied to a wider view of structural reflection, stronger conclusions are thus possible. ------------------------------------------------------------------------- -- Best regards Sakaé Fuchino (渕野昌, Prof., Dr.rer.nat.) ----------------------------------------------------------------------------- Kobe University Graduate School of System Informatics Rokko-dai 1-1, Nada, Kobe 657-8501 Japan e-mail: fuchino(a)diamond.kobe-u.ac.jp web pages: http://fuchino.ddo.jp/index-j.html (in Japanese) http://fuchino.ddo.jp/index-e.html (in English under construction) -----------------------------------------------------------------------------

1 0

LFMTP'18: Logical Frameworks and Meta Languages: Theory and Practice - Last call for papers
by Makoto Hamana 05 Apr '18

05 Apr '18

皆様、（重複してお受け取りの際は御容赦ください） FLoC併設のLFMTP 2018 ワークショップのご案内です。ぜひ投稿をご検討ください。 -- 浜名誠群馬大学理工学府電子情報部門 ======================================================================= Call for papers Logical Frameworks and Meta-Languages: Theory and Practice LFMTP 2018 Oxford, UK, 7 July 2018 Affiliated with FSCD 2018 (part of FLoC) http://lfmtp.org/workshops/2018/ ======================================================================= Abstract submission deadline: 8 April 2018 Paper submission deadline: 15 April 2018 Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process. LFMTP 2018 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following: * Encoding and reasoning about the meta-theory of programming languages, logical systems and related formally specified systems. * Theoretical and practical issues concerning the treatment of variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures. * Logical treatments of inductive and co-inductive definitions and associated reasoning techniques, including inductive types of higher dimension in homotopy type theory * Graphical languages for building proofs, applications in geometry, equational reasoning and category theory. * New theory contributions: canonical and substructural frameworks, contextual frameworks, proof-theoretic foundations supporting binders, functional programming over logical frameworks, homotopy and cubical type theory. * Applications of logical frameworks: proof-carrying architectures, proof exchange and transformation, program refactoring, etc. * Techniques for programming with binders in functional programming languages such as Haskell, OCaml or Agda, and logic programming languages such as lambda Prolog or Alpha-Prolog. Invited Speakers * Delia Kesner (Universit Paris Diderot, France) * Kuen-Bang Hou, alias Favonia (Institute for Advanced Study, Princeton, USA) * Grigore Rosu (University of Illinois at Urbana-Champaign, USA) Important Dates Abstract submission deadline: Sunday April 8th Submission deadline: Sunday April 15th Notification to authors: Tuesday May 15th Final version due: Friday May 25th Workshop date: Saturday July 7th Submission In addition to regular papers, we accept the submission of "work in progress" reports, in a broad sense. Those do not need to report fully polished research results, but should be of interest for the community at large. Submitted papers should be in PDF, formatted using the EPTCS style guidelines. The length is restricted to 15 pages for regular papers and 8 pages for "Work in Progress" papers. Submission is via EasyChair: https://easychair.org/conferences/?conf=lfmtp18. Proceedings Accepted regular papers will be included in the proceedings of LMFTP 2018, whose mode of publication will be determined shortly. Program Committee * Mara Alpuente (Universitat Politcnica de Valncia, Spain) * Andrej Bauer (University of Ljubljana, Slovenia) * Frdric Blanqui (Inria, France), co-chair * Ana Bove (Chalmers University of Technology, Sweden) * Stphane Graham-Lengrand (CNRS, France) * Makoto Hamana (Gunma University, Japan) * Chantal Keller (Universit Paris-Sud, France) * Carlos Olarte (Universidade Federal do Rio grande do Norte, Brazil) * Giselle Reis (CMU Qatar), co-chair * Aaron Stump (University of Iowa, USA) * Yuting Wang (Yale University, USA)

1 0

(no subject)
by KUSAKARI Keiichirou 04 Apr '18

04 Apr '18

皆様，岐阜大の草刈です．複数受け取られましたらご容赦ください． 7月にイギリスで開催される停止性に関する国際ワークショップ WST(International Workshop on Termination)のCFPをお送りします．積極的な投稿とご参加をお待ちしております． ========================================================================== WST 2018 - Call for Papers 16th International Workshop on Termination July 18-19, 2018, Oxford, United Kingdom http://wst2018.webs.upv.es/ ========================================================================== The Workshop on Termination (WST) traditionally brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilization of ideas from the different communities interested in termination (e.g., working on computational mechanisms, programming languages, software engineering, constraint solving, etc.). The friendly atmosphere enables fruitful exchanges leading to joint research and subsequent publications. The workshop is held as part of the 2018 Federated Logic Conference (FLoC 2018) http://www.floc2018.org/ IMPORTANT DATES: * submission deadline: April 15, 2018 * notification: May 15, 2018 * final version due: May 31, 2018 * workshop: July 18-19, 2018 TOPICS: The 16th International Workshop on Termination welcomes contributions on all aspects of termination. In particular, papers investigating applications of termination (for example in complexity analysis, program analysis and transformation, theorem proving, program correctness, modeling computational systems, etc.) are very welcome. Topics of interest include (but are not limited to): * abstraction methods in termination analysis * certification of termination and complexity proofs * challenging termination problems * comparison and classification of termination methods * complexity analysis in any domain * implementation of termination methods * non-termination analysis and loop detection * normalization and infinitary normalization * operational termination of logic-based systems * ordinal notation and subrecursive hierarchies * SAT, SMT, and constraint solving for (non-)termination analysis * scalability and modularity of termination methods * termination analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, etc.) * well-founded relations and well-quasi-orders COMPETITION: Since 2003, the catalytic effect of WST to stimulate new research on termination has been enhanced by the celebration of the Termination Competition and its continuously developing problem databases containing thousands of programs as challenges for termination analysis in different categories, see http://termination-portal.org/wiki/Termination_Competition In 2018, the Termination Competition will run in parallel with FLoC 2018. More details will be provided in a dedicated announcement on the competition. PROGRAM COMMITTEE: Cristina Borralleras - U. de Vic Ugo Dal Lago - U. degli Studi di Bologna Carsten Fuhs - Birkbeck, U. of London Samir Genaim - U. Complutense de Madrid Juergen Giesl - RWTH Aachen Raul Gutiérrez - U. Politecnica de València Keiichirou Kusakari - Gifu University Salvador Lucas (chair) - U. Politecnica de Valencia Fred Mesnard - U. de La Reunion Aart Middeldorp - U. of Innsbruck Albert Rubio - U. Politecnica de Catalunya Rene Thiemann - U. of Innsbruck Caterina Urban - ETH Zürich INVITED SPEAKERS: tba SUBMISSION: Submissions are short papers/extended abstracts which should not exceed 5 pages. There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission. The accepted papers will be made available electronically before the workshop. Papers should be submitted electronically via the submission page: https://easychair.org/conferences/?conf=wst2018 Please, use LaTeX and the LIPIcs style file http://drops.dagstuhl.de/styles/lipics/lipics-authors.tgz to prepare your submission.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml April 2018