Logic-ml

9 participants
1782 discussions

ENTROPY 2019: Second Call for Papers - Co-located with EuroS&P'19
by David Nowak 12 Mar '19

12 Mar '19

NEW: two more invited speakers ************************************************************************** Second Call for papers — ENTROPY 2019 ENabling TRust through Os Proofs … and beYond Second International workshop on the use of theorem provers for modelling and verification at the hardware-software interface https://entropy2019.sciencesconf.org Co-located with EuroS&P'19, KTH, Stockholm, June 2019 ************************************************************************** INVITED SPEAKERS Dominique Bolignano, Prove & Run Gernot Heiser, University of New South Wales Frank Piessens, KU Leuven Peter Sewell, University of Cambridge IMPORTANT DATES Paper submission: March 11 2019 Author notification: April 10, 2019 Camera-ready versions: April 22, 2019 (strict) Workshop: 16 June 2019 AIM AND SCOPE Low level software such as kernels and drivers, along with the hardware this software runs on, is critical for application security. In contrast with user applications, OS kernel software runs in privileged CPU mode and is thus highly critical. Large projects such as seL4, VeriSoft, CertiKoS and Prosper have invested considerable resources in developing formally verified systems such as hypervisors and microkernels, supplying proofs that they satisfy critical properties. Such proofs are delicate in terms of the scale and complexity of real systems, the models used in performing the proof search, and the relations between the two, which recent vulnerabilities such as Spectre and Meltdown have shown to be a highly non-trivial issue. The purpose of this workshop is to share, compare and disseminate best practices, tools and methodologies to verify OS kernels, also setting the stage for future steps in the direction of fully verified systems, dealing with issues related to modelling, model validation, and large proof maintenance through system evolution. On one hand, we need to make low-level proofs more scalable, modular and cost-effective. On the other hand, once certified systems are available, preservation and maintenance of their proofs of validity become key questions. The goal of the ENTROPY workshop is to provide a forum for researchers and practitioners in this space, linking operating systems, formal methods, and hardware architecture, interested in system design as well as machine verified mathematical proofs using proof assistants such as Coq, Isabelle and HOL4. This will be the second edition of the ENTROPY workshop series. The first workshop was organised by the Pip Development Team at University of Lille in 2018. TOPICS OF INTEREST Specific topics include, but are not limited to: * Verified kernels and hypervisors * Verified security architectures and models * Tools and frameworks for hardware security analysis * Tools and frameworks for security analysis * Formal hardware models and model validation techniques * Theorem prover based tools and frameworks for verification of low level code * Combinations of static analysis and theorem proving * Theories and techniques for compositional security analysis * Case studies and industrial experience reports * Proof maintenance techniques and problems * Compositional models and verification techniques * Proof oriented design The aim of the workshop is to stimulate innovation and active exchange of ideas, so position papers, work-in-progress and industrial experience submissions are welcome. SUBMISSION AND PUBLICATION There are two categories of submissions: 1. Regular papers describing fully developed work and complete results (10 pages, references included, IEEE format) 2. Short papers, position papers, industry experience reports, work-in-progress submissions (4 pages, references included, IEEE format) All papers should be in English and describe original work that has not been published or submitted elsewhere. The submission category should be clearly indicated. All submissions will be fully reviewed by members of the Programme Committee. Papers will appear in IEEE Xplore in a companion volume to the regular EuroS&P proceedings. For formatting and submission instructions see https://entropy2019.sciencesconf.org. PROGRAM CHAIRS Mads Dam, KTH Royal Institute of Technology David Nowak, CNRS and University of Lille PROGRAM COMMITTEE Christoph Baumann, Ericsson AB Gustavo Betarte, Univ. de la República, Uruguay David Cock, ETH Zurich Mads Dam, KTH Royal Institute of Technology (chair) Anthony Fox, ARM Deepak Garg, MPI Saarbrucken Ronghui Gu, Columbia University Samuel Hym, Univ. Lille Thomas Jensen, INRIA and Univ. Rennes Toby Murray, Univ. Melbourne David Nowak, CNRS & Univ. Lille (chair) Vicente Sanchez-Leighton, Orange Labs Thomas Sewell, Chalmers -- David Nowak http://www.cristal.univ-lille.fr/~nowakd/

1 1

LCC 2019（7月8日・パトラ）発表募集
by Akitoshi Kawamura 11 Mar '19

11 Mar '19

メーリングリストの皆様九大の河村と申します。7月に国際会議ICALPの併設集会としてギリシアのパトラで行われる「論理学と計算量」研究集会LCC 2019の御案内をお送りいたします。投稿は3～4ページで、締切は5月1日です。 =========================================================== First Call for Contributions LCC 2019 20th International Workshop on Logic and Computational Complexity July 8, 2019, Patras, Greece Collocated with ICALP 2019 http://www.cs.swansea.ac.uk/lcc/ =========================================================== LCC meetings are aimed at the foundational interconnections between logic and computational complexity, as present, for example, in implicit computational complexity (descriptive and type-theoretic methods); deductive formalisms as they relate to complexity (e.g. ramification, weak comprehension, bounded arithmetic, linear logic and resource logics); complexity aspects of finite model theory and databases; complexity-mindful program derivation and verification; computational complexity at higher type; and proof complexity. The program will consist of invited lectures as well as contributed talks selected by the Program Committee. IMPORTANT DATES: * submission May 1, 2019 * notification May 20, 2019 * workshop July 8, 2019 SUBMISSION: Submissions must be in English and in the form of an abstract of about 3-4 pages. All submissions should be submitted through Easychair at: https://easychair.org/conferences/?conf=lcc19 We also welcome submissions of abstracts based on work submitted or published elsewhere, provided that all pertinent information is disclosed at submission time. There will be no formal reviewing as is usually understood in peer-reviewed conferences with published proceedings. The program committee checks relevance and may provide additional feedback. PROGRAM COMMITTEE: Lauri Hella, Co-chair, Tampere University, Finland Monika Seisenberger, Co-chair, Swansea University, UK Sam Buss, University of California, San Diego, US Anupam Das, University of Copenhagen, Denmark Anuj, Dawar, University of Cambridge, UK Akitoshi Kawamura, Kyushu University, Fukuoka, Japan Arne, Meier, University of Hannover, Germany Lidia Tendera, University of Opole, Poland CONTACT: To contact the workshop organizers, please send an e-mail to lcc19(a)easychair.org -- 河村彰星九州大学システム情報科学研究院情報学部門〒819-0395　福岡市西区元岡744 092-802-3806 kawamura(a)inf.kyushu-u.ac.jp

1 0

Nagoya logic seminar
by 吉信康夫 05 Mar '19

05 Mar '19

皆様：名古屋大学の吉信です。先日ご案内いたしました名古屋ロジックセミナーについて、概要をいただきましたのであらためてお知らせいたします。日時：3月8日(金) 15:30〜場所：名古屋大学大学院情報学研究科棟314室講演者：渕野昌(神戸大学) タイトル：Reflection axioms which imply the continuum is very large 概要：Stationary logic の variations 対する，``妥当な'' Löwenheim-Skolem Theorem が成立するべきである，という前提のもとで，連続体の濃度は $\aleph_1$ あるいは $\aleph_2$ あるいは非常に大きなもの (weakly Mahlo, weakly hyper Mahlo 等) になるかのいずれかとなることを示す．この三分律に対応する３つの generic supercompactness axioms についても論ずる．多数の方のご参加をお待ちしております。

1 0

Re: [logic-ml] CSCAT 2019 開催案内
by Kensuke Kojima 04 Mar '19

04 Mar '19

皆様京都大学の小島です。申し込み締め切りが近づいてきましたので、 CSCAT 2019 のご案内を再送いたします。懇親会・講演申し込みの締め切りは22日（金）となっております。特に懇親会に参加を希望される方は早めにお申し込み下さい。講演につきましては枠が残っている限り22日を過ぎても受け付ける予定ですが、仮プログラム作成のため早めにお知らせいただけるとありがたいです。講演申し込み https://goo.gl/forms/DscPaYGBsIbUFDua2 懇親会申し込み https://goo.gl/forms/7cCq16mOxlV1GZ6o2 小島 2019年1月13日(日) 12:40 Kensuke Kojima <kozima(a)kuis.kyoto-u.ac.jp>: > > CSCAT メーリングリストの皆様、 > > 京都大学の小島です。 > 今年の CSCAT のお知らせです。 > > 日時： 2019年3月9日（土）〜3月10日（日） > 会場：東北大学理学部数理科学記念館（川井ホール） > URL：https://sites.google.com/view/cscat2019/home > 連絡先：cscat2019(a)grp.tohoku.ac.jp > > 今年は会場の手配を東北大学の赤間先生にお願いして、 > 講演の取りまとめを小島が行う形で開催することになりました。 > > 懇親会を3月9日の夜に行う予定です。予算は一人6000円程度の見込みです。 > > 講演・懇親会への参加を希望される方は2月22日までに、 > それぞれ以下の申し込みフォームへご記入下さい。 > （聴講のみで懇親会にも参加されない場合は申し込み不要です。） > > 講演申し込み https://goo.gl/forms/DscPaYGBsIbUFDua2 > 懇親会申し込み https://goo.gl/forms/7cCq16mOxlV1GZ6o2 > > 皆様の参加をお待ちしております。 > > 小島

1 1

seminar
by 吉信康夫 03 Mar '19

03 Mar '19

皆様名古屋大学の吉信です。以下の要領で名古屋ロジックセミナーを開催します。日時：3月8日(金) 15:30〜場所：名古屋大学大学院情報学研究科棟314室講演者：渕野昌(神戸大学) タイトル：Reflection axioms which imply the continuum is very large 多数の方のご参加をお待ちしております。

1 0

Summer School in Dynamic Epistemic Logic, Sapporo (Japan), 13-23 Aug 2019
by Katsuhiko Sano 26 Feb '19

26 Feb '19

Dear all, The Department of Philosophy at Hokkaido University (Sapporo, Japan) will hold a two-week summer school in dynamic epistemic logic and its applications, jointly with one guest lecturer, Hans van Ditmarsch, from LORIA in Nancy, between August 13 and August 23 as part of Hokkaido Summer Institute (HSI) 2019. The following two intensive courses are scheduled to be offered during the summer school. Course 1 (13/Aug/2019 - 17/Aug/2019): Introduction to Logic 2019 (For details, see https://hokkaidosummerinstitute.oia.hokudai.ac.jp/courses/CourseDetail=G096) Course 2 (19/Aug/2019 - 23/Aug/2019): Dynamic Epistemic Logic and its Applications 2019 (For details, see https://hokkaidosummerinstitute.oia.hokudai.ac.jp/courses/CourseDetail=G099) The main lecturer of Course 1 is Katsuhiko Sano (Department of Philosophy, Hokkaido University). The main lecturer of Course 2 is Hans van Ditmarsch (Lorraine Research Laboratory in Computer Science and its Applications, Centre national de la recherche scientifique, France). Tomoyuki Yamada (Hokkaido University) will also join the classes to help students follow the lectures, and communicate with the lecturers. The courses are intended for graduate students. Course 1 is meant for students without prior knowledge of logic and will prepare them for Course 2. Each course is designed to be independent from the other course. Those students who have some familiarity with basics of propositional logic, first-order logic, and modal logic can skip Course 1, and those who wish to take only Course 1 can learn basics of logic. There are several application periods for students from universities other than Hokkaido University: 1st application: ** from February 1 to February 28 2019.** 2nd application: ** from April 4 to 10 2019.** 3rd application: ** from April 26 to May 8 2019.** For more details about applications, please check the HSI official website: https://hokkaidosummerinstitute.oia.hokudai.ac.jp/applications/ As the summer in Sapporo is beautiful and pleasant, it's a good idea to learn logic this summer in Sapporo. Katsuhiko Sano Department of Philosophy Graduate School of Letters Hokkaido University

1 0

「圏論シンポジウム」開催のお知らせ; Symposium on the Categorical Unity of the Sciences
by Yoshihiro Maruyama 25 Feb '19

25 Feb '19

皆様、 Oxford大学のSamson Abramsky教授来日に際し、下記の通り圏論シンポジウムを開催いたします。登録不要ですので、お気軽にお立ち寄り下さい。 ------------------------------------------------------------------------------ 圏論シンポジウム Symposium on the Categorical Unity of the Sciences 3月22-23日、益川ホール、北部キャンパス、京都大学 22-23 March at Maskawa Hall, Kyoto University, Japan https://sites.google.com/view/categorical-unified-science/ 講演者 Speakers - Samson Abramsky (University of Oxford) - 久木田水生 (名古屋大学) - 谷村省吾 (名古屋大学) - 蓮尾一郎 (国立情報学研究所) - 春名太一 (東京女子大学) - 丸山善宏 (京都大学) - 三好博之 (京都産業大学) 事前登録/参加費不要。 No registration required. 問い合わせ先 Contact 丸山善宏（京都大学） maruyama(a)i.h.kyoto-u.ac.jp 旅費援助を希望される方は、上記までお早めにご連絡下さい。 (可能な数に限りはございます.) Limited travel funding is available; contact the organizer asap. ------------------------------------------------------------------------------ なおスケジュール詳細はウェブページの方にあります。どうぞよろしくお願い致します。丸山善宏（京都大学白眉センター）

1 0

CTFMのご案内
by 小俣安彦 22 Feb '19

22 Feb '19

皆様 CTFM主催者である彭寧寧氏(武漢理工大学)に代わり，下記のご案内をさせていただきます． Computability Theory and Foundations of Mathematics (CTFM) 昨年の明治大学での開催につづき，本年は標記国際会議が下記の日程で開催されます．日程：2019年 3月 21 日 (木) Registaration 　　　22日〜 25日 Lectures and Talks 　　　26-27日 Discussions and Excursions 場所：中国　武漢理工大学参加申し込みなどさらに詳しい情報は，次のウェブサイトをご覧ください． http://www.ctfm2019.com/index.html 講演申し込みはすでに締め切っておりますが，追加講演が認められる場合もございますので，何かご要望等がございましたら ctfm2019(a)gmail.com　までご相談ください．よろしくお願いします．田中一之（東北大学）小俣安彦（東北大学）

1 0

【参加募集(最終案内)】第21回プログラミングおよびプログラミング言語ワークショップ（PPL2019）
by Kazuyuki ASADA 19 Feb '19

19 Feb '19

PPLの皆様（重複ご容赦ください），東北大学の浅田です． 3月6日(水) 〜 8日(金)に，岩手県花巻市で開催される，第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019) の参加登録の最終案内をいたします．参加登録の締切は明日2月20日(水)です．送迎バスアンケートの締切も同日です．締切までの参加費等のお支払いを忘れずにお願いいたします．会議のプログラムを公開いたしました： https://jssst-ppl.org/workshop/2019/program.html 多くの方々のご参加をお待ちしております． -------------------------------------------------------------------------- 第21回プログラミングおよびプログラミング言語ワークショップ（PPL2019） https://jssst-ppl.org/workshop/2019/ 参加登録のご案内主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2019年3月6日(水) 〜 8日(金) 会場: 岩手県花巻市志戸平温泉「湯の杜ホテル志戸平」 PPL2019は，プログラミングとプログラミング言語に関連する幅広い分野の研究者・技術者・学生が一堂に会し，最新の研究成果の発表や，新たな研究課題の提案・討論・アイディア交換を行うことを目的とした，合宿形式の研究集会です．参加登録ならびに宿泊予約を日本旅行のウェブサービスにて受け付けております．参加費および参加登録方法については次のウェブページをご参照ください． https://jssst-ppl.org/workshop/2019/registration.html 参加登録締切：2019年2月20日(水) 問い合わせ先： ppl2019-oc(a)googlegroups.xn--com()-m53d8hra6b34cycyguk0hje6i3045cmp3h ppl2019-pc-chair(a)jssst-ppl.xn--org(/)-043e5ita1c46ctozdpfoc1401qpyjc ================================================================ ・プログラム委員会笹田耕一 (クックパッド)[プログラム共同委員長] 末永幸平 (京都大学)[プログラム共同委員長] 青谷知幸 (東京工業大学) 赤間陽二 (東北大学) 浅井健一 (お茶の水女子大学) 稲葉一浩 (Google) 鵜川始陽 (高知工科大学) 遠藤侑介 (クックパッド) Jacques Garrigue (名古屋大学) Oleg Kiselyov (東北大学) 酒井政裕 (PFN) 佐藤重幸 (東京大学) 関山太朗 (国立情報学研究所) 高野保真 (青山学院大学) 田中哲 (産業技術総合研究所) 千代英一郎 (成蹊大学) 千葉滋 (東京大学) 塚田武志 (東京大学) 照井一成 (京都大学) 中澤巧爾 (名古屋大) 林崎弘成 (Google) 平井洋一 (brainbot technologies AG) 堀江倫大 (日本IBM) 前田敦司 (筑波大学) 森畑明昌 (東京大学) 山田晃久 (国立情報学研究所) ・組織委員会浅田和之 (東北大学)[組織委員長] 平石拓 (京都大学)[組織副委員長] 木村大輔 (東邦大学)[財務担当] 森口草介 (関西学院大学)[財務副担当] 新屋良磨 (秋田大学)[会場担当] 安部達也 (千葉工業大学)[会場副担当] 佐藤亮介 (九州大学)[渉外担当] 笹田耕一 (クックパッド)[プログラム共同委員長] 末永幸平 (京都大学)[プログラム共同委員長] ================================================================

1 0

CADE-27: Second Call for Papers
by Nao Hirokawa 19 Feb '19

19 Feb '19

皆様来年８月にブラジル・ナタールで開催されます、自動演繹に関する国際会議 CADE の論文募集の案内をお送り致します。締切が少し延び、概要締切が20日、論文締切が 27 日 (AoE) となりました。是非、投稿をご検討下さい。廣川 (JAIST) --- The 27th International Conference on Automated Deduction (CADE-27) Natal, Brazil 25-30 August 2019 http://www.cade-27.info CALL FOR PAPERS CADE is the major international forum for presenting research on all aspects of automated deduction. High-quality submissions on the general topic of automated deduction, including foundations, applications, implementations, theoretical results, practical experiences and user studies are solicited. Key dates: Abstract deadline (extended): 20 February 2019 Submission deadline (extended): 27 February 2019 * Logics of interest include propositional, first-order, equational, higher-order, classical, description, modal, temporal, many-valued, constructive, other non-classical, meta-logics, logical frameworks, type theory, set theory, as well as any combination thereof. * Paradigms of interest include theorem proving, model building, constraint solving, computer algebra, model checking, proof checking, and their integration. * Methods of interest include resolution, superposition, completion, saturation, term rewriting, decision procedures, model elimination, connection methods, tableaux, sequent calculi, natural deduction, as well as their supporting algorithms and data structures, including matching, unification, orderings, induction, indexing techniques, proof presentation and explanation, proof planning. * Applications of interest include program analysis, verification and synthesis of software and hardware, formal methods, computational logic, computer mathematics, natural language processing, computational linguistics, knowledge representation, ontology reasoning, deductive databases, declarative programming, robotics, planning, and other areas of artificial intelligence. Submissions can be made in two categories: regular papers and system descriptions. The page limit in Springer LNCS style is 15 pages excluding references for regular papers and 10 pages excluding references for system descriptions. Submissions must be unpublished and not submitted for publication elsewhere. They will be judged on relevance, originality, significance, correctness, and readability. System descriptions must contain a link to a working system and will also be judged on usefulness and design. Proofs of theoretical results that do not fit in the page limit, executables of systems, and input data of experiments should be made available, via a reference to a website or in an appendix of the paper. For papers containing experimental evaluations, all data needed to rerun the experiments must be available. Reviewers will be encouraged to consider this additional material, but submissions must be self-contained within the respective page limit; considering the additional material should not be necessary to assess the merits of a submission. The review process will include a feedback/rebuttal period where authors will have the option to respond to reviewer comments. The PC chair may solicit further reviews after the rebuttal period. The proceedings of the conference will be published in the Springer LNCS/LNAI series. Formatting instructions and the LNCS style files can be obtained at http://www.springer.de/comp/lncs/authors.html At every CADE conference the Program Committee selects one of the accepted papers to receive the CADE Best Paper Award. The award recognizes a paper that the Program Committee collegially evaluates as the best in terms of originality and significance, having substantial confidence in its correctness. Overall technical quality, completeness, scholarly accuracy, and readability are also considered. Characteristics associated with a best paper include, for instance, introduction of a strong new technique or approach, solution of a long-standing open problem, introduction and solution of an interesting and important new problem, highly innovative application of known ideas or existing techniques, and presentation of a new system of outstanding power. Under exceptional circumstances, the Program Committee may give two awards (ex aequo) or give no award. IMPORTANT DATES Abstract deadline: 20 February 2019 Submission deadline: 27 February 2019 Rebuttal phase: 2 April 2019 Notification: 15 April 2019 Final version: 27 May 2019 SUBMISSION INSTRUCTIONS Papers should be submitted via https://easychair.org/conferences/?conf=cade27 CADE-27 ASSOCIATED EVENTS Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE), http://cl-informatik.uibk.ac.at/users/swinkler/arcade/ The CADE ATP System Competition, http://www.tptp.org/CASC/27/ Deduction Mentoring Workshop Logical and Semantic Frameworks, with Applications (LSFA), https://sites.google.com/view/lsfa2019 Proof eXchange for Theorem Proving (PxTP), http://pxtp.gforge.inria.fr/2019/ Theorem Prover Components for Educational Software (ThEdu'19), http://www.uc.pt/en/congressos/thedu/thedu19 The 6th Vampire Workshop CADE-27 ORGANIZERS Conference Chair: Elaine Pimentel Federal University of Rio Grande do Norte, Brazil Organizers: Carlos Olarte Federal University of Rio Grande do Norte, Brazil Joao Marcos Federal University of Rio Grande do Norte, Brazil Claudia Nalon University of Brasilia, Brazil Giselle Reis CMU, Qatar Program Committee Chair: Pascal Fontaine Universite de Lorraine, CNRS, Inria, LORIA, France Workshop, Tutorial, and Competition Chair: Giles Reger University of Manchester, UK Publicity Chair: Geoff Sutcliffe University of Miami, USA Program Committee: Carlos Areces, FaMAF - Universidad Nacional de Cordoba, Argentina Franz Baader, TU Dresden, Germany Clark Barrett, Stanford University, USA Jasmin Christian Blanchette, Vrije Universiteit Amsterdam, The Netherlands Maria Paola Bonacina, Universita degli Studi di Verona, Italy Leonardo Mendonca de Moura, Microsoft Research, USA Hans de Nivelle, Nazarbayev University, Astana, Kazakhstan Clare Dixon, University of Liverpool, UK Mnacho Echenim, Universite de Grenoble, France Marcelo Finger, University of Sao Paulo, Brazil Pascal Fontaine, Universite de Lorraine, CNRS, Inria, LORIA, France Silvio Ghilardi, Universita degli Studi di Milano, Italy Juergen Giesl, RWTH Aachen University, Germany Rajeev Gore, The Australian National University, Australia Stefan Hetzl, Technische Universitaet Wien, Austria Marijn J. H. Heule, The University of Texas at Austin, USA Nao Hirokawa, JAIST, Japan Moa Johansson, Chalmers University of Technology, Sweden Cezary Kaliszyk, University of Innsbruck, Austria Deepak Kapur, University of New Mexico, USA Benjamin Kiesl, Technische Universitaet Wien, Austria Konstantin Korovin, The University of Manchester, UK Laura Kovacs, Technische Universitaet Wien, Austria Ramana Kumar, DeepMind, UK Claudia Nalon, University of Brasilia, Brazil Vivek Nigam, Federal University of Paraiba & Fortiss, Brazil & Germany Carlos Olarte, Federal University of Rio Grande do Norte, Brazil Jens Otten, University of Oslo, Norway Andre Platzer, Carnegie Mellon University, USA Andrew Reynolds, The University of Iowa, USA Philipp Ruemmer, Uppsala University, Sweden Renate A. Schmidt, The University of Manchester, UK Stephan Schulz, DHBW Stuttgart, Germany Roberto Sebastiani, University of Trento, Italy Natarajan Shankar, SRI International, USA Viorica Sofronie-Stokkermans, Universitaet Koblenz-Landau, Germany Martin Suda, Czech Technical University, Czech Republic Geoff Sutcliffe, University of Miami, USA Rene Thiemann, University of Innsbruck, Austria Uwe Waldmann, Max Planck Institute for Informatics, Germany Christoph Weidenbach, Max Planck Institute for Informatics, Germany Sarah Winkler, University of Innsbruck, Austria

1 0

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml