Logic-ml January 2019

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

12 participants
13 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

【論文募集】Bx 2019 (Workshop on Bidirectional Transformations)【2/12アブスラクト〆切】
by Kazutaka Matsuda 31 Jan '19

31 Jan '19

複数お受けとられた方はご容赦ください．東北大学の松田です．来たる6月4日に開催される双方向変換に関する国際ワークショップ Bx 2019 のご案内を御送りいたします．〆切等の日程は以下となっております．アブストラクト〆切：2/12 (AoE) 論文〆切：2/19 (AoE) 採否通知：4/8 カメラレディ〆：5/1前後〆切まで日数が近くギリギリの案内で恐縮ですが，どうぞご投稿を検討いただければ幸いです． Bx 2019: 8th International Workshop on Bidirectional Transformations ==================================================================== Highlights: - workshop date set on June 4, 2019 - Zachary Ives confirmed as invited speaker - abstract submission in two weeks (Tuesday, Feb 12, AoE) - links to CEUR-WS.org style and template files updated * http://bx-community.wikidot.com/bx2019:home * June 4, 2019, Saint Joseph’s University, Philadelphia, PA, USA * as part of Philadelphia Logic Week (PLW) 2019: https://sites.sju.edu/plw/ * Invited speaker: Zachary Ives (University of Pennsylvania) Bidirectional transformations (bx) are a mechanism for maintaining the consistency of at least two related sources of information. Such sources can be relational databases, software models and code, or any other document following standard or ad-hoc formats. Bx are an emerging topic in a wide range of research areas, with prominent presence at top conferences in several different fields (namely databases, programming languages, software engineering, and graph transformation), but with results in one field often getting limited exposure in the others. Bx 2019 is a dedicated venue for bx in all relevant fields, and is part of a workshop series that was created in order to promote cross-disciplinary research and awareness in the area. As such, since its beginning in 2012, the workshop has rotated between venues in different fields. Bx 2019 will be a part of Philadelphia Logic Week (PLW) 2019, which also includes conference and workshops on logic, provenance, and databases, topics that we hope will complement Bx and help build engagement with these communities. Important Dates =============== - Abstract submission: Feb 12 (AoE) - Paper submission: Feb 19 (AoE) - Author notification: Apr 8 - Camera-ready: around May 1 - Workshop: Jun 4, 2019 Aims and Topics =============== The aim of the workshop is to bring together researchers and practitioners, established and new, interested in bx from different perspectives, including but not limited to: - bidirectional programming languages and frameworks - data and model synchronization - view updating - inter-model consistency analysis and repair - data/schema (or model/metamodel) co-evolution - coupled software/model transformations - inversion of transformations and data exchange mappings - domain-specific languages for bx - analysis and classification of requirements for bx - bridging the gap between formal concepts and application scenarios - analysis of efficiency of transformation algorithms and benchmarks - survey and comparison of bx technologies - case studies and tool support Submission Guidelines ===================== Papers must follow the CEUR-WS.org one-column style (with page numbers) available at - http://ceur-ws.org/Vol-XXX/samplestyles/onecolpceurws.sty and must be submitted via EasyChair: - https://www.easychair.org/conferences/?conf=bx2019 A sample LaTeX file using the above style (along with an included sample image) can be downloaded at - http://ceur-ws.org/Vol-XXX/samplestyles/paper1p.tex - http://ceur-ws.org/Vol-XXX/samplestyles/fig1.eps Five categories of submissions are considered: * Full Research Papers (up to 15 pages) - in-depth presentations of novel concepts and results - applications of bx to new domains - survey papers providing novel comparisons between existing bx technologies and approaches case studies * Tool Papers (up to 8 pages) - guideline papers presenting best practices for employing a specific bx approach (with a specific tool) - presentation of new tools or substantial improvements to existing ones - qualitative and/or quantitative comparisons of applying different bx approaches and tools * Experience Report (up to 8 pages) - sharing experiences and lessons learned with bx tools/frameworks/languages - how bx is used in (research/industrial/educational) projects * Extended Abstracts and Short Papers (up to 4 pages) - work in progress - small focused contributions - position papers and research perspectives - critical questions and challenges for bx * Talk Proposals (up to 2 pages) - proposed lectures about topics of interest for bx - existing work representing relevant contributions for bx - promising contributions that are not mature enough to be proposed as papers of the other categories If your submission is not a Full Research Paper, please include the intended submission category in the Title field of EasyChair’s submission form. The bibliography is excluded from the page limits. All papers are expected to be self-contained and well-written. Tool papers are not expected to present novel scientific results, but to document artifacts of interest and share bx experience/best practices with the community. Experience papers are expected to report on lessons learnt from applying bx approaches, languages, tools, and theories to practical application case studies. Extended abstracts should primarily provoke interesting discussion at the workshop and will not be held to the same standard of maturity as regular papers; short papers contain focused results, positions or perspectives that can be presented in full in just a few pages, and that correspondingly contain fewer results and that therefore might not be competitive in the full paper category. Talk proposals are expected to present work that is of particular interest to the community and worth a talk slot at the workshop. We strongly encourage authors to ensure that any (variants of) examples are present in the bx example repository at the time of submission, and for tool papers, to allow for reproducibility with minimal effort, either via a virtual machine (e.g., via Share - http://share20.eu) or a dedicated website with relevant artifacts and tool access. All papers will be peer-reviewed by at least three members of the program committee. If a paper is accepted, one author of the paper is expected to participate in the workshop to present it. Authors of accepted tool papers are also expected to be available to demonstrate their tool at the event. Proceedings and Special Issue ============================= The workshop proceedings, including all accepted papers (except talk proposals), will be published electronically by CEUR-WS.org. A special issue open to all authors of papers in BX workshops over the past few years is planned. Program committee ================= * Co-chairs - James Cheney, University of Edinburgh, UK - Hsiang-Shang ‘Josh’ Ko, National Institute of Informatics, Japan * Members - Leopoldo Bertossi, Carleton University, Canada - Ravi Chugh, University of Chicago, US - Zinovy Diskin, McMaster University, Canada - Paolo Guagliardo, University of Edinburgh, UK - Jules Hedges, University of Oxford, UK - Michael Johnson, Macquarie University, Australia - Leen Lambers, Hasso Plattner Institute, University of Potsdam, Germany - Kazutaka Matsuda, Tohoku University, Japan - Anders Miltner, Princeton University, US - Alfonso Pierantonio, University of L'Aquila, Italy - Perdita Stevens, University of Edinburgh, UK - Daniel Strüber, University of Koblenz and Landau, Germany - Manuel Wimmer, Vienna University of Technology, Austria - Nicolas Wu, University of Bristol, UK

1 0

[ポスター発表募集] 第21回プログラミングおよびプログラミング言語ワークショップ (PPL 2019)
by Kohei SUENAGA 29 Jan '19

29 Jan '19

皆様第21回プログラミングおよびプログラミング言語ワークショップ (PPL 2019) のプログラム共同委員長を仰せつかっております京大の末永とクックパッドの笹田です。下記の通り、ポスター発表の締め切りが「2019年2月6日 (水) 17:00 (JST)」と迫ってきましたので、ご連絡いたします。重複してお受け取りになりましたらご容赦ください。募集要項には「2時間程度のセッション内でのポスター発表またはデモ発表」とありますが、例年発表が多い割に時間が短い、というご意見もあったため、時間の延長を検討しております。カテゴリ1などの発表でご応募頂いた皆様にも、ぜひポスターで議論を深めて頂くため、ポスターにもご応募頂けますと幸いです。以上、よろしくお願いします。 On 2018/11/26 10:09, Kohei SUENAGA wrote: > PPL 2019 は 2019年3月6日 (水)～3月8日 (金) の日程で > 岩手県志戸平温泉で開催されます．実装系理論系問わず > プログラミングやプログラミング言語に関する研究をされている方は > どうぞ論文の投稿をご検討ください． > > 国内外未発表論文を募集するカテゴリ1については > 発表申込締切: 2019年12月21日 (金) 17:00 (JST) > 論文提出締切: 2019年1月7日 (月) 17:00 (JST) > となっております． > > 本年は以下の二名の方の招待講演を予定しております． > 萩谷昌己（東京大学） > 植山類（Google） ... > カテゴリ3 (ポスター・デモ発表) > ------------------------------ > 2時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発 > 表の別を問いません．PPLへの関連をもとに採否を判定いたしますが，申し込 > み多数の場合はプログラム委員会で選考致します． > > 発表申込締切: 2019年2月6日 (水) 17:00 (JST) > 採否通知：2019年2月11日 (月) -- Kohei Suenaga (末永幸平), Ph.D Associate professor (准教授) Graduate School of Informatics, Kyoto University (京都大学情報学研究科) ksuenaga(a)gmail.com http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 25 Jan '19

25 Jan '19

皆様 LMUミュンヘンのHelmut Schwichtenberg先生の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学系 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 Horizon 2020 Marie Skłodowska-Curie actions RISE project CID (http://www.jaist.ac.jp/logic/ja/core2core, http://cid.uni-trier.de/). Date: Wednesday 6 March, 2019, 15:20-17:00 Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Professor Helmut Schwichtenberg (Mathematisches Institut, LMU Muenchen) Title: Equality and extensionality Abstract: We sketch a theory of computable functionals (TCF) based on finitary algebras given by their constructors. Its intended semantics admits non-total functionals. For closed algebras of level zero we allow infinite stream-like objects. For higher types we define (pointwise) equality as a logical relation, and extensionality by diagonalization of equality. We define realizability and -- in the spirit of Kolmogorov (1932) -- add an invariance axiom: every computationally relevant (c.r.) formula A is equivalent to the existence of an extensional realizer of A. Then we can prove (ordinary and dependent) choice, and also a soundness theorem stating that the computational content extracted from a proof of a c.r. formula A realizes A.

1 0

RIMS
by arai toshiyasu 24 Jan '19

24 Jan '19

みなさま新井@千葉大です。既にご存知の方もいらっしゃると思いますが念のためお知らせします。 RIMS は昨年11月に共（同利用）・共（同研究）拠点から国際共・共拠点に衣替えしました。それに伴う拠点事業の変更の要点は： (1) 従来の拠点事業　プロジェクト研究　RIMS共同研究（公開型）　RIMS共同研究（グループ型）　RIMS合宿型セミナー　長期研究員を以下に再編する：　訪問滞在型研究（プロジェクト研究の拡大版）　RIMS共同研究（公開型）　RIMS共同研究（グループ型A, グループ型B[新規], グループ型C[新規]）　RIMS合宿型セミナー　RIMS総合研究セミナー[新規] 　長期研究員　プロジェクトフェロー[新規] 4つの[新規],は　グループ型Bは、数名による国際共同研究　グループ型Cは、外国人のみによる共同研究　総合研究セミナーは、研究者向けのチュートリアル　プロジェクトフェローは、訪問滞在型研究の　企画実施支援のために雇用されるPD (2) 上記の拠点事業の内、長期研究員とプロジェクトフェロー以外を国際公募とし、事業費による海外からの研究者の渡航費支払いを認める。 (3) グループ型Bに機動性を持たせるために、通年募集とし年3回の締切と採択を行う。詳細はRIMSのページ　http://www.kurims.kyoto-u.ac.jp/kyoten/ja/index.html でご確認下さい。尚、今年度内の追加募集も始まっています。以上、報告まで -- 新井敏康

1 0

【参加募集】第21回プログラミングおよびプログラミング言語ワークショップ（PPL2019）
by Kazuyuki ASADA 24 Jan '19

24 Jan '19

PPLの皆様（重複ご容赦ください），東北大学の浅田です． 3月6日(水) 〜 8日(金)に，岩手県花巻市で開催される，第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019) の参加登録を開始いたしましたので，ご案内いたします．多くの方々のご参加をお待ちしております．参加登録の締切は2月20日(水)です．どうぞお早めのご登録をお願い致します．あわせて，送迎バスのアンケートへのご協力をよろしくお願い致します．また，カテゴリ2 (国外既発表論文) とカテゴリ4 (サーベイ・チュートリアル発表) の発表申込締切が1月25日(金) 17:00 (JST)，カテゴリ3 (ポスター・デモ発表) の発表申込締切が2月6日(水) 17:00 (JST) となっております．これらの投稿もあわせてご検討ください． -------------------------------------------------------------------------- 第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

Talk by Ulrich Berger (17th January, 11.00-)
by Kazushige TERUI 15 Jan '19

15 Jan '19

みなさま今週木曜に京都大学にてUlrich Bergerさんによるご講演があります。詳細は下記の通りです。よろしければご参加ください。京都大学数理解析研究所照井一成 ========== Time: 11:00-12:00, 17th January, 2019 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) Speaker: Ulrich Berger (Swansea University) Title: Extracting the Fan Functional Abstract: Consider a continuous functional F : (N -> B) -> N where N is the type of natural numbers and B is the type of Booleans, both endowed with the discrete topology, and the function space N -> B carries the pointwise topology. By a compactness argument (Koenig's Lemma or Fan Theorem), F is uniformly continuous. Therefore, there exists a least modulus of uniform continuity for F, that is, a least natural number m such that F equates any two arguments that coincide below m. The mapping F |-> m is called Fan Functional. Gandy showed that the Fan Functional is computable. Later it was shown that it is computable even in the restricted sense of Kleene's schemata (S1-S9), or, equivalently, PCF. In this talk we show that the Fan Functional is the computational content of a constructive proof of the uniform continuity of F.

1 0

ENTROPY 2019: Call for Papers - Co-located with EuroS&P'19
by David Nowak 14 Jan '19

14 Jan '19

************************************************************************** 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 Co-located with EuroS&P'19, KTH, Stockholm, 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. INVITED SPEAKERS (to be extended) Frank Piessens, KU Leuven Peter Sewell, Univ. Cambridge IMPORTANT DATES Paper submission: March 11 2019 Author notification: April 10, 2019 Camera-ready versions: April 22, 2019 (strict) Workshop: 16 June 2019 SUBMISSION AND PUBLICATION There are two categories of submissions: 1. Regular papers describing fully developed work and complete results (8 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 0

FSCD 2019 Last Call for Papers
by Nao Hirokawa 11 Jan '19

11 Jan '19

皆様今年６月にドイツ・ドルトムントで開催されます、計算と演繹に関する国際会議 FSCD の論文募集の最終案内をお送り致します。是非、投稿をご検討下さい。廣川 (JAIST) --------------- Updated information: titles and abstracts of invited talks are now available --------------- CALL FOR PAPERS Fourth International Conference on Formal Structures for Computation and Deduction (FSCD 2019) 24 -- 30 June 2019, Dortmund, Germany http://easyconferences.eu/fscd2019/ IMPORTANT DATES --------------- All deadlines are midnight anywhere-on-earth (AoE); late submissions will not be considered. Titles and Short Abstracts: 8 February 2019 Full Papers: 11 February 2019 Rebuttal period: 28 March -- 1 April 2019 Authors Notification: 8 April 2019 Final version for proceedings: 22 April 2019 FSCD covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logics, models of computation (e.g. quantum computing, probabilistic computing, homotopy type theory), semantics and verification in new challenging areas (e.g. blockchain protocols or deep learning algorithms). Suggested, but not exclusive, list of topics for submission are: 1. Calculi: Rewriting systems, Lambda calculus, Concurrent calculi, Logics, Type theory, Homotopy type theory, Logical frameworks, Quantum calculi 2. Methods in Computation and Deduction: Type systems; Induction and coinduction; Matching, unification, completion and orderings; Strategies; Tree automata; Model checking; Proof search and theorem proving; Constraint solving and decision procedures 3. Semantics: Operational semantics; Abstract machines; Game Semantics; Domain theory; Categorical models; Quantitative models 4. Algorithmic Analysis and Transformations of Formal Systems: Type inference and type checking; Abstract interpretation; Complexity analysis and implicit computational complexity; Checking termination, confluence, derivational complexity and related properties; Symbolic computation 5. Tools and Applications: Programming and proof environments; Verification tools; Proof assistants and interactive theorem provers; Applications in industry (e.g. design and verification of critical systems); Applications in other sciences (e.g. biology) 6. Semantics and verification in new challenging areas: Certification; Security; Blockchain protocols; Data bases; Deep learning and machine learning algorithms; Planning INVITED SPEAKERS ----------- Titles and abstracts available at http://easyconferences.eu/fscd2019/invited-speakers/ * Beniamino Accattoli (INRIA, Paris, France) https://sites.google.com/site/beniaminoaccattoli/ * Amy Felty (University of Ottawa, Canada) http://www.site.uottawa.ca/~afelty/ * Sarah Winkler (University of Innsbruck, Austria) http://cl-informatik.uibk.ac.at/users/swinkler/ * Hongseok Yang (KAIST, Korea) https://sites.google.com/view/hongseokyang/ PUBLICATION ----------- The proceedings will be published as an electronic volume in the Leibniz International Proceedings in Informatics (LIPIcs) of Schloss Dagstuhl. All LIPIcs proceedings are open access. SUBMISSION GUIDELINES --------------------- Submissions can be made in two categories. Regular research papers are limited to 15 pages (including references, with the possibility to add an annex for technical details, e.g.\ proofs) and must present original research which is unpublished and not submitted elsewhere. System descriptions are limited to 15 pages (including references) and must present new software tools in which FSCD topics play an important role, or significantly new versions of such tools. Submissions must be formatted using the LIPIcs style files and submitted via EasyChair. Complete instructions on submitting a paper can be found on the conference web site: http://easyconferences.eu/fscd2019/ BEST PAPER AWARD BY JUNIOR RESEARCHERS -------------------------------------- The program committee will consider declaring this award to a paper in which at least one author is a junior researcher, i.e. either a student or whose PhD award date is less than three years from the first day of the meeting. Other authors should declare to the PC Chair that at least 50% of contribution is made by the junior researcher(s). SPECIAL ISSUE ------------- Authors of selected papers will be invited to submit an extended version for a special issue of Logical Methods in Computer Science. PROGRAM COMMITTEE ----------------- H. Geuvers, Radboud U. Nijmegen (Chair) Z. Ariola, U. of Oregon M. Ayala Rincón, U. of Brasilia A. Bauer, U. of Ljubljana F. Bonchi, U. of Pisa S. Broda, U. of Porto U. Dal Lago, U. of Bologna & Inria U. De'Liguoro, U. of Torino D. Kapur, U. of New Mexico P. Dybjer, Chalmers U. of Technology M. Fernandez, King's College London J. Giesl, RWTH Aachen N. Hirokawa, JAIST S. Lucas, U. Politecnica de Valencia A. Middeldorp, U. of Innsbruck F. Pfenning, Carnegie Mellon U. B. Pientka, McGill U. J. van de Pol, Aarhus U. & U. of Twente F. van Raamsdonk, VU Amsterdam C. Schürmann, ITU Copenhagen P. Severi, U. of Leicester A. Silva, U. College London S. Staton, Oxford U. T. Streicher, TU Darmstadt A. Stump, U. of Iowa N. Tabareau, Inria S. Tison, U. of Lille A. Tiu, Australian National U. T. Tsukada, U. of Tokyo J. Urban, CTU Prague P. Urzyczyn, U. of Warsaw J. Waldmann, Leipzig U. of Applied Sciences CONFERENCE CHAIR ---------------- Jakob Rehof, TU Dortmund LOCAL WORKSHOP CHAIR -------------------- Boris Düdder, U. of Copenhagen STEERING COMMITTEE WORKSHOP CHAIR -------------------------------- J. Vicary, Oxford U. PUBLICITY CHAIR --------------- Sandra Alves , Porto U. FSCD STEERING COMMITTEE ----------------------- S. Alves (Porto U.), M. Ayala-Rincón (Brasilia U.) C. Fuhs (Birkbeck, London U.) D. Kesner (Chair, Paris U.) H. Kirchner (Inria) N. Kobayashi (U. Tokyo) C. Kop (Radboud U. Nijmegen) D. Miller (Inria) L. Ong (Chair, Oxford U.) B. Pientka (McGill U.) S. Staton (Oxford U.)

1 0

CFP: Agda Implementors' Meeting XXIX (March 13 - 19 at Ochanomizu University)
by Youyou Cong 10 Jan '19

10 Jan '19

Dear all (English translation follows below), 皆様、お茶の水女子大学の叢です。第29回 Agda Implementors' Meeting (AIM XXIX) を 3月13日（水）から 3月19日（火）までの予定で、お茶の水女子大学にて開催します。このミーティングでは、定理証明支援系 Agda のユーザと開発者が言語の理論や応用、拡張などについて議論します。参加者に期待されるのは、 - 発表セッションへの貢献（任意・進行中の仕事も歓迎） - code sprints への参加の2つです。ミーティングに関する情報は、以下のページに追加していく予定です： http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXXIX 参加者と発表の概数を把握したいので、参加をご希望の方は、 3月1日（金）までにメール最下部のフォームを so.yuyu(a)is.ocha.ac.jp 宛にお送りください。多数のご参加をお待ちしております。どうぞよろしくお願いいたします。叢悠悠 We are happy to announce that the 29th Agda Implementors' Meeting (AIM XXIX) will be held at Ochanomizu University from March 13 (Wednesday) to March 19 (Tuesday). AIM provides an opportunity for the users and implementors of the Agda proof assistant to discuss the theory, applications, and extensions of the language. Participants are expected to present their work in the talk session and take part in one or more projects in the code sprint session. More information about the meeting can be found at: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXXIX If you are interested in joining the meeting, please fill out the form below and send it to so.yuyu(a)is.ocha.ac.jp by March 1 (Friday). We look forward to your participation and contribution! Best regards, Youyou -------8<-------------------------------------------------- Name: Title and abstract (if you want to give a talk or lead a discussion; optional): Suggestions for code sprints (optional): Additional comments (optional):

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml January 2019