- Logic-ml - fos.kuis.kyoto-u.ac.jp

Fwd: [TYPES/announce] TTCS 2015 - Call for Papers
by Ichiro Hasuo 14 May '15

14 May '15

========================================= Topics in Theoretical Computer Science (TTCS 2015) http://www.ttcs.ir/ Institute for Research in Fundamental Sciences (IPM), Tehran, Iran August 26-28, 2015 *Submission Deadline:* May 15, 2015 ======================================== Scope ------------------------------ TTCS is a new bi-annual conference series, intending to serve as a forum for novel and high-quality research in all areas of Theoretical Computer Science. The conference is held in cooperation with the European Association for Theoretical Computer Science. There will be a number of satellite events at TTCS, These will feature presentation of early research results, and position papers. There will also be a forum for Ph.D. students to receive comments about their ongoing research projects. Topics of interest include but are not limited to: - algebra and co-algebra in computer science, - algorithms and data structures, - algorithmic coding theory, - algorithmic graph theory and combinatorics, - approximation algorithms, - computational complexity, - computational geometry, - computational learning theory, - concurrency theory, - coordination languages, - economics and algorithmic game theory, - fixed parameter algorithms, - formal verification and model-based testing, - logic in computer science, - machine learning - methods, models of computation and reasoning for embedded, hybrid, and cyber-physical systems, - optimization, - parallel and distributed algorithms, - quantum computing, - randomness in computing, - stochastic and probabilistic specification and reasoning - theoretical aspects of other CS-related research areas, e.g., computational science, databases, information retrieval, and networking, - theoretical cryptography, - theory of programming languages, and - type theory and its application in program verification. Keynote Speakers ------------------------------ Anuj Dawar, Cambridge University, UK Michael Fellows, Charles Darwin University, Australia Mehrnoosh Sadrezadeh, Queen Mary University of London, UK Submission ------------------------------ For the main conference, we solicit research papers in all areas of theoretical computer science. All papers will undergo a rigorous review process and will be judged based on their originality, soundness, significance of the results, and relevance to the theme of the conference. Papers should be written in English. Research papers should not exceed 15 pages in the LNCS style format. Multiple and/or concurrent submission to other scientific venues is not allowed and will result in rejection as well as notification to the other venue. Any case of plagiarism (including self-plagiarism from earlier publications) will result in rejection as well as notification to the the authors' institutions. Papers should be submitted through our EasyChair submission website: https://www.easychair.org/conferences/?conf=ttcs2015 . The web site is open for submissions. Important Dates ------------------------------ - *Paper Submission:* May 15, 2015 (Anywhwere on Earth) - *Author notification:* June 26, 2015 - *Camera ready paper due:* July 10, 2015 - *Conference:* August 26-28, 2015 Program Committee ------------------------------ *Track A: Algorithms and Complexity* - Mohammad Ali Abam, Sharif University of Technology, Iran - Saeed Akbari, Sharif University of Technology, Iran - Saeed Alaei, Cornell University, USA - Mohammad Hossein Bateni, Google Research, USA - Salman Beigi, IPM, Iran - Amir Daneshgar, Sharif University of Technology, Iran - Fedor Fomin, University of Bergen, Norway - Ali Ghodsi, University of Waterloo, Canada - Mohammad Ghodsi, Sharif University of Technology, Iran - Mohammad T. Hajiaghayi, University of Maryland, USA (Chair) - Amin Karbasi, Yale University, USA - Nicole Immorlica, Microsoft Research, USA - Amit Kumar, IIT Delhi, India - Mohammad Mahdian, Google Research, USA - Hamid Mahini, University of Maryland, USA - Bojan Mohar, Simon Fraser University, Canada - Mohammad Mahmoody, University of Virginia, USA - Vahab Mirrokni, Google Research, USA - Morteza Monemizadeh, Frankfurt University, Germany - Shayan Oveisgharan, UC Berkeley and University of Washington, USA - Debmalya Panigrahi, Duke University, USA - Jorg Sack, Carleton University, Canada - Mohit Singh, Microsoft Research, USA - Dimitrios M. Thilikos, CNRS, France and University of Athens, Greece - Suresh Venkatasubramanian, University of Utah, USA - Jan Vondrak, IBM Almaden Research Center, USA *Track B: Logic, Semantics, and Programming Theory* - Farhad Arbab, CWI and Leiden University, The Netherlands - S. Arun-Kumar, IIT Delhi, India - Ilaria Castellani, INRIA Sophia Antipolis, France - Dave Clarke, Uppsala University, Sweden and KU Leuven, Belgium - Pieter Cuijpers, Eindhoven University of Technology, The Netherlands - Fatemeh Ghassemi, Tehran University, Iran - Matthew Hennessy, Trinity College Dublin, Ireland - Ichiro Hasuo, University of Tokyo, Japan - Mahdi Jaghoori, AMC University of Amsterdam, The Netherlands - Jeroen Keiren, Vrije Universiteit Amsterdam, The Netherlands - Bas Luttik, Eindhoven University of Technology, The Netherlands - Jose Meseguer, University of Illinois at Urbana, USA - Lary Moss, Indiana University, USA - Mohammad Mousavi, Halmstad University, Sweden (Chair) - Jun Pang, University of Luxembourg, Luxembourg - Gerardo Schneider, Chalmers University of Technology, Sweden - Marjan Sirjani, Reykjavik University, Iceland - Walter Vogler, Augsburg University, Germany - Tim Willemse, Eindhoven University of Technology, The Netherlands

1 1

Kobe set theory seminar on Tue 19 May.
by Daisuke Ikegami 14 May '15

14 May '15

皆様神戸大学の池上と申します。来週の火曜日13:30から行われる神戸集合論セミナーのお知らせです。講演者は、カーネギーメロン大学でポスドクをしている Nam Trang さんです。どうぞお気軽にお越しください。問合せ先：池上大祐神戸大学大学院システム情報学研究科 E-mail: ikegami(a)people.kobe-u.ac.jp ========================================================================= 日時：2015年5月19日（火）13:30-15:00 講演者：Nam Trang （Carnegie Mellon University）場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室）交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車、「神大本部工学部前」停留所下車、徒歩すぐ。 http://www.kobe-u.ac.jp/guid/access/rokko/rokkodai-dai2.html （「ローカルマップ」の59番の建物）題目： Descriptive inner model theory and forcing axioms. アブストラクト： We discuss some recent developments in descriptive inner model theory, focusing on works on constructing canonical inner models of large cardinals and determinacy from combinatorial consequences of forcing axioms such as PFA. The upshot is the speaker’s result, built on earlier works of Steel and Sargsyan, that PFA implies the existence of models of “AD_R + Θ is regular”. The talk is mostly a survey talk and we aim to explain definitions and notions involved, hence should be accessible to general set theorists. =========================================================================

1 0

WoLLIC 2015 - CALL FOR PARTICIPATION
by 小野寛晰 14 May '15

14 May '15

CALL FOR PARTICIPATION WoLLIC 2015 22nd Workshop on Logic, Language, Information and Computation July 20-23, 2015 Bloomington, IN, USA CO-LOCATED WITH Conference on Computing Natural Reasoning (CoCoNat'15 <http://www.indiana.edu/~iulg/wollic/coconat.htm>) July 19-20, 2015 SCIENTIFIC SPONSORSHIP Interest Group in Pure and Applied Logics (IGPL) The Association for Logic, Language and Information (FoLLI) Association for Symbolic Logic (ASL) European Association for Theoretical Computer Science (EATCS) European Association for Computer Science Logic (EACSL) Sociedade Brasileira de Computação (SBC) Sociedade Brasileira de Lógica (SBL) ORGANISATION Department of Computer Science, Indiana University, USA Program in Pure and Applied Logic, Indiana University, USA Centro de Informática, Universidade Federal de Pernambuco, Brazil HOSTED BY Department of Computer Science, Indiana University, USA CALL FOR PARTICIPATION WoLLIC is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. Each meeting includes invited talks and tutorials as well as contributed papers. The twenty-second WoLLIC will be held at the Department of Computer Science, Indiana University, Bloomington, from July 20th to 23rd, 2015. It is sponsored by the Association for Symbolic Logic (ASL), the Interest Group in Pure and Applied Logics (IGPL), the The Association for Logic, Language and Information (FoLLI), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), the Sociedade Brasileira de Computação (SBC), and the Sociedade Brasileira de Lógica (SBL). PROCEEDINGS The proceedings of WoLLIC 2015, including both invited and contributed papers, will be published in advance of the meeting as volume 9160 in Springer's LNCS series. In addition, abstracts will be published in the Conference Report section of the Logic Journal of the IGPL, and selected contributions will be published as a special post-conference WoLLIC 2015 issue of Mathematical Structures in Computer Science, CUP (tbc). INVITED TALKS . Adriana Compagnoni (Stevens Institute, USA) Modeling Language Design for Complex Systems Simulation . Nina Gierasimczuk (University of Amsterdam) Learning in the Limit, General Topology and Modal Logic . John Harrison (Intel, USA) Formalization of Mathematics for Fun and Profit . Peter Jipsen (Chapman U, USA) From Residuated Lattices via GBI-algebras to BAOs . André Joyal (U du Québec Montreal, Canada) Categories of Games . Mehrnoosh Sadrzadeh (Queen Mary, UK) Multi-Linear Algebraic Semantics for Natural Language . Chung-chieh Shan (Indiana U, USA) (tba) . Alexandra Silva (Radboud U Nijmegen, The Netherlands) Towards a Nominal Chomsky Hierarchy. TUTORIALS Nina Gierasimczuk (University of Amsterdam) John Harrison (Intel, USA) André Joyal (U du Québec Montreal, Canada) Alexandra Silva (Radboud U Nijmegen, The Netherlands) SPECIAL SESSION: SCREENING OF MOVIES ABOUT MATHEMATICIANS In remembrance of the 30th anniversary of the passing away of Julia Hall Bowman Robinson (December 8, 1919 – July 30, 1985), an American mathematician best known for her work on decision problems and Hilbert's Tenth Problem, the program of the meeting will include a screening of George Csicsery's documentary "Julia Robinson and Hilbert's Tenth Problem" (2008). As a tribute to a recent breakthrough in mathematics, there will also be a screening of Csicsery's "Counting from Infinity: Yitang Zhang and the Twin Prime Conjecture" (2015) which centers on a very exciting string of mathematical discoveries that occurred during 2013, started when Yitang Zhang, a virtually unknown mathematician working as adjunct professor at the University of New Hampshire, submitted a paper to the Annals of Mathematics in April 2013. PROGRAMME COMMITTEE Juliana Küster Filipe Bowles (U St Andrews, Scotland) Robin Cooper (U Gothenburg, Sweden) Martín Escardó (U Birmingham, UK) Nikos Galatos (U Denver, USA) Achim Jung (U Birmingham, UK) Sara Kalvala (U Warwick, UK) Elham Kashefi (Edinburgh U, Scotland) Peter Lefanu Lumsdaine (Institute for Advanced Study, USA) Ian Mackie (U Sussex, UK) Gerard de Melo (Tsinghua U, China) Vivek Nigam (Federal U of Paraíba, Brazil) Catarina Dutilh Novaes (U Groningen, The Netherlands) Valeria de Paiva (Nuance Comm, USA) (CHAIR) Luiz Carlos Pereira (PUC-Rio, Brazil) Elaine Pimentel (Federal U of Rio Grande do Norte, Brazil) Alexandra Silva (Radboud Nijmegen U, The Netherlands) Carolyn Talcott (SRI International, USA) Josef Urban (Radboud Nijmegen U, The Netherlands) Laure Vieu (IRIT-Toulouse, France) Renata Wasserman (U São Paulo, Brazil) Anna Zamansky (U Haifa, Israel) STEERING COMMITTEE Samson Abramksy, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid Hodges, Ulrich Kohlenbach, Daniel Leivant, Leonid Libkin, Angus Macintyre, Luke Ong, Hiroakira Ono, Ruy de Queiroz. ORGANISING COMMITTEE Daniel Leivant (Indiana U) (Local co-chair) Larry Moss (Indiana U) (Local co-chair) Anjolina G. de Oliveira (U Fed Pernambuco) Ruy de Queiroz (U Fed Pernambuco) (co-chair) REGISTRATION Now open at http://www.indiana.edu/~iulg/wollic/registration.html <http://www.indiana.edu/~iulg/wollic/registration.html> ACCOMODATION Please visit http://www.indiana.edu/~iulg/wollic/venue.html <http://www.indiana.edu/~iulg/wollic/venue.html> FURTHER INFORMATION Contact one of the Co-Chairs of the Organising Committee. WEB PAGE www.indiana.edu/~iulg/wollic <http://www.indiana.edu/~iulg/wollic>

1 0

CFP: LCC 2015 - extended deadline
by Nao Hirokawa 21 Apr '15

21 Apr '15

皆様７月に京都で開催されます「第16回論理と計算量に関するワークショップ LCC 2015」の講演者募集の締切を延長致しました。計算量理論からプログラムの計算量解析まで、計算量に関する研究発表を広く募集しております。講演を検討頂けましたら幸いです。廣川　直 (JAIST) ====================================================================== Third Call for Papers (extended deadline) LCC 2015 16th International Workshop on Logic and Computational Complexity July 4-5, 2015, Kyoto, Japan collocated with ICALP/LICS 2015 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 April 29, 2015 (extended) * notification May 14, 2015 * workshop July 4-5, 2015 INVITED SPEAKERS: * Olaf Beyersdorff (University of Leeds) * Mikołaj Bojańczyk (Warsaw University) * Akitoshi Kawamura (University of Tokyo) * Jean-Yves Marion (LORIA, Nancy) * ... SUBMISSION: We 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. 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=lcc2015 PROGRAM COMMITTEE: * Albert Atserias (Universitat Politècnica de Catalunya, Barcelona) co-chair * Guillaume Bonfante (LORIA, Nancy) * Yijia Chen (Fudan University, Shanghai) * Ugo Dal Lago (Università degli Studi di Bologna) * Nao Hirokawa (JAIST, Nomi) co-chair * Antonina Kolokolova (Memorial University of Newfoundland) * Damiano Mazza (CNRS, LIPN - University Paris 13) * Georg Moser (University of Innsbruck) * Moritz Müller (Kurt Gödel Research Center for Mathematical Logic, Wien) * Benjamin Rossman (National Institute of Informatics, Tokyo) * Iddo Tzameret (Royal Holloway, University of London) * Heribert Vollmer (Leibniz Universität Hannover)

1 0

Talk by Yoshimura Kazuto (23 Apr 11:00-)
by Tetsuya Sato 17 Apr '15

17 Apr '15

京都大学数理解析研究所の佐藤です。 4月23日11:00から、北陸先端科学技術大学院大学の吉村和人氏に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 23 Apr, 2015 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: Yoshimura Kazuto (Japan Advanced Institute of Science and Technology) Title: A brief introduction to the theory of the Weihrauch lattice Abstract: The Weihrauch lattice and its underlying reducibility notion, Weihrauch reducibility, was introduced in 1980s as fundamental concepts for investigating the discontinuities of functions. However it is only recently when the deep analysis of the Weihrauch lattice started, being influenced by the project of constructive reverse mathematics. In this talk, we aim to present a brief review on the theory of the Weihrauch lattice from both historical and technical perspectives, and try to point out the importance of the structure for computable analysis, constructive mathematics and computer science respectively.

1 0

2nd CFP: LCC 2015
by Nao Hirokawa 14 Apr '15

14 Apr '15

皆様７月に京都で開催されます、ICALP/LICS 併設のワークショップ「第16回論理と計算量に関するワークショップ LCC 2015」の講演者募集のご案内を致します。計算量理論からプログラムの計算量解析まで、計算量に関する研究発表を広く募集しております。皆様、ぜひ投稿をご検討下さい！廣川　直 (JAIST) ====================================================================== Second Call for Papers LCC 2015 16th International Workshop on Logic and Computational Complexity July 4-5, 2015, Kyoto, Japan collocated with ICALP/LICS 2015 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 April 19, 2015 * notification May 14, 2015 * workshop July 4-5, 2015 INVITED SPEAKERS: * Olaf Beyersdorff (University of Leeds) * Mikołaj Bojańczyk (Warsaw University) * Akitoshi Kawamura (University of Tokyo) * Jean-Yves Marion (LORIA, Nancy) * ... SUBMISSION: We 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. 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=lcc2015 PROGRAM COMMITTEE: * Albert Atserias (Universitat Politècnica de Catalunya, Barcelona) co-chair * Guillaume Bonfante (LORIA, Nancy) * Yijia Chen (Fudan University, Shanghai) * Ugo Dal Lago (Università degli Studi di Bologna) * Nao Hirokawa (JAIST, Nomi) co-chair * Antonina Kolokolova (Memorial University of Newfoundland) * Damiano Mazza (CNRS, LIPN - University Paris 13) * Georg Moser (University of Innsbruck) * Moritz Müller (Kurt Gödel Research Center for Mathematical Logic, Wien) * Benjamin Rossman (National Institute of Informatics, Tokyo) * Iddo Tzameret (Royal Holloway, University of London) * Heribert Vollmer (Leibniz Universität Hannover)

1 0

Fwd: categories: CALCO Early Ideas 2015 : Call for Contributions
by Ichiro Hasuo 11 Apr '15

11 Apr '15

みなさま，６月下旬の国際会議 CALCO の併設ワークショップ CALCO Early Ideas の案内をお送りします．特に学生さんに，いろいろとフィードバックがもらえておすすめです．どうか投稿をご検討ください．蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/ ********************************************************** CALL FOR CONTRIBUTIONS: CALCO Early Ideas 2015 *********************************************************** A satellite event of CALCO 2015 6th International Conference on Algebra and Coalgebra in Computer Science In cooperation with ACM SIGLOG June 24 - 26, 2015 Nijmegen, Netherlands http://coalg.org/calco15/ei.html ========================================================== Submission: May 8, 2015 Author notification: May 22, 2015 Final version: June 5, 2015 ========================================================== The programme of CALCO 2015 will include special sessions reserved for the CALCO Early Ideas Workshop, featuring presentations of work in progress and original research proposals. PhD students and young researchers are particularly encouraged to contribute. Attendance at the workshop is open to all conference participants. The CALCO Early Ideas Workshop invites submissions on the same topics as the CALCO conference: reporting results of theoretical work, 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. CALCO Early Ideas presentations will be selected according to originality, significance, and general interest, on the basis of submitted 2-page short contributions. It can be work in progress, a summary of work submitted to a conference or workshop elsewhere, or work that in some other way might be interesting to the CALCO audience. A booklet with the accepted short contributions will be available at the workshop. SUBMISSION INFORMATION Submissions will be handled via the CALCO 2015 Early Ideas EasyChair site https://www.easychair.org/conferences/?conf=calco2015ei and will be evaluated by the CALCO PC chairs. Submissions should be no more than 2 pages long in the format specified by LIPIcs. The volume of selected papers will be made available in the arXiv and on the CALCO pages. Authors will retain copyright, and are also encouraged to disseminate the results by subsequent publication elsewhere. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Fwd:
by Ichiro Hasuo 11 Apr '15

11 Apr '15

LAST CALL FOR PAPERS The 12th International Workshop on Quantum Physics and Logic (QPL) July 13-17, Oxford, United Kingdom http://www.cs.ox.ac.uk/qpl2015 The 12th International Workshop on Quantum Physics and Logic (QPL) will take place at the Department of Computer Science of the University of Oxford between Wednesday 15 and Friday 17 July, 2015. The workshop will be preceded by tutorials on Monday 13 and Tuesday 14 July 2015. This workshop brings together researchers working on mathematical foundations of quantum physics, quantum computing, spatio-temporal causal structures, and related areas such as computational linguistics. Of particular interest are topics that use logical tools, ordered algebraic and category-theoretic structures, formal languages, semantical methods and other computer science methods for the study of physical behaviour in general. Previous QPL events were held in Kyoto (2014), Barcelona (2013), Brussels (2012), Nijmegen (2011), Oxford (2010), Oxford (2009), Reykjavik (2008), Oxford (2006), Chicago (2005), Turku (2004), and Ottawa (2003). INVITED SPEAKERS Dan Browne (University College London) Paul Busch (University of York) Chris Douglas (University of Oxford) Lucien Hardy (Perimeter Institute) TUTORIAL SPEAKERS Dan Browne (University College London) Paul Busch (University of York) Oscar Dahlsten (University of Oxford) Pawel Sobocinski (University of Southampton) IMPORTANT DATES Submission Deadline: May 1, 2015 Notification of Acceptance: June 1 Papers Ready: June 15 Tutorials: July 13-14 Workshop: July 15-17 SUBMISSIONS Prospective speakers are invited to submit a contribution to the workshop. - *Short contributions* consist of a 3 page description of the work, and a link to a paper available elsewhere. - Longer *original contributions* consist of a 5-12 page extended abstract which provides sufficient evidence of results of genuine interest and provides sufficient detail to allow the program committee to assess the merits of the work. Submissions of works in progress are encouraged but must be more substantial than a research proposal. Extended versions of accepted original research contributions will be published in Electronic Proceedings in Theoretical Computer Science (EPTCS) after the workshop. Submissions should be prepared using LaTeX, and must be submitted in PDF format. Use of the EPTCS style is encouraged. Submission is done via EasyChair: https://www.easychair.org/conferences/?conf=qpl2015 There will be an award for the best paper whose authors are all students, at the discretion of the programme committee. REGISTRATION Please visit the website to register. We encourage participation by graduate students, and will be able to provide limited reimbursement to partially support students for travel and accommodation. Further information is found on the workshop website. PROGRAMME COMMITTEE John Baez (University of California Riverside) Dan Browne (University College London) Giulio Chiribella (Tsinghua University) Bob Coecke (University of Oxford) Ross Duncan (University of Strathclyde) Tobias Fritz (Perimeter Institute) Simon Gay (University of Glasgow) Ichiro Hasuo (University of Tokyo) Chris Heunen (University of Oxford, co-chair) Matty Hoban (University of Oxford) Bart Jacobs (Radboud University Nijmegen) Viv Kendon (Durham University) Matt Leifer (Perimeter Institute) Prakash Panangaden (McGill University) Dusko Pavlovic (University of Hawaii) Simon Perdrix (CNRS Nancy) Mehrnoosh Sadrzadeh (Queen Mary University of London) Peter Selinger (Dalhousie University, co-chair) Rob Spekkens (Perimeter Institute) Bas Spitters (Aarhus University) Isar Stubbe (Universite du Littoral-Cote-d'Opale) Jamie Vicary (University of Oxford, co-chair) Mingsheng Ying (University of Technology Sydney, Tsinghua University) STEERING COMMITTEE Bob Coecke (University of Oxford) Prakash Panangaden (McGill University) Peter Selinger (Dalhousie University) LOCAL ORGANISATION Destiny Chen Chris Heunen Jamie Vicary [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

NLCS '15 Final Call for Papers - New Deadline: April 20
by Makoto Kanazawa 06 Apr '15

06 Apr '15

******************************************************* EXTENDED SUBMISSION DEADLINE: April 20 ******************************************************* Third Workshop on Natural Language and Computer Science NLCS '15 July 5, 2015 Kyoto, Japan http://www.indiana.edu/~iulg/nlcs.html A workshop affiliated with 42nd International Colloquium on Automata, Languages and Programming (ICALP 2015) and 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015) Endorsed by the Association for Computational Linguistics Special Interest Group on Computational Semantics Paper submission deadline (extended): April 20, 2015 AIMS AND SCOPE Formal tools coming from logic and category theory are important in both natural language semantics and in computational semantics. Moreover, work on these tools borrows heavily from all areas of theoretical computer science. In the other direction, applications having to do with natural language has inspired developments on the formal side. The workshop invites papers on both topics. Specific topics includes, but are not limited to: • logic for semantics of lexical items, sentences, discourse and dialog • continuations in natural language semantics • formal tools in textual inference, such as logics for natural language inference • applications of category theory in semantics • linear logic in semantics • formal approaches to unifying data-driven and declarative approaches to semantics INVITED SPEAKERS Makoto Kanazawa, National Institute of Informatics Gerard de Melo, Tsinghua University PROGRAM COMMITTEE • Heather Burnett, Université de Toulouse 2 • Robin Cooper, University of Gothenburg • Valeria de Paiva, Nuance Communications • Tim Fernando, Trinity College • Nissim Francez, The Technion • Makoto Kanazawa, National Institute of Informatics • Larry Moss, Indiana University • Aarne Ranta, University of Gothenburg • Christian Retoré, Université de Montpellier PAPER SUBMISSIONS Extended abstracts of up to 10 pages may be submitted through Easychair: https://easychair.org/conferences/?conf=nlcs15 ORGANIZERS Valeria de Paiva Nuance.com Email: Valeria.dePaiva at nuance .com Makoto Kanazawa National Institute of Informatics Email: kanazawa at nii.ac.jp Larry Moss Indiana University Email: lsm at cs.indiana . edu IMPORTANT DATES Paper submission deadline (extended): April 20, 2015 Author notification: May 1, 2015 Electronic versions of papers due: May 14, 2015 Workshop: July 5, 2015

1 0

Talk by Gergei Bana (26 Mar 11:00-)
by Shinya Katsumata 19 Mar '15

19 Mar '15

京都大学数理解析研究所の勝股です。 3月26日11:00から、INRIA Paris-RocquencourtのGergei Bana氏に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 26 Mar, 2015 Place: Rm 478, Research Building 2, Main Campus, Kyoto University http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (See 34) 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speaker: Gergei Bana (INRIA Paris-Rocquencourt) Title: Formal Verification of Complexity-Theoretic Properties of Security Protocols Abstract: Rigorous modeling of attackers to security protocols, and hence the prospect of proving the security of protocols has been developed from the 1980’s in two directions. One focused on automated proving and accordingly modeled protocol execution and attackers with a set of symbolic operations on symbolic terms, treating cryptographic primitives such as encryption as black-box operations (Dolev-Yao approach). The other took a complexity-theoretic approach, modeled protocol execution and attackers as probabilistic polynomial-time algorithms with the aim of deriving protocol security from hardness assumptions such as the DDH assumption (computational approach). While the first technique is convenient for automation and is effective in finding attacks, there is little guarantee that if there is no Dolev-Yao attack, then there is no real-life attack either. Computational approach approximates real life far closer, but is not convenient for automation, proving by hand is too laborious and error prone. From the beginning of the 2000’s there have been numerous research directions trying to unify the two approaches and provide automated verification of computational properties, with variable success. In this talk we briefly review the history of the unification process, the failed attempts, the currently available tools, and we give a more detailed account of our approach with Hubert Comon-Lundh of ENS Cachan and Mitsuhiro Okada of Keio University, which we call “computationally complete symbolic attacker”.

1 0

Prof. Giovanni Sambin at NII Logic Seminar
by Makoto Tatsuta 16 Mar '15

16 Mar '15

Prof. Giovanni Sambin at NII Logic Seminar Date: March 23, 2015, 13:30--15:30 Place: National Institute of Informatics, Room 1716 (17th floor) 場所: 国立情報学研究所 17階 1716室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Giovanni Sambin (University of Padova) Title: Realizability interpretation of topology Abstract: It is a fact of life that the classical notion of topological space can be obtained in a constructive (intuitionistic and predicative) way by starting from neighbourhoods and defining points as specific subsets of neighbourhoods. Beginning in the 80s, we introduced what is now called formal topology: a predicative and intuitionistic pointfree approach to topology. The key ingredient of a formal topology is a relation, called cover, between elements and subsets of a given set S of formal neighbourhoods, or observables. In the 90s, we showed that the cover relation of formal topologies can be generated by induction. Given a set of observables S, a family of sets I(a) set (a in S) and a family C(a,i) of subsets of S, for a in S and i in I(a), one can generate by induction the least cover such that every C(a,i) is a cover of a. We call this an axiom-set. Soon after, I also added a positivity relation, again between elements and subsets of S, which provides a way to introduce closed subsets in a pointfree way. We showed that positivity relations can be generated coinductively from an axiom-set. It turns out that generation, by induction and by coinduction, from axiom-sets is the only postulate over a very elementary foundation, which have been shown to admit a realizability interpretation. So to obtain a realizability interpretation of constructive topology one only need to find a realizability interpretation for the principle of generation from axiom-sets. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

TSSS (Tsukuba Software Science Seminar) at AIST Tsukuba, Mar. 23, 2015
by 山形賴之 11 Mar '15

11 Mar '15

Dear everyone, (apologies for multiple posts) I am pleased to announce another TSSS at AIST Tsukuba central, held Mar. 23, 2015. The program is as follows. Note that the largest canteen in AIST Tsukuba central is closed, so we have a long lunch break. You can eat and drink in the seminar room. The seminar is open to everyone, but please let me know by Mar. 19 if you want to attend. In particular, if you come by car, please let me know. 皆様、(重複投稿をお許し下さい) 2015年3月23日に産総研のつくばセンターでTSSSを開催いたします。プログラムは下記のとおりです。どなたでも参加できますが、参加予定の方はあらかじめ3月19日までに山形までご一報下さい。特にお車でお越しになる方は連絡をお願いします。なお、産総研の大食堂は現在閉鎖中です。外に食事に行けるよう昼休みを長めにとっています。セミナー室は飲食可能です。よろしくお願いします。 Tsukuba Software Science Seminar Date: Mar. 23, 2015 Place: National Institute of Advanced Industrial Science and Technology (AIST), Tsukuba central, AIST Tsukuba Headquarters and Information Technology Collaborative Research Center Map: http://www.aist.go.jp/aist_e/guidemap/tsukuba/tsukuba_map.html http://www.aist.go.jp/aist_e/guidemap/tsukuba/center/tsukuba_map_c.html 10:00 - 10:45 Runtime verification using a process algebra CSP, Yoriyuki Yamagata 10:45 - 11:00 Discussion 11:00 - 13:00 Break 13:00 - 13:45 Applying Formal Methods in Trust and Security systems, Liu Yang 13:45 - 14:00 Discussion 14:00 - 14:15 Break 14:15 - 15:00 Using Model Checking and Theorem Proving to Validate and Verify Cyber-Physical Systems, Chen-wei Wang 15:00 - 15:15 Discussion Title: Speaker: Yoriyuki Yamagata Abstract: A process algebra such as CSP, CCS, and pi-calculus is used to describe a concurrent system. In this talk, we introduce a tool called CSP_E, CSP for event monitoring. CSP_E tests a runtime log against a specification given by CSP, and report whether the log satisfies the given specification or not. CSP_E is implemented as a internal DSL within Scala programming language. Title: Using Model Checking and Theorem Proving to Validate and Verify Cyber-Physical Systems Speaker: Chen-wei Wang Abstract: In this talk I present part of the results that contribute to the research project "Certification of Safety-Critical Software-Intensive Systems" funded by the Ontario government. The project involves various application domains: biomedical, automotive, and nuclear. This talk focuses on the nuclear domain. Contributions are made by researchers at York University and McMaster University. I first present the use of an automated checking tools for Timed Transition Models (TTM) to model, simulate, and validate cyber-physical systems, with respect to discrete-time temporal properties. I then present the use of tabular expressions and the PVS theorem prover to model and verify function blocks that can be reused to build Programmable Logic Controllers (PLCs). In both approaches, I use function blocks supplied by the industrial standard 61131-3 for illustration. To conclude the talk, I report lessons that we learn and mention ongoing research. Title: Applying Formal Methods in Trust and Security systems Speaker: Liu Yang Abstract: Cyber-attack detection, defense and recovery are important topics in cybersecurity, but the ultimate goal of cybersecurity is to build attack-free systems. Security verification and building attack-free systems are very challenging tasks in view of the size and the complexity of the systems. In this talk, we will present our recent attempts in applying formal methods in modeling and verifying security protocols, security protocol implementations, malware in Android OS and even vulnerabilities. We will also discuss the challenges in applying formal methods in security and possible solutions. Lastly, we will introduce our recent research project “Securify: A Compositional Approach of Building Security Verified System”, which aims at building secure and verifiable systems ground-up. Short Bio: Dr Liu Yang graduated in 2005 with a Bachelor of Computing (Honours) in the National University of Singapore (NUS). In 2010, he obtained his PhD and started his post doctoral work in NUS, MIT and SUTD. In 2011, Dr Liu is awarded the Temasek Research Fellowship at NUS to be the Principal Investigator in the area of Cyber Security. In 2012 fall, he joined School of Computer Engineering, Nanyang Technological University as a Nanyang Assistant professor. Dr. Liu specializes in software verification, security and software engineering. His research has bridged the gap between the theory and practical usage of formal methods to evaluate the design and implementation of software for high assurance. His work led to the development of a state-of-the-art model checker, Process Analysis Toolkit (PAT). This tool is used by research institutions in over 70 countries for research and education. He has more than 100 publications and leading a research group of 30 people. -- 山形頼之独立行政法人産業技術総合研究所主任研究員 https://staff.aist.go.jp/yoriyuki.yamagata/

1 1

島根大学教授(任期なし) 公募【5/28締切】について
by Munehiro Iwami 11 Mar '15

11 Mar '15

皆様島根大学の岩見と申します。浜口先生の代理で「島根大学教授(任期なし) 公募【5/28締切】」の情報を送ります。 ------------------------------------------------------------------- 島根大学教授(任期なし) 公募【5/28締切】大学院総合理工学研究科情報システム学領域１．職名及び人数：教授　１名２．所属：島根大学大学院総合理工学研究科　情報システム学領域３．担当専門分野：情報科学／情報工学(ソフトウェア工学が望ましい) ４．担当予定授業科目　　　大学院総合理工学研究科情報システム学コースに関わる専門科目及び　　数理・情報システム学科（情報系）に関わる専門科目および全学基礎科目　　　大学院：専門分野に関連する科目，セミナー，特別研究　　　学　部：プログラミング関連および専門分野に関連する講義・演習科目，　　　　　　　　情報科学(全学基礎科目)，卒業研究５．任用予定年月日：平成２７年　１０月　１日以降のできるだけ早い時期６．応募資格　　　・博士の学位を有すること．　　・国籍は問わないが，日本語で授業ができること．７．提出書類　　　(1) 履歴書（写真貼付のこと）　　(2) 研究業績リスト　　　　研究費の獲得実績，および学会活動・社会活動の実績を含む　　(3) 論文別刷3編程度（コピー可）　　(4) 上記(3)の論文の概要（各論文について200字以内）　　(5) 教育研究に対する抱負　　(6) 業績を評価できる方2名の氏名及び連絡先　　応募書類は原則として返却しません。 ※ 提出書類に含まれる個人情報は，選考及び採用以外の目的には使用しま　せん。８．選考方法　　　書類選考及び必要に応じ本学において面接等を行います。その際の旅費・宿泊費は応募者の負担となります。また，島根大学では男女共同参画社会の実現を目指しています。「男女共同参画社会基本法」の趣旨に則り，業績（研究　業績，教育業績，社会的貢献等）及び人物の評価において同等と認められた場　合は女性を採用します。選考結果は応募者本人に通知します。９．応募締め切り：平成２７年５月２８日（木）必着　 10．応募書類の送付先　　〒690-8504　松江市西川津町１０６０　　島根大学大学院総合理工学研究科長　服部　泰直　　封筒の表に，「情報システム学領域教員応募書類在中」と朱書し，　　「（簡易）書留郵便」で郵送して下さい。 11．問い合わせ先　　島根大学大学院総合理工学研究科　情報システム学領域　領域長浜口　清治　　　TEL/FAX: 0852-32-6468 　　　E-mail: hama(a)cis.shimane-u.ac.jp (備　考) 本学は，「男女共同参画社会基本法」の趣旨に則り，男女共同参画を推進しています。以上． ------------------------------------------------------------------------ -- 以上、よろしくお願い致します。岩見宗弘島根大学総合理工学研究科情報システム学領域 E-mail: munehiro(a)cis.shimane-u.ac.jp

1 0

Workshop on Logic and Philosophy of Logic, March 19th(Thu)-20th(Fri), 2015
by Yuta Takahashi 11 Mar '15

11 Mar '15

--------------------------------------------------------------------- We apologize if you receive this message more than once. --------------------------------------------------------------------- The following Workshop on Logic and Philosophy of Logic is scheduled. 次のようなワークショップ「Workshop on Logic and Philosophy of Logic」を予定しております。参加自由です。 ---- Workshop on Logic and Philosophy of Logic 「論理学・論理哲学ワークショップ」 Date: March 19th(Thu)-20th(Fri), 2015 日時: 2015年3月19日(Thu)-20日(Fri) Place: Distance Learning Room (B4F), South Building, Mita campus of Keio University. 場所: 慶應大学三田キャンパス南館地下4階ディスタンスラーニングルーム (http://www.keio.ac.jp/en/maps/mita.html 13番の建物です。/ Building #13 on this map.) URL: http://ctj.keio.ac.jp/news/27 (*最新プログラムはこちらでご確認ください) ---- Tentative Program: 3/19: 13:00-13:10 Opening Remark, Mitsuhiro Okada (Keio University) 13:00-13:50 Makoto Fujiwara (Tohoku University, Department of Mathematics): "Constructive provability versus uniform provability in classical computable mathematics" 13:50-14:50 Giovanni Sambin (Dipartimento di Matematica Pura e Applicata, Università di Padova): "A single system for a plurality of logics" 14:50-15:20 Break 15:20-16:10 Gergei Bana (INRIA, France) "Fitting's model construction and computability" (joint work with Mitsuhiro Okada) 16:10-17:10 Sandra Laugier (Université Paris 1, Centre de Philosophie Contemporaine de la Sorbonne) "Rule-Following, Practice, and Forms of life" 17:10-17:30 Discussion 3/20: 10:30-11:10 Ukyo Suzuki (The University of Tokyo, Department of History and Philosophy of Science): "The Possibility of Predicative Arithmetic" (Talk in Japanese, possibly with English slides) 11:10-12:00 Shunsuke Yatabe (West Japan Railway Company): "Is truth a logical connective?" 12:00-13:30 Lunch Break 13:30-14:30 Mirja Hartimo (University of Jyväskylä, Department of Social Sciences and Philosophy) "Husserl and mathematics in the 1920s" 14:30-14:50 Break 14:50-15:50 Mathieu Marion (Université du Québec à Montréal, Philosophie Department) "Wittgenstein and Intuitionism: The Law of Excluded Middle and Following a Rule" 15:50-16:10 Break 16:10-17:00 Ryota Akiyoshi (Kyoto University, Department of Philosophy) "An interpretation of Brouwer’s argument of the bar induction via infinitary proof theory" 17:00-17:20 Concluding Discussion --------------------------------------------------------------------- Organisers: Ryota Akiyoshi (co-chair) Mitsuhiro Okada (co-chair) Yutaro Sugimoto Yuta Takahashi 主催: 慶應義塾大学「思考と行動判断」の研究拠点共催: 慶應義塾大学論理と感性のグローバル研究センター問合せ先: Mita Logic Seminar /「思考と行動判断」の研究拠点事務局 logic(a)abelard.flet.keio.ac.jp ------------------------- ABSTRACTS: Makoto Fujiwara "Constructive provability versus uniform provability in classical computable mathematics" So-called intuitionistic analysis EL is two-sorted intuitionistic arithmetic, which serves as system to formalize constructive mathematics. In this talk, we show that for any existence theorem T of some syntactical form, T is provable in EL if and only of T is uniformly provable in classical variant RCA of EL. From a philosophical point of view, it might be remarkable that all of our proofs are constructive, namely, they are just explicit syntactic translations. Thus we constructively (from a meta-perspective) establish the equivalence between constructive provability and classical uniform provability in RCA for a large number of existence theorems. ---- Giovanni Sambin "A single system for a plurality of logics" We propose a single, unified formulation for a wide variety of logics. This is achieved thorugh a sequent calculus UB for classical logic which uses a third structural sign, besides turnstile and comma, to denote active formulas in a context. Then, besides weakening and contraction, structural rules of UB include also some rules for the management of active formulas. All most common logics (classical, intuitionistic, paraconsistent, substructural, both in their intuitionistic and classical version) become literally (equivalent to) subsystems of UB. In other words, our previous approach showing that many logics could be seen as extensions of our basic logic B (JSL 2000), is now fully formal and internalized. Inference rules for all logical constants in UB are justified through the principle of reflection.This offers a single proof-theoretic semantics for all logical constants in all logics and confirms beyond doubts Dosen's principle saying that a logic is only determined by structural rules.A proof in one of the above logics is just a proof in UB which does not use some of the structural rules. We produce a cut-elimination procedure which respects structural rules and thus automatically becomes a cut-elimination procedure for all logics expressible as subsystems of UB.One benefit is that one can concentrate efforts on UB to improve both understanding and computational efficiency for a wide variety of logics. ---- Gergei Bana "Fitting’s model construction and computability" (joint work with Mitsuhiro Okada) We review Fitting’s embedding of classical logic into S4, that is, Fitting’s possible world semantics for classical logic.This is closely related to Cohen's forcing.Then we show how this construction naturally emerges when trying to formalize what a (malicious) agent can possibly computeor cannot compute from what is available to the agent as input.Finally, we illustrate how this construction helps us to carry out security proofs for cryptographic prot. ---- Sandra Laugier "Rule-Following, Practice, and Forms of life" TBA ---- Ukyo Suzuki "The Possibility of Predicative Arithmetic" (可述算術の可能性) In this talk, I will present an idea to find a non-revisionistic kind of interest in Edward Nelson’s Predicative Arithmetic. First, I’ll briefly summarize Predicative Arithmetic as a research program with Nelson’s own revisionistic motivation. Next, I’ll suggest Predicative Arithmetic can provide a formal model for Wittgenstein’s conception of mathematical proof as concept-formation. If my suggestion is correct, Predicative Arithmetic can give a Wittgensteinian answer to the so-called “paradox of inference” presented by Dummett. (この発表では、エドワード・ネルソン(1932-2014)の可述算術の興味を、非改訂主義的観点から捉えるアイデアを提示する。はじめに、可述算術という研究プログラムを、ネルソン自身の改訂主義的モチベーションと共に簡単に解説する。次に、可述算術が、ウィトゲンシュタインによって提示された、概念形成としての数学的証明という考え方に、形式的モデルを提供するものであることを示唆したい。この捉え方が正しければ、ダメットによって提示されたいわゆる「推論のパラドクス」に対して、可述算術は、ウィトゲンシュタイン的な解答を与える。) ---- Shunsuke Yatabe "Is truth a logical connective?" Truth theories like the Friedman-Sheard's truth theory ({\bf FS}) have two rules, T-in rule and T-out rule, about introduction and elimination of the truth predicate. They look like the introduction rule and the elimination rule of a logical connective. From the proof theoretic semantics viewpoint, one might think that the truth predicate is a logical connective which is governed by these two rules. >From this proof theoretic semantics viewpoint, the nature of truth is like deflationist's nature of truth. Additionally one of the most important things is that the truth predicate does not disturb the traceability of the argument from the premises to a conclusion. However, a crucial problem has been known: any criteria to be a logical connective, known as a ``harmony" of the introduction rule and the elimination rule, are not satisfied because of the $\omega$-inconsistency of FS. Such $\omega$-inconsistency is caused by the fact that the truth predicate enables us to define paradoxical formulae of seemingly infinite-length. These formulae can be regarded as coinductive objects in terms of computer science. The reason of the failure of the harmony is that these criteria are defined not for coinductively defined paradoxical formulae but for inductively defined formulae. In this talk, we examine how we can extend the criteria for harmony for coinductive formulae in terms of the inversion principle of proftheoretic semantics and corecursive functions in coinductive datatypes. --- Mirja Hartimo "Husserl and mathematics in the 1920s" The paper contextualizes Husserl’s writings on mathematics in the 1920s. It offers a look to Husserl’s library and in particular to the books on mathematics he owned and were published after 1917 but before 1929. Some of these books have reading marks showing that Husserl studied them. Four of them have been studied particularly carefully: Hilbert’s 1922 Neubegründung der Mathematik, Weyl’s article ”Die heutige Erkenntnislage in der Mathematik”(1925) and the book Philosophie der Mathematik und Naturwissenschaft (1926). The presentation will discuss the nature of Husserl’s reading marks on these items and then show how these influences can be seen in Husserl’s Formal and Transcendental Logic. --- Mathieu Marion "Wittgenstein and Intuitionism: The Law of Excluded Middle and Following a Rule" Wittgenstein attended a lecture by Brouwer in Vienna, in March 1928. Witness accounts by Herbert Feigl and Karl Menger and even Brouwer’s own testimony point to his interest, but there are few comments on typically intuitionistic topics, such as the critique of the unrestricted application of the Law of Excluded Middle, and the impact of intuitionism on his philosophy remains a controversial topic – nowadays, the opinion that it had none is quasi-universally accepted. In this paper, I shall begin by an overview of Wittgenstein’s relation to intuitionism, and then focus on two important topics, the Law of Excluded Middle and ‘following a rule’. On the first, I shall adduce evidence that he agreed with Brouwer’s reasoning, with his ‘weak counterexample’ using the decimal expansion of p (WVC, p. 71, AWL, p. 107 and M, p. 303). But Wittgenstein disagreed with Brouwer’s claim that the Law of Excluded Middle did not apply only for the ‘mathematics of the infinite’ (e. g ., PR § 73 or PG, p. 458); he believed that it does not apply even for elementary number theoretic equations. I shall argue that Wittgenstein’s position can only be understood in terms of the views laid out in the Tractatus Logico-Philosophicus, where a calculus of number-theoretic equations is presented: given that these are Scheinsätze and that logic applies to propositions, that calculus is meant to be logic-free. (This standpoint was further developed in the early 1930s, and led him, for example, to introduce a rule of uniqueness of a function defined by recursion, to do without mathematical induction.) On the second topic, Wittgenstein arrived at the following view of intuitionism in 1929: “each number has its individual properties […] Thus we never get away from the endlessly many individualities” (MS 106, p. 282). (This may not be an appropriate understanding of Brouwer’s views, but I shall leave this question aside.) But this raises a difficulty for the notion of a general rule and its application, since one “must recognize each time afresh that this rule may be applied […] No act of foresight can absolve me from this act of insight (Einsicht)” (PR, p. 171). See also Ambrose’s lectures notes, AWL, p. 133-134. We have here premises of the notorious ‘rule-following’ argument of PI §§ 143-242. (See, e.g., § 186 and LFM, p. 237 for a late critique of intuitionism along that line.) I shall end the paper by showing thus how the ‘rule-following’ argument embodies a critique of intuitionism, helping myself to recently published remarks by Waismann in his Oxford lectures on causality, and the current debate in analytic philosophy on ‘blind rule following’ sparks by paper by Paul Boghossian and Crispin Wright. --- Ryota Akiyoshi "An interpretation of Brouwer’s argument of the bar induction via infinitary proof theory" In a series of papers, Brouwer had developed intuitionistic analysis based on his concept of ``set”. In particular, he derived a key theorem called the fan theorem from another strong theorem called ``the bar induction”. Brouwer gave his argument to justify the bar induction in 1927, which is of great philosophical importance because it was one important source of the BHK-interpretation But the argument essentially depends on the assumption on the form of canonical proofs, so it has been considered as obscure or at least not evident. In this talk, we sketch an approach to understanding Brouwer’s argument via a tool in infinitary proof theory called the Omega-rule. This tool was introduced by Buchholz for ordinal analysis of impredicative theories. After explaining a historical background of the bar induction and basic notions in intuitionistic analysis, we introduce a version of the Omega-rule to analyze the bar induction and sketch how to embed the bar induction by it. By inspecting the embedding argument, we analyze the role of Brouwer’s assumption and conclude that his argument is mathematically well-motivated.

1 0

AIST Seminar on Software Reliability
by 山形賴之 10 Mar '15

10 Mar '15

皆様、産総研の山形です。重複して案内を受け取られた方にはお詫びいたします。下記の内容で、形式手法の実践的な側面に焦点を当てたセミナーを開催いたします。どなたでも参加できますが、参加される方は前日までに山形までご一報下さい。特にお車で参加される方はその旨お伝えください。 Dear everyone, I am pleased to announce "AIST Seminar on Software Reliability". This is a seminar on formal methods which is focused on industrial applications. The seminar is open to everyone, but please let me know by 3/19 if you want to join. In particular, if you come by a car, please let me know. AIST Seminar on Software Reliability date: Mar 20, 2015 Place: National Institute of Advanced Industrial Science and Technology (AIST), Tsukuba central, AIST Tsukuba Headquarters and Information Technology Collaborative Research Center Map: http://www.aist.go.jp/aist_e/guidemap/tsukuba/tsukuba_map.html http://www.aist.go.jp/aist_e/guidemap/tsukuba/center/tsukuba_map_c.html 14:00 - 14:45 Survey on concurrent model checkers, Yoriyuki Yamagata 14:45 - 15:00 Discussion 15:00 - 15:15 Break 15:15 - 16:00 Using Model Checking and Theorem Proving to Validate and Verify Cyber-Physical Systems, Chen-wei Wang 16:00 - 16:15 Discussion 16:15 - 16:30 Break 16:30 - 17:15 Applications of Model Checking on Different Systems using PAT, Liu Yang 17:15 - 17:30 Discussion 18:30 - Dinner Title: Survey on concurrent model checkers Speaker: Yoriyuki Yamagata Abstract: In this talk, we compare algorithms and performance benchmarks of concurrent model checkers Spin and LTSmin. The benchmarks suggests that LTSmin uses multicore quite efficiently, while Spin is optimized to singlecore. Title: Using Model Checking and Theorem Proving to Validate and Verify Cyber-Physical Systems Speaker: Chen-wei Wang Abstract: In this talk I present part of the results that contribute to the research project "Certification of Safety-Critical Software-Intensive Systems" funded by the Ontario government. The project involves various application domains: biomedical, automotive, and nuclear. This talk focuses on the nuclear domain. Contributions are made by researchers at York University and McMaster University. I first present the use of an automated checking tools for Timed Transition Models (TTM) to model, simulate, and validate cyber-physical systems, with respect to discrete-time temporal properties. I then present the use of tabular expressions and the PVS theorem prover to model and verify function blocks that can be reused to build Programmable Logic Controllers (PLCs). In both approaches, I use function blocks supplied by the industrial standard 61131-3 for illustration. To conclude the talk, I report lessons that we learn and mention ongoing research. Title: Applications of Model Checking on Different Systems using PAT Speaker: Liu Yang Abstract: Model checking is emerging as an effective software verification method with wide applications. However, still there are a lot research challenges in model checking techniques and in applying model checking techniques. To address these challenges, this talk presents our recent research contributions in the system modeling, efficient model checking algorithms development and the application of formal verification in concurrent objects design, cyber physical systems, security, multi-agent systems and pervasive systems. More important, we introduce a process analysis toolkit (PAT,www.patroot.com), which is a self-contained verification framework for specification, simulation and verification of concurrent, real-time and probabilistic systems. Since PAT is released 8 years ago, it has attracted 3500+ registered users world wide. Our vision is to achieve pervasive model checking so as to build a framework for realizing different verification techniques, and making model checking as planning, problem-solving, scheduling/services. Short Bio: Dr Liu Yang graduated in 2005 with a Bachelor of Computing (Honours) in the National University of Singapore (NUS). In 2010, he obtained his PhD and started his post doctoral work in NUS, MIT and SUTD. In 2011, Dr Liu is awarded the Temasek Research Fellowship at NUS to be the Principal Investigator in the area of Cyber Security. In 2012 fall, he joined School of Computer Engineering, Nanyang Technological University as a Nanyang Assistant professor. Dr. Liu specializes in software verification, security and software engineering. His research has bridged the gap between the theory and practical usage of formal methods to evaluate the design and implementation of software for high assurance. His work led to the development of a state-of-the-art model checker, Process Analysis Toolkit (PAT). This tool is used by research institutions in over 70 countries for research and education. He has more than 100 publications and leading a research group of 30 people. -- 山形頼之独立行政法人産業技術総合研究所主任研究員 https://staff.aist.go.jp/yoriyuki.yamagata/

2 1

Fwd: [TYPES/announce] CALCO 2015 : Last Call for Papers
by Ichiro Hasuo 10 Mar '15

10 Mar '15

========================================================= CALL FOR PAPERS: CALCO 2015 6th International Conference on Algebra and Coalgebra in Computer Science In cooperation with ACM SIGLOG June 24 - 26, 2015 Nijmegen, Netherlands http://coalg.org/calco15/ ========================================================== Abstract submission: March 22, 2015 Paper submission: April 2, 2015 Author notification: May 6, 2015 Final version due: June 3, 2015 ========================================================== -- 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) and Warsaw (Poland, 2013). The sixth edition will be held in Nijmegen, the Netherlands, colocated with MFPS XXXI. -- INVITED SPEAKERS -- Andy Pitts - University of Cambridge, UK (joint with MFPS) Chris Heunen - University of Oxford, UK Matteo Mio - CNRS, ENS Lyon, FR Daniela Petrisan - Radboud University, Nijmegen, NL -- 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 -- NEW TOPIC -- This edition of CALCO will feature a new topic, and submission of papers in this area is particularly encouraged. * 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. Starting with CALCO 2015, proceedings will be published in the Dagstuhl LIPIcsâ EURO "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=calco2015 -- BEST PAPER AND BEST PRESENTATION AWARDS -- Following from the successful trial at CALCO 2013, 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: March 22, 2015 Paper submission: April 2, 2015 Author notification: May 6, 2015 Final version due: June 3, 2015 -- PROGRAMME COMMITTEE -- Samson Abramsky, University of Oxford, UK Andrej Bauer, University of Ljubljana, SLO Filippo Bonchi, CNRS and ENS Lyon, FR Corina Cirstea, University of Southampton, UK Andrea Corradini, University of Pisa, IT Ross Duncan, University of Strathclyde, UK MartÃ-n EscardÃ³, University of Birmingham, UK Dan Ghica, University of Birmingham, UK Helle Hansen, Radboud University Nijmegen and CWI, NL Ichiro Hasuo, University of Tokyo, JP Bart Jacobs, Radboud University Nijmegen, NL Bartek Klin, University of Warsaw, PL Barbara KÃ¶nig, University of Duisburg-Essen, D Dexter Kozen, Cornell, US Alexander Kurz, University of Leicester, UK Paul-AndrÃ(c) MelliÃ¨s, CNRS and University Paris VII, FR Stefan Milus, University of Erlangen-NÃ 1/4 rnberg, D Larry Moss (co-chair), Indiana University, US Dusko Pavlovic, University of Hawaii, US Daniela Petrisan, ENS Lyon, FR Damien Pous, ENS Lyon, FR John Power, University of Bath, UK Jan Rutten, Radboud University Nijmegen and CWI, NL Lutz Schroeder, University of Erlangen-Nuernberg, D Monika Seisenberger, University of Swansea, UK Alexandra Silva, Radboud University Nijmegen, NL Pawel Sobocinski (co-chair), University of Southampton, UK Ana Sokolova, University of Salzburg, AT Andrzej Tarlecki, University of Warsaw, PL -- ORGANISING COMMITTEE -- Alexandra Silva Bart Jacobs Nicole Messink Sam Staton -- PUBLICITY -- Fabio Zanasi -- LOCATION -- Nijmegen is the oldest city in the Netherlands and celebrated its 2,000th year of existence in 2005. It is situated in the eastern province of Gelderland, quite near to the German border. The latin name for Nijmegen, `NoviomagusÂ´, is a reminder of its Roman past. `NoviomagusÂ´ means `new marketÂ´ and refers to the right to hold a market as granted by the Romans. In the days of Charlemagne, the city was called `NumagaÂ´; later on, this became `NieumeghenÂ´ and `NimmegenÂ´. However, citizens born and bred in Nijmegen speak affectionately of `NimwegenÂ´. Nijmegen is one of the warmest cities of the Netherlands, especially during summer, when the highest temperatures in the country are usually measured in the triangle Roermond â EURO " Nijmegen â EURO " Eindhoven. The lack of north-south oriented mountain ranges in Europe make this area prone to sudden shifts in weather, giving the region a semi-continental climate. -- SATELLITE WORKSHOPS -- The workshop is intended to enable presentation of work in progress and original research proposals. PhD students and young researchers are particularly encouraged to contribute. CALCO 2015 will run together with the CALCO Early Ideas Workshop, with dedicated Early Ideas sessions at the end of each conference day. -- CALCO Early Ideas Overview -- The CALCO Early Ideas Workshop invites submissions on the same topics as the CALCO conference: reporting 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. The list of topics of particular interest is shown on the main CALCO 2015 page. CALCO Early Ideas presentations will be selected according to originality, significance, and general interest, on the basis of submitted 2-page short contributions. It can be work in progress, a summary of work submitted to a conference or workshop elsewhere, or work that in some other way might be interesting to the CALCO audience. A booklet with the accepted short contributions will be made available. We encourage PhD students and young researchers to submit Early Ideas papers to the CALCO 2015 Easychair site as for ordinary submissions, mentioning in the abstract that the paper is to be considered for an Early Ideas talk. =========== SIGLOG Anti-harassment Policy The open exchange of ideas and the freedom of thought and expression are central to the values and goals of SIGLOG. They require an environment that recognizes the inherent worth of every person and group. They flourish in communities that foster mutual understanding and embrace diversity. For these reasons, SIGLOG is committed to providing a harassment-free conference experience, and implements the ACM policy against harassment (see http://www.acm.org/sigs/volunteer_resources/officers_manual/anti-harassment…). Conference participants violating these standards may be sanctioned or expelled from the meeting, at the discretion of the conference organizers. Conference organizers are requested to report serious incidents to the SIGLOG Chair. =========

1 0

教員公募（名古屋大学情報科学研究科・助教）
by NISHIMURA Harumichi 08 Mar '15

08 Mar '15

logic-mlの皆様，名古屋大学の西村です．このたび情報科学研究科計算機数理科学専攻にて教員を公募することになりましたのでお知らせします．所属：名古屋大学大学院情報科学研究科計算機数理科学専攻情報数理モデル論講座募集人員：助教（テニュアトラック教員）1 名専門分野：数理情報学（量子計算理論，量子情報理論，量子測定理論，機械学習，数理統計学，統計的データ解析，組合せ最適化，アルゴリズム，およびその関連分野）着任時期：平成27 年10 月1 日以降のできるだけ早い時期応募締切：平成27年5月29日（金）必着詳細は添付のPDFをご覧ください．よろしくお願いいたします．名古屋大学大学院情報科学研究科西村治道

1 0

LCC 2015 - Call for Papers
by Nao Hirokawa 08 Mar '15

08 Mar '15

皆様第16回論理と計算量に関するワークショップ LCC 2015 の論文募集をご案内致します。今回は７月に京都で開催される ICALP / LICS のサテライトワークショップとして開催されます。ぜひ投稿をご検討下さい！廣川　直 (JAIST) ====================================================================== First Call for Papers LCC 2015 16th International Workshop on Logic and Computational Complexity July 4-5, 2015, Kyoto, Japan collocated with ICALP/LICS 2015 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 April 19, 2015 * notification May 14, 2015 * workshop July 4-5, 2015 INVITED SPEAKERS: tba SUBMISSION: We 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. 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=lcc2015 PROGRAM COMMITTEE: * Albert Atserias (Universitat Politècnica de Catalunya, Barcelona) co-chair * Guillaume Bonfante (LORIA, Nancy) * Yijia Chen (Fudan University, Shanghai) * Ugo Dal Lago (Università degli Studi di Bologna) * Nao Hirokawa (JAIST, Nomi) co-chair * Antonina Kolokolova (Memorial University of Newfoundland) * Damiano Mazza (CNRS, LIPN - University Paris 13) * Georg Moser (University of Innsbruck) * Moritz Müller (Kurt Gödel Research Center for Mathematical Logic, Wien) * Benjamin Rossman (National Institute of Informatics, Tokyo) * Iddo Tzameret (Royal Holloway, University of London) * Heribert Vollmer (Leibniz Universität Hannover)

1 0

講演会 (Nadia Polikarpova氏)
by Atsushi Igarashi 06 Mar '15

06 Mar '15

皆様，京都大学の五十嵐です．以下の要領で MIT の Nadia Polikarpova さんの講演会を実施いたしますので，ふるってご参加ください．当日夕方には，簡単な懇親会も考えておりますので，興味のある方は五十嵐までご連絡ください．どうぞよろしくお願いいたします -- 五十嵐淳 (IGARASHI Atsushi) E-mail: igarashi(a)kuis.kyoto-u.ac.jp url: http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/ ---------------------------------------------------------------------- 日時: ３月１２日(木) 14:00〜15:00 場所: 京都大学吉田キャンパス総合研究７号館(旧工学部１０号館)１階１３１号室(セミナー室２) Title: A Fully Verified Container Library and Synthesis from Liquid Types Abstract: In this talk I will discuss two approaches to constructing provably correct programs: one is based on automated deductive verification, and the other one combines program synthesis and refinement types. The first part of my talk will present AutoProof: an automated deductive verifier for heap-manipulating object-oriented programs, as well as our experience using AutoProof to prove full functional correctness of a realistic general-purpose container library. While the comprehensive functionality and flexible design of container libraries pose nontrivial challenges to formal verification, our results indicate that verifying a realistic library (135 public methods, 8,400 LOC) is possible with moderate annotation overhead (1.4 lines of specification per LOC) and good performance (0.2 seconds per method on average). The second part of my talk builds upon the Liquid Types framework, which has been successfully used to verify a wide range of properties of functional programs with very little human interaction. The secret to this success is the encoding of program invariants using a combination of types and predicates from an SMT-decidable logic. I will discuss some ideas on how Liquid Type inference could be extended to infer program components, and ultimately synthesize programs that are correct by construction. Bio: Nadia Polikarpova is a postdoctoral researcher at MIT, where she works with Armando Solar-Lezama. She obtained her PhD at ETH Zurich in 2014. Her research interests are in program verification and synthesis.

1 0

Talk by G. Sambin and M. Maietti [13 Mar 15:30-]
by Shinya Katsumata 06 Mar '15

06 Mar '15

京都大学数理解析研究所の勝股です。 3月13日15:30から、University of PadovaのGiovanni Sambin氏とMaria Emilia Maietti氏に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 15:30-17:30, 13 Mar, 2015 Place: Rm 478, Research Building 2, Main Campus, Kyoto University http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (See 34) 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speaker: Giovanni Sambin and Maria Emilia Maietti (University of Padova) Title: 1 A new foundation of constructive mathematics 50 years after Bishop's FCA 2 Why developing mathematics in a two-level foundation Abstract: --- 1. Giovanni Sambin --- A new foundation of constructive mathematics 50 years after Bishop's FCA Bishop's book Foundations of constructive analysis, 1967, briefly CFA, showed that constructive mathematics can be emancipated from the subjective views of its founder Brouwer. That single book started the process turning constructive mathematics into a rich and lively research field and community, as it is today. While standing on the shoulders of such giants, after almost fifty years it is our task to see further. Some epochal changes which took place after 1967 provide motivations and support. Outside mathematics: 1. Evolutionary thought has expanded its range of application and is now commonly accepted in science, except in mathematics. The main challenge awaiting us is to pass from a static, transcendent view of mathematics to a dynamic, human one. 2. The power of computers and other tools has enormously increased. Their active role in mathematical research will certainly also increase. This requires fully detailed formal systems for the foundation of mathematics. 3. Diffusion of information technology makes our world intensely connected. One feels the need of a framework which allows for a plurality of different world views. Moreover, inside mathematics: 1. new branches have been created, 2. other branches besides analysis have been constructivized, such as algebra and topology. The talk will give a preliminary view on a new foundational system inspired by these facts, first introduced in 2005 and later developed by M. E. Maietti and myself and called the Minimalist Foundation, shortly MF. Aims of MF include: 1. to permit the development of constructive mathematics, including topology, in agreement with a dynamic view (different levels of abstractions, real and ideal entities,...), 2. to provide a framework in which virtually all foundations of mathematics can be expressed by adding some assumptions (hence the adjective minimalist) and hence in particular a good setting for reverse mathematics, 3. to allow formalization of mathematics in a computer language, 4. to express the computational content of mathematics. More specifically MF keeps: 1. an effective notion of set different from an ideal notion of collection 2. the notions of operation (with instructions) distinct from that of function (without instructions), 3. a positive notion of existence We wish to know that MF is consistent by a proof, not by faith or feelings. One can prove much more than consistency for MF, namely a normalization theorem, a realizability interpretation, implementation in a proof-assistant. We conclude the talk by showing that one needs a theory with two levels of abstraction, thus providing a good introduction to Maietti's talk. --- 2. Maria Emilia Maietti --- Why developing mathematics in a two-level foundation We provide motivations for developing mathematics in a two-level formal system following the ideas put forward in joint work with G. Sambin in [MS05]. There we introduced the notion of two-level system to found constructive mathematics but it turned out that the same notion can be accomodated to develop mathematics in general with computer-aided formalization of its proofs. A main motivating example of such foundations is the Minimalist Foundation for constructive mathematics which was ideated in [MS05] and completed into two levels in [M09]. Its peculiarity is that it is compatible with most relevant constructive and classical foundations at the "right level". Another perculiarity is that its design makes use of different languages: mostly that of type theory, but also that of category theory and axiomatic set theory. [MS05] M.E. Maietti and G. Sambin "Toward a minimalist foundation for constructive mathematics" in L. Crosilla and P. Schuster eds., ''From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics", Oxford University Press, 2005 [M09] M.E. Maietti "A minimalist two-level foundation for constructive mathematics" Annals of Pure and Applied Logic 160(2009):319-354

1 0

教員公募（名古屋大学情報科学研究科・准教授）
by Jacques Garrigue 05 Mar '15

05 Mar '15

PPLおよびlogic-mlの皆様、名古屋大学のGarrigueです。名古屋大学の結縁先生のご依頼で、教員公募（名古屋大学情報科学研究科・准教授）をお送りします。 ====================================== （重複してお受け取りの場合はご容赦ください。）名古屋大学の結縁です。メーリングリストをお借りして公募情報をお送りいたします。名古屋大学情報科学研究科情報システム学専攻准教授　１名応募期限　4/28(消印有効) ------------------------------------------- 平成 27 年 2 月 4 日関係各位名古屋大学大学院情報科学研究科研究科長　坂部俊樹教員の公募について（依頼）謹啓　時下ますますご清祥のことお慶び申し上げます．さて，この度当研究科では，下記の要領により，教員を公募いたします．つきましては，貴学（機関）関係者にご周知いただければ幸いです．謹白記 1. 公募対象：准教授 1 名（名古屋大学大学院情報科学研究科情報システム学専攻ソフトウェア論講座） 2. 専門分野：ソフトウェア科学 (プログラムの検証理論，検証技術など) 3. 担当科目：情報科学研究科情報システム学専攻の講義および大学院学生の指導，工学部電気電子・情報工学科の講義および学生の指導，全学教育の講義 4. 応募資格：博士の学位を有する方 5. 任期：なし 6. 着任時期：2015 年 10 月 1 日以降のできるだけ早い時期 7. 提出書類： (1) 履歴書（写真付き） (2) 研究業績リスト（著書，学術論文誌，国際会議などを区分して記述） (3) 主要論文別刷（主要なもの 3 編以内，コピーも可） (4) これまでの研究概要（A4 用紙 2 枚程度） (5) 今後の研究計画および教育についての抱負（A4 用紙 1 枚程度） (6) その他選考に役立つ情報（教育実績，学会および社会活動，獲得した外部資金，受賞，特許，ソフトウェア開発実績など） (7) 応募者の業績について問い合わせることのできる方 2 名の氏名と連絡先 8. 応募期限：2015 年 4 月 28 日（火）(郵送の場合，当日消印有効) 9. 書類提出先および問い合わせ先：〒 464-8603 名古屋市千種区不老町 C3-1（631）名古屋大学大学院情報科学研究科平成 26 年度情報システム学専攻長　高田広章 TEL: 052-789-5887 Email: hiro ＠ is.nagoya-u.ac.jp ★封筒に「情報システム学専攻教員応募書類在中」と朱書し，持参または書留で郵送して下さい． 10. 備考： (1) 応募書類は原則として返却しません． (2) 応募書類は本選考のみに使用し，他の目的には使用しません． (3) 選考の過程でプレゼンテーションをお願いすることがあります． (4) 本学では採用に際して男女共同参画に配慮しております． -- Shoji Yuen, Graduate School of Information Science, Nagoya Univ., Japan 結縁祥治　名古屋大学大学院情報科学研究科 +81-52-789-3649

1 0

情報処理学会全国大会企画「計算に潜む数理，計算としての数理 --- 証明はプログラミング！」のご案内
by Kazutaka Matsuda 04 Mar '15

04 Mar '15

logic-ml関係者の皆様，東京大学の松田です．複数受け取られた場合はご容赦ください．この場をお借りして，情報処理学会全国大会の企画の一つとして 3/17の13:00〜15:30より京都大学吉田キャンバス吉田南総合館 2F 共北26で開催される「計算に潜む数理，計算としての数理 --- 証明はプログラミング！」 http://www.gakkai-web.net/gakkai/ipsj/77program/html/event/A-6.html のご案内をさせていただきたく存じます．情報処理学会全国大会は当日のご参加も受けつけており，企画セッションのみの聴講は無料です．詳しくは以下をご欄下さい． http://www.ipsj.or.jp/event/taikai/77/on_site_registration.html 本セッションでは，論理と計算に関する以下の3件の講演を企画しております． # 田中一之（東北大学大学院理学研究科教授）「決定問題の相転移について」 1920年代にヒルベルト学派が数理論理学の中心テーマとして掲げた「決定問題」は，狭義には1階論理における真偽を判定する手続きを求める問題である．これはゲーデルやチューリングによってすぐに否定的に解かれたが，その後も様々な角度から類似の問題が提起され，肯定的にも否定的にも豊富な結果と解決手法が生れた．肯定的な手法としては，オートマトンの強化がしばしば有効であるが，それをさらに非決定性にすると顕著に決定不能な結果が得られることがある．たとえば，決定性ω文脈自由言語のゲームは（計算的に）決定可能だが，非決定性の場合は通常の集合論で決定できない．本講演では，決定問題の大きな流れを振り返りつつ，決定可能性と不可能性の相転移現象についていくつかの例をもとに考察する．文献：田中一之『チューリングとメタパズル』東京大学出版会2013．田中一之『無限ゲームとオートマトン』数学セミナー2014年11月号． # 佐藤雅彦（京都大学名誉教授）「計算と論理」プログラミングという行為の背景にある計算と論理について解説する．特に，「プログラム」，「計算」，「論理」という3つの概念に共通するキーワードである「証明」に焦点を合せて，これら3概念の共通点，相異点を明きらかにし，プログラミングという行為の本質に迫ることを目標とする．直観主義的型理論において発見された「カリー・ハワード同型対応」は，命題と型の同型性に基づき，（命題の）「証明」と（型の要素としての）「プログラム」を同一視するという「証明」の見方を与えた．これは確かに有力な「ものの見方」であり，型を持つプログラミング言語や型理論に基づく Coq 等の証明支援系の理論的基盤を与えている．本講演では，このような「カリー・ハワード同型対応」によるプログラム観を紹介し，その有用性と同時にそれが抱える問題点を指摘する．上の型理論的証明観の問題点を理解するために，型理論誕生の動機となった18世紀末から19世紀初頭にかけての，「数学の危機」とよばれた数学の基礎付けをめぐる問題とその解決策が何であったかを説明する．これにより型理論を絶対視することなく，より広い観点からプログラミングという行為の本質に迫りたい． # AFFELDT　Reynald （産業技術総合研究所セキュアシステム研究部門・高信頼ソフトウェア研究グループ主任研究員）「定理証明支援系Coqによる形式検証」ソフトウェアや数学の証明に誤りのないことを保証するのは重要な研究課題である．1970年代からカリー＝ハワード同型対応に基づく形式体系の研究が継続的に行われてきた．その形式体系が定理証明支援系という形式検証ツールとして実現された結果，厳密で現実的な形式検証が可能となった．例えば，クリティカルな基盤ソフトウェア（コンパイラやオペレーティングシステム等）と大規模な数学の証明（四色定理やケプラー予想等）の形式検証が近年相次いで成功し，IT業界でも形式検証はスマートカードの厳密な安全性評価に応用されている．本発表では，ソフトウェアと数学の形式検証の実例を通じて，定理証明支援系による形式検証の基本を説明する．特に，ACMによる受賞を契機に注目を集めているフランス国立情報学自動制御研究所（INRIA）で開発されているCoqという定理証明支援系を紹介する．どうぞご参加を検討いただけますと幸いです．

1 0

Workshop on secure quantum computing
by NISHIMURA Harumichi 02 Mar '15

02 Mar '15

logic-mlの皆様，名古屋大学の西村です．群馬大学の森前先生に代わって secure quantum computingのワークショップのご案内を以下に投稿させていただきます．参加費無料，レジストレーション不要です．ご興味のある皆様の参加をお待ちしております．名古屋大学大学院情報科学研究科西村治道 ---------------------------------------- メーリングリストの皆様、群馬大の森前と申します。３月１９，２０日に東大本郷キャンパスで行われるWorkshop on secure quantum computingについてご案内させて頂きます。 http://tomoyukimorimae.web.fc2.com/Workshop_on_secure_quantum_computing.html 宜しくお願いします。森前 -------------------------------------

1 0

CSL 2015 - call for papers
by Kazushige TERUI 01 Mar '15

01 Mar '15

みなさま Computer Sicence Logic 2015のご案内をさせていただきます。アブストラクト締切は４月３日となっております。どうぞ奮ってご投稿ください。照井 ______________________________________________________________________________________________ CSL 2015 COMPUTER SCIENCE LOGIC 2015 Berlin, 7 - 10 September 2015 http://logic.las.tu-berlin.de/csl2015/ Call for Papers _______________________________________________________________________________________________ AIM AND SCOPE Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. LOCATION The 24th EACSL Annual Conference on Computer Science Logic will be held at the Technical University Berlin from Monday, 7 September 2015 to Thurday, 10 September 2015. LIST OF TOPICS OF INTEREST (NON EXHAUSTIVE) • automated deduction and interactive theorem proving • constructive mathematics and type theory • equational logic and term rewriting • automata and games, game semantics • modal and temporal logic • model checking • decision procedures • logical aspects of computational complexity • finite model theory • computational proof theory • bounded arithmetic and propositional proof complexity • logic programming and constraints • lambda calculus and combinatory logic • domain theory • categorical logic and topological semantics • database theory • specification, extraction and transformation of programs • logical aspects of quantum computing • logical foundations of programming paradigms • verification and program analysis • linear logic • higher-order logic • nonmonotonic reasoning INVITED SPEAKERS * Martín Abadi (Santa Cruz) * Elham Kashefi (Edinburgh) * Markus Lohrey (Siegen) * Ryan Williams (Standford) IMPORTANT DATES Abstract submission: 3 April 2015 Paper Submission: 10 April 2015 Paper Notification: 13 June 2015 Conference: 7 - 10 September 2015 SUBMISSION Authors are invited to submit papers of not more than 15 pages in LIPIcs style presenting work not previously published. Papers are to be submitted through Easychair. Submitted papers must be in English and must provide sufficient detail to allow the PC to assess the merits of the paper. Full proofs may appear in a technical appendix which will be read at the reviewers' discretion. Authors are strongly encouraged to include a well written introduction which is directed at all members of the program committee. The submission is in two stages. Abstract submissions are due on 3 April 2015. Full paper submissions must be done on or before 10 April 2015. Papers must not be submitted concurrently to another conference with refereed proceedings. The PC chair should be informed of closely related work submitted to a conference or a journal. Papers authored or co-authored by members of the Programme Committee are not allowed. SATELLITE EVENTS * The 11th International Workshop on Fixed Points in Computer Science (FICS'15) will be held on 11 and 12 September 2015 as a co-located event of CSL’15. * YuriFest: we will celebrate Yuri Gurevich’s 75th birthday with a symposium in his honour on 11 and 12 September 2015 as a co-located event of CSL’15. * The annual meeting of the GI Fachgruppe Logik will be organised at the Technical University Berlin in conjunction with CSL'15. PROGRAMME COMMITTEE • Albert Atserias (Universitat Politècnica de Catalunya, Barcelona) • Achim Blumensath (Technical University Darmstadt) • Mikolaj Bojanczyk (Warsaw University) • Maria Paola Bonacina (Università degli Studi di Verona) • Patricia Bouyer-Decitre (LSV, CNRS & ENS de Cachan) • Ugo Dal Lago (Università di Bologna) • Maribel Fernández (King's College London) • Richard Garner (Macquarie University, Sydney) • Rajeev Goré (Australian National University, Canberra) • Stéphane Graham-Lengrand (CNRS & École Polytechnique, Paris-Saclay) • Martin Grohe (RWTH Aachen University) • Lauri Hella (University of Tampere) • Martin Hofmann (Ludwig-Maximilians-University Munich) • Stephan Kreutzer (Technical University Berlin, pc chair) • Martin Lange (University of Kassel) • Luigi Santocanale (LIF, Aix-Marseille Université & CNRS) • Alexandra Silva (Radboud University Nijmegen) • Alex Simpson (University of Edinburgh) • Sonja Smets (University of Amsterdam) • Makoto Tatsuta (National Institute of Informatics, Tokyo) • Kazushige Terui (Kyoto University) • James Benjamin Worrell (University of Oxford) • Nobuko Yoshida (Imperial College London) ORGANISING COMMITTEE: • Christoph Dittmann (Technical University Berlin) • Viktor Engelmann (Technical University Berlin) • Stephan Kreutzer (Technical University Berlin, Chair) • Jana Pilz (Technical University Berlin) • Roman Rabinovich (Technical University Berlin) • Sebastian Siebertz (Technical University Berlin) ------------------------------------------ Kazushige TERUI Research Institute for Mathematical Sciences, Kyoto University. Kitashirakawa Oiwakecho, Sakyo-ku, Kyoto 606-8502, JAPAN. Phone: +81-75-753-7235 Fax: +81-75-753-7276 terui(a)kurims.kyoto-u.ac.jp http://www.kurims.kyoto-u.ac.jp/~terui/

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 28 Feb '15

28 Feb '15

皆様ストックホルム大学のErik Palmgren先生の連続講義のお知らせです。ふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学研究科 e-mail: ishihara(a)jaist.ac.jp -------------------------------------------------- * JAIST Logic Seminar Series * * This seminar is held as a part of the EU FP7 Marie Curie Actions IRSES project CORCON (http://corcon.net/). Date: Lecture 1. Monday 9 March, 2015, 15:10-16:40 Lecture 2. Tuesday 10 March, 2015, 15:10-16:40 Lecture 3. Wednesday 11 March, 2015, 15:10-16:40 Place: JAIST, Lecture room I3-I4 (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Professor Erik Palmgren (Department of Mathematics, Stockholm University) Title: Lectures on type theory with a view towards formalizing Bishop-style mathematics Abstract: In this series of three lectures we give an introduction to Martin-Lof type theory and the tools it provides for formalizing Bishop-style constructive mathematics. The first lecture will cover basic principles of type theory and give an introduction to its manifestation in the well-known proof assistant Coq. In the second lecture we consider "Bishop's set theory" (Bishop and Bridges 1985) from the point of view of type theory, which will involve a development the theory of setoids and subsetoids. The third lecture will cover models constructive set theory (CZF) in type theory, and how it can be used to solve the problem of universes of setoids and development of category theory. Throughout the lectures we provide examples and suggestions how you can yourself experiment with the Coq system in the formalization of constructive mathematics. References E. Bishop and D.S. Bridges. Constructive Analysis. Springer 1985. E. Palmgren. Lecture notes on Type Theory. Stockholm 2014. URL: http://kurser.math.su.se/course/view.php?id=48 E. Palmgren and O. Wilander. Constructing categories and setoids of setoids in type theory. Logical Methods in Computer Science. 10(2014), Issue 3, paper 25.

1 1

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml