Logic-ml

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

7 participants
1772 discussions

Fwd: categories: CALCO 2017: Second Call for Papers
by Ichiro Hasuo 04 Feb '17

04 Feb '17

========================================================= CALL FOR PAPERS: CALCO 2017 7th International Conference on Algebra and Coalgebra in Computer Science June 13 - 16, 2017 Ljubljana, Slovenia http://coalg.org/mfps-calco2017/ ========================================================== Abstract submission: April 3, 2017 Paper submission: April 7, 2017 Author notification: May 15, 2017 Final version due: May 31, 2017 ========================================================== -- SCOPE -- CALCO aims to bring together researchers and practitioners with interests in foundational aspects, and both traditional and emerging uses of algebra and coalgebra in computer science. It is a high-level, bi-annual conference formed by joining the forces and reputations of CMCS (the International Workshop on Coalgebraic Methods in Computer Science), and WADT (the Workshop on Algebraic Development Techniques). Previous CALCO editions took place in Swansea (Wales, 2005), Bergen (Norway, 2007), Udine (Italy, 2009), Winchester (UK, 2011), Warsaw (Poland, 2013) and Nijmegen (the Netherlands, 2015). The seventh edition will be held in Ljubljana, Slovenia, colocated with MFPS XXXIII. -- INVITED SPEAKERS -- Nicoletta Sabadini - University of Insubria, IT Alex Simpson - University of Ljubljana, SL *Joint Session with MFPS on Metrics, Privacy and Learning:* James Worrell - University of Oxford, UK (Tutorial) *Further Invited Speakers:* Catuscia Palamidessi - Ecole polytechnique, FR Vincent Danos - Ecole normale superieure, FR Marco Gaboardi - University at Buffalo, USA -- TOPICS OF INTEREST -- We invite submissions of technical papers that report results of theoretical work on the mathematics of algebras and coalgebras, the way these results can support methods and techniques for software development, as well as experience with the transfer of the resulting technologies into industrial practice. We encourage submissions in topics included or related to those listed below. * Abstract models and logics - Automata and languages - Categorical semantics - Modal logics - Relational systems - Graph transformation - Term rewriting * Specialised models and calculi - Hybrid, probabilistic, and timed systems - Calculi and models of concurrent, distributed, mobile, and context-aware computing - General systems theory and computational models (chemical, biological, etc.) * Algebraic and coalgebraic semantics - Abstract data types - Inductive and coinductive methods - Re-engineering techniques (program transformation) - Semantics of conceptual modelling methods and techniques - Semantics of programming languages * System specification and verification - Algebraic and coalgebraic specification - Formal testing and quality assurance - Validation and verification - Generative programming and model-driven development - Models, correctness and (re)configuration of hardware/middleware/architectures, - Process algebra * Corecursion in Programming Languages - Corecursion in logic / constraint / functional / answer set programming - Corecursive type inference - Coinductive methods for proving program properties - Implementing corecursion - Applications * Algebra and Coalgebra in quantum computing - Categorical semantics for quantum computing - Quantum calculi and programming languages - Foundational structures for quantum computing - Applications of quantum algebra * String Diagrams and Network Theory - Combinatorial approaches - Theory of PROPs and operads - Rewriting problems and higher-dimensional approaches - Automated reasoning with string diagrams - Applications of string diagrams - Connections with Control Theory, Engineering and Concurrency -- SUBMISSION GUIDELINES -- Prospective authors are invited to submit full papers in English presenting original research. Submitted papers must be unpublished and not submitted for publication elsewhere. Experience papers are welcome, but they must clearly present general lessons learned that would be of interest and benefit to a broad audience of both researchers and practitioners. Proceedings will be published in the Dagstuhl LIPIcs???Leibniz International Proceedings in Informatics series. Final papers should be no more than 15 pages long in the format specified by LIPIcs (http://www.dagstuhl.de/publikationen/lipics/anleitung-fuer-autoren/). It is recommended that submissions adhere to that format and length. Submissions that are clearly too long may be rejected immediately. Proofs omitted due to space limitations may be included in a clearly marked appendix. Both an abstract and the full paper must be submitted by their respective submission deadlines. A special issue of the open access journal Logical Methods in Computer Science (http://www.lmcs-online.org), containing extended versions of selected papers, is also being planned. Submissions will be handled via EasyChair https://www.easychair.org/conferences/?conf=calco2017 -- BEST PAPER AND BEST PRESENTATION AWARDS -- This edition of CALCO will feature two awards: a Best Paper Award whose recipients will be selected by the PC before the conference and a Best Presentation Award, elected by the participants. -- IMPORTANT DATES -- Abstract submission: April 3, 2017 Paper submission: April 7, 2017 Author notification: May 15, 2017 Final version due: May 31, 2017 -- PROGRAMME COMMITTEE -- Andrej Bauer (University of Ljubljana, Slovenia) Filippo Bonchi (ENS Lyon, France, co-chair) Marcello Bonsangue (University of Leiden, Netherlands) Corina Cirstea (University of Southampton, UK) Robin Cockett (University of Calgary, Canada) Andrea Corradini (University of Pisa, Italy) Sergey Goncharov (Universitaet Erlangen-Nuernberg, Germany) Helle Hvid Hansen (Delft University of Technology, Netherlands) Ichiro Hasuo (University of Tokyo, Japan) Tobias Heindel (University of Copenhagen, Denmark) Tom Hirschowitz (Savoie Mont Blanc University, France) Bart Jacobs (University of Nijmegen, Netherlands) Bartek Klin (Warsaw University, Poland) Barbara Koenig (University of Duisburg-Essen, Germany, co-chair) Alexander Kurz (University of Leicester, UK) Paul Levy (University of Birmingham, UK) Radu Mardare (Aalborg University, Denmark) Stefan Milius (Universitaet Erlangen-Nuernberg, Germany) Samuel Mimram (Ecole Polytechnique, France) Till Mossakowski (Universitaet Magdeburg, Germany) Larry Moss (Indiana University, US) Daniela Petrisan (Universite Paris-Diderot, France) John Power (University of Bath, UK) Grigore Rosu (University of Illinois, US) Jan Rutten (CWI, University of Nijmegen, Netherlands) Peter Selinger (Dalhousie University, Canada) Alexandra Silva (University College London, UK) Pawel Sobocinski (University of Southampton, UK) Ana Sokolova (University of Salzburg, Austria) -- ORGANISING COMMITTEE -- Andrej Bauer (University of Ljubljana, Slovenia) Matija Pretnar (University of Ljubljana, Slovenia) -- PUBLICITY CHAIR -- Fabio Zanasi (University College London, UK) -- SATELLITE WORKSHOPS: CALCO EARLY IDEAS AND CALCO TOOLS -- The CALCO Early Ideas Workshop is intended to enable presentation of work in progress and original research proposals. PhD students and young researchers are particularly encouraged to contribute. The CALCO Tools Workshop is dedicated to tools based on algebraic and/or coalgebraic principles. CALCO 2017 will run together with the CALCO Early Ideas Workshop, with dedicated sessions at the end of each conference day. CALCO Tools will take place on June 13. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

第28回松山TGSAセミナーのお知らせ
by Hiroshi Fujita 03 Feb '17

03 Feb '17

皆さま、第28回松山TGSAセミナーにおいて、下記のとおり、池上大祐さん（東京電機大学）の講演を予定していますのでお知らせします。皆さまのご参加をお待ちしております。　　（記）【日時】2017年2月22日(水) 16:30〜17:30 【場所】愛媛大学理学部2号館2階・大演習室(201号室) 【講演題目】 omega_1 の超コンパクト性【講演概要】集合論は無限について研究する数学の一分野である。現代数学では通常選択公理を仮定して議論を進めるが、集合論で重要な数学的対象である巨大基数の研究を進めるうえで、 "ZF+決定性公理" を初めとする選択公理の否定を導く集合論の公理系について考察するのが重要であることがここ三十年ほどで明らかになってきた。この講演では、集合論や巨大基数について紹介した後、選択公理の否定を導く巨大基数の性質について考察する。特に、omega_1（可算でない最小の無限基数）が超コンパクト基数という巨大基数になっているとき、実数直線にどのような影響があるかについて議論する。この研究は Nam Trang 氏との共同研究である。　　（以上です） -- 追記：松山TGSAセミナーは、「一般トポロジー・幾何学・集合論およびその応用」を広く扱うセミナーで、原則として月に１回、愛媛大学において開催されています。これまでの講演の記録はWeb http://www.math.sci.ehime-u.ac.jp/MGTSA.ja.html でご覧になれます。 -- 愛媛大学理学部藤田博司 <fujita.hiroshi.mh(a)ehime-u.ac.jp>

1 0

Talk by Marc Bagnol (9 Feb 11:00-)
by Tetsuya Sato 30 Jan '17

30 Jan '17

京都大学数理解析研究所の佐藤です。 2月9日11:00から、東京大学のMarc Bagnol氏に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 9 Feb, 2017 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: Marc Bagnol (JSPS Postdoctoral Fellow, University of Tokyo) Title: Multiplicative-Additive Proof Equivalence is Logspace-complete Abstract: Given a logic presented in a sequent calculus, a natural question is that of equivalence of proofs: to determine whether two given proofs are equated by any denotational semantics, i.e. any categorical interpretation of the logic compatible with its cut-elimination procedure. This notion can usually be captured syntactically by a set of rule permutations. Very generally, proofnets can be defined as combinatorial objects which provide canonical representatives of equivalence classes of proofs. In particular, the existence of proof nets for a logic provides a solution to the equivalence problem of this logic. In certain fragments of linear logic, it is possible to give a notion of proofnet with good computational properties, making it a suitable representation of proofs for studying the cut-elimination procedure, among other things. It has recently been proved that there cannot be such a notion of proofnets for the multiplicative (with units) fragment of linear logic, due to the equivalence problem for this logic being Pspace-complete. We will investigate the multiplicative-additive (without unit) fragment of linear logic and see it is closely related to binary decision trees: we can build a representation of proofs based on binary decision trees, reducing proof equivalence to decision tree equivalence. We will see as a consequence that the proof equivalence problem multiplicative-additive linear logic is Logspace-complete.

1 0

Kusatsu_Seminar_2017
by Naosuke MATSUDA 29 Jan '17

29 Jan '17

みなさま神奈川大学の松田と申します．毎年草津セミナーハウスで開催されている，ラムダ計算と論理の早春セミナーを，今年も開催することになりましたので連絡させていただきます．日程：2017年3月16日-3月20日場所：国立大学草津セミナーハウス詳細等は， http://www.geocities.jp/naosuke_not_good/event/lls_spring_2017.html にあります．研究打ち合わせ・学生の発表練習の場など，様々な用途でお使いいただければと思います．質問等ございましたら，松田（神奈川大学）までお気軽にお問い合わせください． -- Naosuke Matsuda, Dept. of Information Sciences Kanagawa University 2946, Tsuchiya, Hiratsuka-shi, Kanagawa, 259-1293, JAPAN matsuda.naosuke(a)gmail.com -- ------------------------------ Naosuke Matsuda, Dept. of Information Sciences Kanagawa University Tsuchiya 2946, Hiratsuka-shi, Kanagawa 259-1293, Japan

1 0

TABLEAUX 2017, Brasilia (Brazil), 25-28 Sep 2017
by Katsuhiko Sano 24 Jan '17

24 Jan '17

Apologies for multiple postings. ------------------------------------------------------------------------------------------- SECOND CALL FOR PAPERS TABLEAUX 2017 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods University of Brasilia, Brazil September 25-28, 2017 Submission Deadline: 25 Apr 2017 http://tableaux2017.cic.unb.br/ GENERAL INFORMATION TABLEAUX is the main international conference at which research on all aspects, theoretical foundations, implementation techniques, systems development and applications, of the mechanization of tableau-based reasoning and related methods is presented. As the first TABLEAUX workshop was held in Lautenbach in 1992, this year's conference will include special events celebrating 25 years of TABLEAUX. The conference will be held in Brasilia from 25-28 September 2017. It will be co-located with both the 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017) and the 8th International Conference on Interactive Theorem Proving (ITP 2017). TOPICS Tableau methods offer a convenient and flexible set of tools for automated reasoning in classical logic, extensions of classical logic, and a large number of non-classical logics. For large groups of logics, tableau methods can be generated automatically. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, teaching, and system diagnosis. Topics of interest include but are not limited to: * tableau methods for classical and non-classical logics (including first-order, higher-order, modal, temporal, description, hybrid, intuitionistic, substructural, relevance, non-monotonic logics) and their proof-theoretic foundations; * related methods (SMT, model elimination, model checking, connection methods, resolution, BDDs, translation approaches); * sequent calculi and natural deduction calculi for classical and non-classical logics, as tools for proof search and proof representation; * flexible, easily extendable, light weight methods for theorem proving; * novel types of calculi for theorem proving and verification in classical and non-classical logics; * systems, tools, implementations, empirical evaluations and applications (provers, logical frameworks, model checkers, ...); * implementation techniques (data structures, efficient algorithms, performance measurement, extensibility, ...); * extensions of tableau procedures with conflict-driven learning, generation of proofs; compact (or humanly readable) representation of proofs; * decision procedures, theoretically optimal procedures; * applications of automated deduction to mathematics, software development, verification, deductive and temporal databases, knowledge representation, ontologies, fault diagnosis or teaching. We also welcome papers describing applications of tableau procedures to real world examples. Such papers should be tailored to the tableau community and should focus on the role of reasoning, and logical aspects of the solution. CELEBRATING 25 YEARS To celebrate 25 years TABLEAUX the conference will include a special session of invited talks by: Reiner Haehnle Technische Universitaet Darmstadt, Germany Wolfgang Bibel Technische Universitaet Darmstadt, Germany INVITED SPEAKERS: Carlos Areces FaMAF - Universidad Nacional de Cordoba, Argentina Katalin Bimbo University of Alberta, Canada (joint with FroCoS and ITP) Jasmin Blanchette Inria and LORIA, Nancy, France (joint with FroCoS and ITP) Cesary Kaliszyk Universitaet Innsbruck, Austria (joint with FroCoS and ITP) WORKSHOPS AND TUTORIALS There will be a three-day programme of four workshops and four tutorials from 23-25 September. Workshops: 12th Logical and Semantic Frameworks with Applications (LSFA 2017) Sandra Alves, Renata Wassermann, Flavio L. C. de Moura 23 and 24 September 2017 Proof eXchange for Theorem Proving (PxTP) Catherine Dubois, Bruno Woltzenlogel Paleo 23 and 24 September 2017 EPS - Encyclopedia of Proof Systems Giselle Reis, Bruno Woltzenlogel Paleo 24 and 25 September 2017 DaLi - Dynamic Logic: new trends and applications Mario Benevides, Alexandre Madeira 24 September 2017 Tutorials: General methods in proof theory for modal and substructural logics Bjoern Lellmann, Revantha Ramanayake 23 September 2017 From proof systems to complexity bounds Anupam Das 24 September 2017 Proof Compressions and the conjecture NP =3D PSPACE Lew Gordeev, Edward Hermann Haeusler 25 September 2017 PVS for Computer Scientists Cesar Munoz, Mauricio Ayala-Rincon, Mariano Moscato 25 September 2017 Details will be published in separate calls and on the conference website. PUBLICATION DETAILS The conference proceedings will be published in the Springer LNAI/LNCS series, as in previous editions. SUBMISSIONS Submissions are invited in two categories: A Research papers, which describe original theoretical research, original algorithms, or applications, with length up to 15 pages. B System descriptions, with length up to 9 pages. Submissions will be reviewed by the PC, possibly with the help of external reviewers, taking into account readability, relevance and originality. For category A, theoretical results and algorithms must be original, and not submitted for publication elsewhere. Submissions will be reviewed taking into account correctness, theoretical elegance, and possible implementability. For category B submissions, a working implementation must be accessible via the internet, which includes sources. The aim of a system description is to make the system available in such a way that users can use it, understand it, and build on it. Accepted papers in both categories will be published in the conference proceedings. Papers must be edited in LaTeX using the llncs style and must be submitted electronically as PDF files via the EasyChair system: https://easychair.org/conferences/?conf=3Dtableaux2017. For all accepted papers at least one author is required to attend the conference and present the paper. A paper title and a short abstract of about 100 words must be submitted before the paper submission deadline. Further information about paper submissions will be made available at the conference website. Be aware that neither plagiarism, nor self-plagiarism, nor duplicate publication is acceptable. Formatting instructions and the LNCS style files can be obtained via http://www.springer.com/br/computer-science/lncs/conference-proceedings-gui= delines BEST PAPER AWARD The TABLEAUX 2017 Best Paper Award will be presented to the best submission nominated and chosen by the Program Committee among the accepted papers. The eligibility criteria will place emphasis on the originality and significance of the contribution, but readability and the overall technical quality, including correctness and completeness of results, will also be considered. The TABLEAUX Best Paper Award was established in 2015 and is a permanent initiative of TABLEAUX. IMPORTANT DATES 18 Apr 2017 Abstract submission 25 Apr 2017 Paper submission 8 Jun 2017 Notification of paper decisions 3 Jul 2017 Camera-ready papers due 23-25 Sep 2017 Workshops & Tutorials 25-28 Sep 2017 TABLEAUX Conference PROGRAM COMMITTEE Peter Baumgartner National ICT Australia, Canberra Maria Paola Bonacina Universita degli Studi di Verona Laura Bozzelli Universidad Politecnica de Madrid Torben Brauener Roskilde University Serenella Cerrito Ibisc, Universite d'Evry Val d'Essonne Agata Ciabattoni Technische Universitaet Wien Clare Dixon University of Liverpool Pascal Fontaine LORIA, INRIA, Universite de Lorraine Didier Galmiche LORIA, Universite de Lorraine Martin Giese Universitetet i Oslo Laura Giordano DISIT, Universita del Piemonte Orientale Rajeev Gore The Australian National University Volker Haarslev Concordia University George Metcalfe Universitaet Bern Angelo Montanari Universita degli Studi di Udine Barbara Morawska Technische Universitaet Dresden Boris Motik University of Oxford Leonardo de Moura Microsoft Research Neil Murray SUNY at Albany Claudia Nalon Universidade de Brasilia Linh Anh Nguyen Uniwersytet Warszawski Hans de Nivelle Uniwersytet Wroclawski Nicola Olivetti LSIS, Aix-Marseille Universite Jens Otten Universitetet i Oslo Valeria de Paiva Nuance Communications Nicolas Peltier Centre National de la Recherche Scientifique, Laboratoire d'Informatique de Grenoble Elaine Pimentel Universidade Federal do Rio Grande do Norte Giselle Reis Carnegie Mellon University-Qatar Philipp Ruemmer Uppsala Universitet Katsuhiko Sano Hokkaido University Renate Schmidt The University of Manchester Cesare Tinelli The University of Iowa Alwen Tiu Nanyang Technological University David Toman University of Waterloo Josef Urban Ceske vysoke uceni technicke v Praze LOCAL CONFERENCE ORGANIZATION COMMITTEE Claudia Nalon, Universidade de Brasilia, Brazil Daniele Nantes Sobrinho, Universidade de Brasilia, Brazil Elaine Pimentel, Universidade Federal do Rio Grande do Norte, Brazil Joao Marcos, Universidade Federal do Rio Grande do Norte, Brazil CONFERENCE CHAIR Claudia Nalon, University of Brasilia, Brazil PC CHAIRS Claudia Nalon, University of Brasilia, Brazil Renate Schmidt, The University of Manchester, UK

1 0

第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）参加募集
by Isao Sasano 24 Jan '17

24 Jan '17

皆様芝浦工業大学の篠埜です。第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）のご案内です。以下のweb pageで参加登録を開始いたしました。参加登録の締切は 2月21日（火）です。 https://ppl2017.ipl-e.ai.kyutech.ac.jp/registration/ カテゴリ2（国外既発表論文）およびカテゴリ4（サーベイ・チュートリアル発表）の発表申込締切も近づいております。カテゴリ2 発表申込締切: 2017年1月25日(水) 17:00 (JST) カテゴリ4 発表申込締切: 2017年1月25日(水) 17:00 (JST) 是非、発表申込、参加登録をお願いいたします。篠埜　功 -- Isao Sasano <sasano(a)sic.shibaura-it.ac.jp>

1 0

ITP 2017 - 2nd Call for Papers
by Nao Hirokawa 24 Jan '17

24 Jan '17

皆様９月にブラジリアで開催されます、対話的定理証明に関する国際会議 ITP 2017 の論文募集案内をお送り致します。ぜひ投稿をご検討下さい。廣川 (JAIST) -------------------------------------------------------------------- SECOND CALL FOR PAPERS ITP 2017 8th International Conference on Interactive Theorem Proving Brasilia, Brazil September 26-29, 2017 http://itp2017.cic.unb.br SUBMISSION DEADLINES * April 3, 2017 (abstracts) * April 10, 2017 (full papers) GENERAL INFORMATION The ITP conference series is concerned with all topics related to interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. ITP is the evolution of the TPHOLs conference series to the broad field of interactive theorem proving. TPHOLs meetings took place every year from 1988 until 2009. The eighth ITP conference, ITP 2017, will be held at Universidade de Brasilia, September 26-29, 2017. SCOPE OF CONFERENCE ITP welcomes submissions describing original research on all aspects of interactive theorem proving and its applications. Suggested topics include but are not limited to the following: * formal aspects of hardware and software * formalizations of mathematics * improvements in theorem prover technology * user interfaces for interactive theorem provers * formalizations of computational models * verification of security algorithms * use of theorem provers in education * industrial applications of interactive theorem provers * concise and elegant worked examples of formalizations (proof pearls) PUBLICATION DETAILS The proceedings of the symposium will be published in the Springer's LNCS series. PAPER SUBMISSIONS All submissions must be original, unpublished, and not submitted concurrently for publication elsewhere. Furthermore, when appropriate, submissions are expected to be accompanied by verifiable evidence of a suitable implementation, such as the source files of a formalization for the proof assistant used. Submissions should be no more than 16 pages in length and are to be submitted in PDF via EasyChair at the following address: https://easychair.org/conferences/?conf=itp2017 Submissions must conform to the LNCS style in LaTeX. Authors of accepted papers are expected to present their paper at the conference and will be required to a sign copyright release form. In addition to regular papers, described above, there will be a rough diamond section. Rough diamond submissions are limited to 6 pages and may consist of an extended abstract. They will be refereed and be expected to present innovative and promising ideas, possibly in an early form and without supporting evidence. Accepted diamonds will be published in the main proceedings and will be presented as short talks. After the conference the authors of selected papers will be invited to submit revised papers for a special issue of the Journal of Automated Reasoning. IMPORTANT DATES Abstract submission deadline: April 3, 2017 Full paper submission deadline: April 10, 2017 Author notification: June 2, 2017 Camera-ready papers: June 30, 2017 Workshops & Tutorials: September 23-25, 2017 Conference: September 26-29, 2017 INVITED SPEAKERS Moa Johansson, Chalmers University of Technology, Sweden Leonardo de Moura, Microsoft Research Katalin Bimbo, University of Alberta, Canada (joint with TABLEAUX and FroCos) Jasmin Blanchette Inria and LORIA, Nancy, France (joint with TABLEAUX and FroCos) Cesary Kaliszyk Universitaet Innsbruck, Austria (joint with TABLEAUX and FroCos) WORKSHOPS AND TUTORIALS There will be a three-day programme of four workshops and four tutorials from 23-25 September. Workshops: 12th Logical and Semantic Frameworks with Applications (LSFA 2017) Sandra Alves, Renata Wassermann, Flavio L. C. de Moura 23 and 24 September 2017 Proof eXchange for Theorem Proving (PxTP) Catherine Dubois, Bruno Woltzenlogel Paleo 23 and 24 September 2017 EPS - Encyclopedia of Proof Systems Giselle Reis, Bruno Woltzenlogel Paleo 24 and 25 September 2017 DaLi - Dynamic Logic: new trends and applications Mario Benevides, Alexandre Madeira 24 September 2017 Tutorials: General methods in proof theory for modal and substructural logics Bjoern Lellmann, Revantha Ramanayake 23 September 2017 From proof systems to complexity bounds Anupam Das 24 September 2017 Proof Compressions and the conjecture NP =3D PSPACE Lew Gordeev, Edward Hermann Haeusler 25 September 2017 PVS for Computer Scientists Cesar Munoz, Mauricio Ayala-Rincon, Mariano Moscato 25 September 2017 Details will be published in separate calls and on the conference website. PROGRAM COMMITTEE CHAIRS Mauricio Ayala-Rincon, U. Brasilia Cesar Munoz, NASA PROGRAM COMMITTEE CHAIRS Maria Alpuente, T.U. Valencia Vander Alves, U. Brasilia June Andronick, Data61, CSIRO, UNSW Jeremy Avigad, Carnegie Mellon U. Sylvie Boldo, INRIA LRI Ana Bove, Chalmers & Gothenburg U. Adam Chlipala, MIT Gilles Dowek, INRIA, ENS Cachan Aaron Dutle, NASA Amy Felty, U. Ottawa Marcelo Frias, I.T. Buenos Aires Ruben Gamboa, U. Wyoming Herman Geuvers, Radboud U. Elsa Gunter, U. Illinois U.C. John Harrison, Intel Corporation Nao Hirokawa, JAIST Matt Kaufmann, U. Texas Austin Mark Lawford, McMaster U. Andreas Lochbihler, ETH Zurich Assia Mahboubi, INRIA Panagiotis Manolios, Northeastern U. Gopalan Nadathur, U. Minnesota Keiko Nakata, SAP Potsdam Adam Naumowicz, U. Bialystok Tobias Nipkow, T.U. Munich Scott Owens, U. Kent Sam Owre, SRI Lawrence Paulson, U. Cambridge Leila Ribeiro, U.F. Rio Grande do Sul Claudio Sacerdoti Coen, U. Bologna Augusto Sampaio, U.F. Pernambuco Monika Seisenberger, Swansea U. Christian Sternagel, U. Innsbruck Sofiene Tahar, Concordia U. Christian Urban, King's College London Josef Urban, Czech T.U. Prague CONTACT INFORMATION Cesar Munoz Mauricio Ayala-Rincon itp2017(a)easychair.org http://itp2017.cic.unb.br

1 0

セミナー案内
by KASHIMA Ryo 21 Jan '17

21 Jan '17

数理論理学セミナーのお知らせ日時：1月20日(金) 17:00から場所：東京工業大学大岡山西８号館Ｗ棟10階 W1008 話者：竹内泉（産総研）題目：数学と変数概要：　これは数学の言語哲学の研究である。変数の使用は数学の言語に特有であるので変数の使用を分析することによって数学の本質に迫ることを目標とする。数学の変数の使用には幾つもの種類がある。本発表では、以下のような分類に沿って説明する。 (1)恒等式の文字 (2)方程式の未知数 (3)多項式論の変数と命題変数 (4)座標変数と確率変数 (5)独立変数と従属変数 ------ 本セミナーは定期的に東工大で開催しているものです。初めて参加を希望される方はご一報ください。 ----- 鹿島亮東京工業大学情報理工学院数理・計算科学系 kashima(a)is.titech.ac.jp

1 1

DICE-FOPARA 2017: Call for Papers
by Nao Hirokawa 18 Jan '17

18 Jan '17

皆様 ETAPS 2017 に併設されます、暗黙計算量 (ICC) とリソース解析に関する合同ワークショップ DICE-FOPARA 2017 の論文募集の案内をお送り致します。ぜひ投稿をご検討下さい。廣川 (JAIST) ------------------------------------------------------------------------------------------- 8th Workshop on Developments in Implicit Computational complExity and 5th Workshop on Foundational and Practical Aspects of Resource Analysis (DICE-FOPARA 2017) Affiliated with ETAPS 2017 April 22 - 23, 2017, Uppsala, Sweden http://cbr.uibk.ac.at/events/dice-fopara ------------------------------------------------------------------------------------------- OBJECTIVES The first joint international workshop on Developments in Implicit Computational complExity (DICE) and FOundational and Practical Aspects of Resource Analysis (FOPARA) will be held in Uppsala, Sweden, from April 22-23, 2017 as part of ETAPS. The DICE workshop explores the area of Implicit Computational Complexity (ICC), which grew out from several proposals to use logic and formal methods to provide languages for complexity-bounded computation (e.g. Ptime, Logspace computation). It aims at studying the computational complexity of programs without referring to external measuring conditions or a particular machine model, but only by considering language restrictions or logical/computational principles entailing complexity properties. The FOPARA workshop serves as a forum for presenting original research results that are relevant to the analysis of resource (e.g. time, space, energy) consumption by computer programs. The workshop aims to bring together the researchers that work on foundational issues with the researchers that focus more on practical results. Therefore, both theoretical and practical contributions are encouraged. We also encourage papers that combine theory and practice. Given the complementarity and the synergy between these two communities, and following the successful experience of co-location of DICE-FOPARA 2015 in London at ETAPS 2015, we will hold the 8th Workshop on DICE and the 5th Workshop on FOPARA together at ETAPS 2017. TOPICS he joint international DICE-FOPARA workshop serves as a forum for presenting original and established research results that are relevant to the implicit computational complexity theory and to the analysis of resource (e.g. time, space, energy) consumption by computer programs. The workshop aims to bring together the researchers that work on foundational issues with the researchers that focus more on practical results. Therefore, both theoretical and practical contributions are encouraged, as well as papers that combine theory and practice. Areas of interest to the workshop include, but are not limited to, the following: * type systems for controlling/inferring/checking complexity * logical and machine-independent characterisations of complexity classes * logics closely related to complexity classes * linear logic * semantics of complexity-bounded computation * rewriting and termination orderings * interpretation-based methods for implicit complexity * programming languages for complexity-bounded computation * theoretical foundations of program complexity analysis * application of implicit complexity to security * resource static analysis for embedded or/and critical systems; * semantic methods to analyse resources, including quasi-interpretations; * practical applications of resource analysis; * resource analysis by term and graph rewriting. SUBMISSIONS We ask for submission of *regular papers* describing original work (10-15 pages) or *extended abstracts* (2-6 pages) presenting already published work or work in progress. With respect to regular papers, submissions will be in particular verified for originality and novelty and the manuscript must not have been published, nor is presently submitted, elsewhere. With respect of submissions of extended abstracts already published manuscripts are acceptable, but have to be within the scope of the workshop and potentially give rise to lively discussions during the meeting. After the workshop we plan to edit a special issue of DICE-FOPARA 2017 in a renown journal in conjunction with the 7th Workshop on Developments in Implicit Computational complExity (DICE 2016). Regular papers must be prepared using the LaTeX EPTCS class (see http://eptcs.org/). Accepted regular papers will appear in an EPTCS volume (application pending). Papers should be submitted electronically via the submission page: https://easychair.org/conferences/?conf=dicefopara2017 IMPORTANT DATES Paper submission February 19, 2017 Notification March 19, 2017 Final versions due March 26, 2017 Workshop date April 22-23, 2017 CONFERENCE VENUE The workshop will be held as a satellite workshop of European Joint Conferences on Theory and Practice of Software 2017 (ETAPS 2017) which takes place in Uppsala, Sweden. PROGRAM COMMITTEE Beniamino Accattoli (Paris) Guillaume Bonfante (Nancy, co-chair) Marko van Eekelen (Nijmegen) Marco Gaboardi (Buffalo) Dan Ghica (Birmingham) Clemens Grelck (Amsterdam) Charles Grellois (Bologna) Nao Hirokawa (JAIST) Jan Hoffmann (CMU) Thomas Jensen (Rennes) Björn Lisper (Mälardalen) Hans-Wolfgang Loidl (Edinburgh) Georg Moser (Innsbruck, co-chair) Kazushige Terui (Kyoto) Simon Wegener (Saarbrücken) Florian Zuleger (Vienna)

1 0

第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）論文募集/発表募集
by Isao Sasano 17 Jan '17

17 Jan '17

皆様芝浦工業大学の篠埜です。第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）のご案内です。カテゴリ2（国外既発表論文）およびカテゴリ4（サーベイ・チュートリアル発表）の発表申込締切が近づいてまいりました。カテゴリ2 発表申込締切: 2017年1月25日(水) 17:00 (JST) カテゴリ4 発表申込締切: 2017年1月25日(水) 17:00 (JST) 是非、発表申込をお願いいたします。 ====================================================================== 第19回プログラミングおよびプログラミング言語ワークショップ (PPL2017) https://ppl2017.ipl-e.ai.kyutech.ac.jp/ 論文募集/発表募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2017年3月8日(水)～3月10日(金) 会場: 山梨県笛吹市石和温泉「華やぎの章慶山」 PPL2017は，プログラミングとプログラミング言語に関連する幅広い分野の研究者・技術者・学生が一堂に会し，最新の研究成果の発表や，新たな研究課題の提案・討論・アイディア交換を行うことを目的とした，合宿形式の研究集会です．プログラミング方法論，プログラミング言語の理論・設計・実装などに関する研究発表を，カテゴリ別に幅広く募集します．カテゴリ1: 国内外で未発表の論文の発表カテゴリ2: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ3: ポスター・デモ発表(既発表・未発表の別を問いません) カテゴリ4: サーベイ・チュートリアル発表(既発表・未発表の別を問いません) カテゴリ1の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また全論文発表と全ポスター・デモのなかから，聴衆の投票によりそれぞれ，最も優秀な論文プレゼンテーションには発表賞(一般の部，学生の部，既受賞者は除く)，最も優秀なポスター・デモにはポスター賞を授与する予定です．カテゴリ1 (国内外未発表論文) ---------------------------- 完成した理論やシステムの研究発表のみならず，萌芽的なアイディアや問題点の提示等も歓迎します．発展途上の研究内容も積極的に採録する方針です(ただし，PPLでの発表として相応しくないと判断される場合は，この限りではありません)．また，カテゴリ1で発表された研究については，会場での討議や査読コメントをもとにその完成度を高め，将来の学術雑誌・国際会議等での業績に結び付けることを奨励しています．そのため，予稿集の配布は参加者のみへの限定的なものとします．カテゴリ1で発表された研究のうち，PPL2017プログラム委員会により優れていると認められたものは， PPL2017終了後(2017年4月下旬予定)，「コンピュータソフトウェア」誌のPPL2017推薦論文としての投稿が可能です．推薦論文は，PPLプログラム委員が引き続き査読を行うことによる，迅速な査読プロセスを特長としています．カテゴリ2 (国外既発表論文) -------------------------- 査読付の国際会議または学術雑誌等で既発表であるが国内では未発表である研究を紹介する場です．採録決定済みの研究も含みます．PPLへの関連をもとに採否を判定いたしますが，申し込み多数の場合はプログラム委員会で選考致します．カテゴリ3 (ポスター・デモ発表) ------------------------------ 2時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採否を判定いたしますが，申し込み多数の場合はプログラム委員会で選考致します．会場の状況により，ポスターの常設展示を可能とします．ショートプレゼンテーションは行いません．カテゴリ4 (サーベイ・チュートリアル発表) ---------------------------------------- 研究動向の紹介(発表者の研究も含む) や分野間の相互理解と参加者の知識の底上げとなる発表を募集します．既発表・未発表の別を問いません．発表後，発表スライドをPPL2017ウェブページ上にて公開して頂く予定です．PPLへの関連，著者の研究発表実績，トピックや切り口の興味深さをもとに，プログラム委員会で選考致します．招待講演 -------- 神谷年洋（島根大学教授）原田康徳（合同会社デジタルポケット代表）以上お二方の招待講演を予定しております．なお，PPL2017の終了は昼頃〜夕刻を予定しています． ====================================================================== 投稿・発表申込要領すべてのカテゴリの投稿・発表について，次のURLから申し込んでください． https://easychair.org/conferences/?conf=ppl2017 申込にあたってはEasyChairのアカウントが必要です．4つのカテゴリそれぞれに対する申込要領の詳細は以下の通りです．申し込み時にEasychairで入力する氏名，所属の情報はプログラム作成に用いますので，参加者の便宜を考慮し，日本語が良いと考えられる場合には日本語での入力をお願い致します．最新の情報は上記ウェブページでご確認ください．カテゴリ1 (国内外未発表論文) --------------------------- 投稿手続きは2段階です．発表申込を行った上で論文提出を行ってください．発表申込締切: 2016年12月21日(水) 17:00 (JST) 著者名，所属，論文タイトル，論文概要(日本語300〜400字程度もしくは英語200 words 程度)，キーワード(3つ以上)を提出してください．論文提出締切: 2017年1月11日(水) 17:00 (JST) 10ページ程度(最大15ページ，参考文献を含む)の論文(日本語もしくは英語，PDF形式．PPL2017ウェブページにて指定のスタイルファイルを利用のこと)を提出してください．最大ページ数を超える付録は投稿版に入れて構いませんが，最終原稿においては削除してもらいます．著者のweb page等においてソースコードや実験データなどを載せて引用しても構いません．最大ページ数を超える付録やweb page等の情報については査読において考慮されない場合もあります．採否通知：2017年2月3日(金) 最終原稿締切: 2017年2月16日(木) 採録された論文の最終原稿の提出方法は，採否通知にてお知らせいたします． (注) 採録された論文等著作物は，日本ソフトウェア科学会著作権規定にもとづいて利用されますので，予めご確認ください． (注) 投稿論文と類似の論文を，他の会議(予稿集を出版するもの)・論文誌などに同時投稿する場合は，査読の有無に関わらず，その旨を発表申込および論文提出の際に明記してください．PPLでは同時投稿の事実のみをもって論文を不採録とすることはありませんが，採否の決定に利用する場合があります(他の会議との重複を避けるため，発表内容についての条件付採録とすることもあります)．カテゴリ2 (国外既発表論文) ------------------------- 発表申込時に採録が決定している国際会議および国際学術雑誌等の発表論文が対象です．理論系だけではなく実装系の論文の投稿も歓迎いたします．発表申込締切: 2017年1月25日(水) 17:00 (JST) 原論文(ページ数不問，PDF形式)と論文概要(テキスト形式)を，著者名，所属，論文タイトル，キーワード(3つ以上)と併せて提出してください．論文概要にて，原論文の出典(発表会議名，掲載済／予定の別等を含む)についても明記してください．採否通知：2017年2月6日(月) カテゴリ3 (ポスター・デモ発表) ----------------------------- ポスター発表またはデモ発表(あるいは両方)を募集いたします．発表申込締切: 2017年2月8日(水) 17:00 (JST) 希望する発表形態を明記して著者名，所属，発表タイトル，発表概要 (200〜300字程度)，キーワード(3つ以上)を提出してください．発表形態については発表タイトル(Title欄)の最後の部分に括弧（）に入れて，「ポスター」「デモ」「ポスター・デモ」のいずれかを記載してください．採否通知：2017年2月15日(水) カテゴリ4 (サーベイ・チュートリアル発表) --------------------------------------- 発表申込締切: 2017年1月25日(水) 17:00 (JST) 著者名，所属，発表タイトル，キーワード(3つ以上)，発表概要(3ページ以内，PDF形式．目的，カバーする話題，想定する聴衆，必要な知識の記述を含むもの)を提出してください．採否通知：2017年2月6日(月) ====================================================================== 問い合わせ先 ppl2017-oc(a)ipl-e.ai.kyutech.ac.xn--jp()-753c9gpa1b92cqcsg7jrh5d1ix122cxi0h ppl2017-pc-chairs(a)ipl-e.ai.kyutech.ac.xn--jp(/)-m53d8hra6b05cmntd6e6b1719ok76b ====================================================================== プログラム委員会青谷知幸 (東京工業大学) 浅田和之 (東京大学) Reynald Affeldt (産業技術総合研究所) 稲葉一浩 (Google) 上野雄大 (東北大学) 菊池健太郎 (東北大学) 小宮常康 (電気通信大学) 篠埜功 (芝浦工業大学) 佐藤亮介 (東京大学) 首藤一幸 (東京工業大学) 末永幸平 (京都大学) 宋剛秀 (神戸大学) 千葉滋 (東京大学) 土屋達弘 (大阪大学) 中野圭介 (電気通信大学) 鍋島英知 (山梨大学) 番原睦則 (神戸大学) 前田敦司 (筑波大学) 松田一孝 (東北大学) 森畑明昌 (東京大学) 八杉昌宏 (九州工業大学) 組織委員会江本健斗 (九州工業大学) [組織委員長] 平石拓 (京都大学) 佐藤重幸 (高知工科大学) 海野広志 (筑波大学) 対馬かなえ (国立情報学研究所) 塚田武志 (東京大学) 篠埜功 (芝浦工業大学) [プログラム共同委員長] 番原睦則 (神戸大学) [プログラム共同委員長] ====================================================================== 篠埜　功 -- Isao Sasano <sasano(a)sic.shibaura-it.ac.jp>

1 0

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml