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

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

13 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 13 May '15

13 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 小野寛晰 13 May '15

13 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 10 Apr '15

10 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 10 Apr '15

10 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 10 Mar '15

10 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 09 Mar '15

09 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 07 Mar '15

07 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 03 Mar '15

03 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 28 Feb '15

28 Feb '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

論理哲学ワークショップ 2月27日(金) / Workshop on Philosophy of Logic, Feb 27th (Fri)
by Yuta Takahashi 25 Feb '15

25 Feb '15

みなさま、こんにちは、慶応大学の高橋優太と申します。この場をお借りして、次のワークショップをお知らせさせていただきます。重複して受け取られた場合はどうかご容赦ください。 ---- 論理哲学ワークショップ 2月27日(金) / Workshop on Philosophy of Logic, Feb 27th (Fri) 次のような「論理哲学ワークショップ」を予定しております。今回は特に、現代論理の歴史的背景についても議論します。参加自由です。 The following Workshop on Philosophy of Logic is scheduled. The historical background of some modern logic will be discussed among others. 日時/Date&Time: 2015年2月27日(金) 14:00-17:00, Feb 27 (Fri), 2015 場所: 慶應大学三田キャンパス南館地下4階ディスタンスラーニングルーム Place: Distance Learning Room (Basement 4F), South Building, Mita campus of Keio University. ( http://www.keio.ac.jp/en/maps/mita.html 13番の建物です。/ Building #13 on this map. ) ---- 1. Speaker: Juan Luis Gastaldi (IRePH, Université Paris Ouest Nanterre La Défense) Title: The relation between logical content and arithmetic in the semiotic constitution of Boolean logic 2. Speaker: Yuta Takahashi (Keio University) Title: The Intuitionistic Background of Gentzen's 1935/36 Consistency Proofs --------------------------------------------------------------------- 問合せ先: Mita Logic Seminar 思考と行動判断の研究拠点事務局 logic(a)abelard.flet.keio.ac.jp ABSTRACTS ENCLOSED BELOW: 1. Speaker: Juan Luis Gastaldi (IRePH, Université Paris Ouest Nanterre La Défense) Title: The relation between logical content and arithmetic in the semiotic constitution of Boolean logic Abstract: After the publication of his Begriffsschrift, Frege distanced himself from the Booleans by insistently opposing the content that his logic was able to express to the abstraction of Boolean logic. Frege’s commitment to the notion of content would last until the end of his work, becoming in particular the source of his famous distinction between sense and denotation. But what did Frege exactly mean by this opposition between “contentual” (inhaltlich) and abstract, as a properties of logical systems? A semiotic perspective on the constitution of Boolean logic shows that this distinction can be associated with the one between Arithmetic and Algebra, considered as different mathematical practices on signs respectively underpinning the constitution of these two logical systems. Moreover, a particular attention paid to Boole's own voluntary deviations from what would soon become the standard Boolean system permits to identify different figures of what can be seen as a content dimension arising as a logical effect of the semiotic properties of Arithmetic. 2. Speaker: Yuta Takahashi (Keio University) Title: The Intuitionistic Background of Gentzen's 1935/36 Consistency Proofs Abstract: Gerhald Gentzen gave three consistency proofs for number theory. These consistency proofs have a common aim that originates from Hilbert's Program. Hilbert, in his program, aimed to justify the use of ideal propositions in mathematics, by showing that no contradiction can be derived in a formal system of the ideal parts of mathematics. Gentzen aimed to justify the use of ideal propositions in number theory, and this aim is prominent especially in Gentzen's 1938 consistency proof. In Gentzen's 1935/36 consistency proofs, there is another aim that is not found in Hilbert's Program. The aim is to formulate a ``finitary'' interpretation that gives a meaning to every ideal proposition of number theory and makes the theory sound. In this talk, first we argue that what motivated Gentzen to give such an interpretation is an intuitionists' objection against the significance of consistency proofs. Second, we show that his way of the interpretation appealed to a notion being very close to the notion of spreads, which was introduced in intuitionistic mathematics. As a consequence, we claim that intuitionism was deeply related to both Gentzen's motivation and method for the interpretation. END OF ANNOUNCEMENT------------------------------------------------

1 0

KusatsuSeminar3/16--20: just a reminder
by Fujita Kenetsu 24 Feb '15

24 Feb '15

皆様，『ラムダ計算と論理の早春セミナー』のご案内　（再送）日程：2015年3月16日(月) 午後5時から3月20日(金) 正午まで場所：国立大学草津セミナーハウス　　　〒377-1711 群馬県吾妻郡草津町大字草津字白根737 詳細：http://www.cs.gunma-u.ac.jp/~fujita/2015.03LLSinKusatsu.htm 申込・質問などは藤田（群馬大学）までご連絡をお願いします．興味をお持ちのみなさまのご参加をお待ちしております． ----------- 群馬大学　藤田憲悦

1 0

論理哲学ワークショップ 2月27日(金) / Workshop on Philosophy of Logic, Feb 27th (Fri)
by Yuta Takahashi 24 Feb '15

24 Feb '15

みなさま、こんにちは、慶応大学の高橋優太と申します。この場をお借りして、次のワークショップのご案内をさせていただきます。重複して受け取られた場合はご容赦ください。 ---- 論理哲学ワークショップ 2月27日(金) / Workshop on Philosophy of Logic, Feb 27th (Fri) 次のような「論理哲学ワークショップ」を予定しております。今回は特に、現代論理の歴史的背景についても議論します。参加自由です。 The following Workshop on Philosophy of Logic is scheduled. The historical background of some modern logic will be discussed among others. 日時/Date&Time: 2015年2月27日(金) 14:00-17:00, Feb 27 (Fri), 2015 場所: 慶應大学三田キャンパス南館地下4階ディスタンスラーニングルーム Place: Distance Learning Room (B4F), South Building, Mita campus of Keio University. ---- 1. Speaker: Juan Luis Gastaldi (IRePH, Université Paris Ouest Nanterre La Défense) Title: The relation between logical content and arithmetic in the semiotic constitution of Boolean logic 2. Speaker: Yuta Takahashi (Keio University) Title: The Intuitionistic Background of Gentzen's 1935/36 Consistency Proofs --------------------------------------------------------------------- 問合せ先: Mita Logic Seminar 思考と行動判断の研究拠点事務局 logic(a)abelard.flet.keio.ac.jp ABSTRACTS ENCLOSED BELOW: 1. Speaker: Juan Luis Gastaldi (IRePH, Université Paris Ouest Nanterre La Défense) Title: The relation between logical content and arithmetic in the semiotic constitution of Boolean logic Abstract: After the publication of his Begriffsschrift, Frege distanced himself from the Booleans by insistently opposing the content that his logic was able to express to the abstraction of Boolean logic. Frege’s commitment to the notion of content would last until the end of his work, becoming in particular the source of his famous distinction between sense and denotation. But what did Frege exactly mean by this opposition between “contentual” (inhaltlich) and abstract, as a properties of logical systems? A semiotic perspective on the constitution of Boolean logic shows that this distinction can be associated with the one between Arithmetic and Algebra, considered as different mathematical practices on signs respectively underpinning the constitution of these two logical systems. Moreover, a particular attention paid to Boole's own voluntary deviations from what would soon become the standard Boolean system permits to identify different figures of what can be seen as a content dimension arising as a logical effect of the semiotic properties of Arithmetic. 2. Speaker: Yuta Takahashi (Keio University) Title: The Intuitionistic Background of Gentzen's 1935/36 Consistency Proofs Abstract: Gerhald Gentzen gave three consistency proofs for number theory. These consistency proofs have a common aim that originates from Hilbert's Program. Hilbert, in his program, aimed to justify the use of ideal propositions in mathematics, by showing that no contradiction can be derived in a formal system of the ideal parts of mathematics. Gentzen aimed to justify the use of ideal propositions in number theory, and this aim is prominent especially in Gentzen's 1938 consistency proof. In Gentzen's 1935/36 consistency proofs, there is another aim that is not found in Hilbert's Program. The aim is to formulate a ``finitary'' interpretation that gives a meaning to every ideal proposition of number theory and makes the theory sound. In this talk, first we argue that what motivated Gentzen to give such an interpretation is an intuitionists' objection against the significance of consistency proofs. Second, we show that his way of the interpretation appealed to a notion being very close to the notion of spreads, which was introduced in intuitionistic mathematics. As a consequence, we claim that intuitionism was deeply related to both Gentzen's motivation and method for the interpretation. END OF ANNOUNCEMENT------------------------------------------------

1 0

千葉 logic seminar
by arai toshiyasu 23 Feb '15

23 Feb '15

みなさま新井@千葉大学です。千葉 logic seminar の第5回のお知らせです。どなたでも参加できますのでどうぞ気軽にいらっしゃって下さい。問合せ先新井敏康（千葉大学） tosarai(a)faculty.chiba-u.jp ------------------------------------------ 日時：3月13日(金)13:30-15:00 場所：千葉大学理学部2号館105号室アクセスは http://www.chiba-u.ac.jp/campus_map/nishichiba/index.html の地図の黄色い理学部の中で数字2が付いている建物の1階です。 Speaker: Stan Wainer (Leeds UK) Title: A miniaturized predicativity Abstract: This talk attempts to characterize those recursive functions which are "predictably terminating" according to a finitistic point of view. The basis of the work is Leivant's (1995) theory of ramified induction over N, which has elementary recursive strength. It has been redeveloped and extended in various ways by many people. Eg. Spoors & W. (2012) built a hierarchy of ramified "input-output" theories whose strengths correspond to the levels of the Grzegorczyk hierarchy. Here, a further extension of this hierarchy is developed, with one additional input level on top (level omega). The underlying logic is an autonomously generated infinitary calculus with arbitrary finitely-many stratification levels of numerical inputs and a ramified Repetition Rule. The autonomous control on allowable ordinals is based on a weak (finitistic) notion of "pointwise transfinite induction". It turns out that the ordinal of this theory is then Gamma-0; the provably computable functions are those which are resource-bounded by the slow growing hierarchy; and these are the functions elementary recursive in the Ackermann function. ------------------------------------------------------------------------------------------

1 0

鈴木右京のセミナー (名古屋大学にて)
by Jacques Garrigue 19 Feb '15

19 Feb '15

logic-mlの皆さん、名古屋大学多元数理科学研究科のJacques Garrigueです。突然ですが、以下のセミナーを開催しますので、ご案内申し上げます。講演者:　鈴木佑京（東京大学大学院広域科学科）日時:　　2月24日（火）　10:30--12:00と13:00--14:30 会場:　　名古屋大学　理学A館　A328号室タイトル:　可述算術の世界アブストラクト: エドワード・ネルソンは、古典的算術に対するオルタナティブでありながら、直観主義的算術や有限主義的算術とも異なる――より徹底した構成主義の立場に立つ ――自然数論として、「可述算術」と呼ばれる理論を提案した。彼の理論は、後の限定算術の研究に影響をあたえるとともに、数学的帰納法に関する独特な分析を含んでおり、極めて興味深い。この講演では、１）まずネルソンの構成主義的な思想を説明した後、２）可述算術の数学的展開を解説することで、まず可述算術に対するイントロダクションを行う。そののち、３）ネルソンのような改訂主義とは異なる、講演者自身の観点から、可述算術の持つ概念的な興味を解説する。ここでは、可述算術が、ウィトゲンシュタインなどが展開した「概念形成としての数学」という描像をモデル化したものであることが主張される。

1 0

鈴木右京のセミナー (名古屋大学にて)
by Jacques Garrigue 19 Feb '15

19 Feb '15

1 0

Call for Papers: Hilbert’s Epsilon and Tau in Logic, Informatics and Linguistics
by Makoto Kanazawa 18 Feb '15

18 Feb '15

Call for Papers Hilbert’s Epsilon and Tau in Logic, Informatics and Linguistics Dates: June 10-12, 2015 Location: Montpellier, France Workshop Webpage: https://sites.google.com/site/epsilon2015workshop/ Contact email: Epsilon2015(a)easychair.org Submission deadline: April 1st, 2015 Submission webpage: https://easychair.org/conferences/?conf=epsilon2015 Organizers / workshop co-chairs: Stergios Chatzikyriakidis, LIRMM-CNRS, University of Montpellier Fabio Pasquali, University of Marseille Christian Retoré, University of Montpellier & LIRMM-CNRS Host: I2M-CNRS and University of Montpellier Workshop information: This workshop aims at promoting work on Hilbert’s epsilon calculus in a number of relevant fields ranging from Philosophy and Mathematics to Linguistics and Informatics. The Epsilon and Tau operators were introduced by David Hilbert, inspired by Russell's Iota operator for definite descriptions, as binding operators that form terms from formulae. One of their main features is that substitution with Epsilon and Tau terms expresses quantification. This leads to a calculus which is a strict and conservative extension of First Order Predicate Logic. The calculus was developed for studying first order logic in view of the program of providing a rigorous foundation of mathematics via syntactic consistency proofs. The first relevant outcomes that certainly deserve a mention are the two "Epsilon Theorems" (similar to quantifiers elimination), the first correct proof of Herbrand’s theorem or the use of the Epsilon operator in Bourbaki’s Éléments de Mathématique. Nowadays the interest in the Epsilon substitution method has spread in a variety of fields: Mathematics, Logic, Philosophy, History of Mathematics, Linguistic, Type Theory, Computer science, Category Theory and others. Submission The workshop welcomes submissions of up to 4 (but not less than 2) pages. Usual spacing, font and margin should be used (single-spaced, 11pt or larger, and 1 inch margin on A4 or letter size paper). Abstracts should be submitted by April 1st, 2015 as pdf files through the EasyChair conference system ( https://easychair.org/conferences/?conf=epsilon2015). An indicative list of themes that are of particular interest to the conference are (non-exhaustive): - History of Logic - Philosophy - Proof theory - Model theory - Category theory - Type theory - Quantification in Natural language - Noun-Phrases Semantics - Proof Assistants (e.g. Coq, Isabelle, ... ) - Other subnectors (e.g. Russell's iota, μ-operator, ... ) Reviewing: Abstracts will be reviewed by members of the program committee, and, where appropriate, outside reviewers. The organizers will be responsible for making decisions partly in consultation with the program committee. Notifications will be made by May 1st, 2015. Post-Proceedings: Selected papers from the workshop will appear as a special volume in Journal of Logics and their Applications Important dates: April 1st, 2015: Submission deadline May 1st,2015: Notification of acceptance June 10-12, 2015: Workshop Invited speakers: Claus-Peter Wirth (University of Saarland): The descriptive operators iota, tau and epsilon - on their origin, partial and complete specification, model- theoretic semantics, practical applicability (with the support of the Hilbert Bernays Project (sponsored by IFCoLog)). Vito Michele Abrusci (University of Roma Tre): Hilbert's tau and epsilon in proof theory. Hartley Slater (University of Western Australia): Linguistic and philosophical ramifications of the epsilon calculus. Program Committee: Daisuke Bekki (Ochanomizu University) Stergios Chatzikyriakidis (LIRMM-CNRS & University of Montpellier) Francis Corblin (University of Paris-Sorbonne & Institut Jean Nicod CNRS) Michael Gabbay (University of Cambridge) Makoto Kanazawa (National Institute of Informatics of Tokyo) Ruth Kempson (King's College, London) Alda Mari (CNRS Institut Jean Nicod & ENS & EHESS) Georg Moser (University of Innsbruck) Bruno Woltzenlogel Paleo (Vienna University of Technology) Michel Parigot (CNRS-PPS & University of Paris Diderot 7) Fabio Pasquali (University of Aix-Marseille & I2M CNRS) Christian Retoré (University of Montpellier & LIRMM-CNRS) Mark Steedman (University of Edimburgh) Richard Zach (University of Calgary)

1 0

PPL2015最終参加募集：第17回プログラミングおよびプログラミング言語ワークショップ
by Kazutaka Matsuda 16 Feb '15

16 Feb '15

logic-ml関係者の皆様，東京大学の松田です．複数受け取られた場合はご容赦ください． 3月4日（水）から3月6日（金）に道後温泉で開催される第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015) の参加募集の締切が2/17とせまっておりますので，再度の参加募集のご案内をお届けいたします．今回は， * 橋本和幸 (NVIDIA. 元日本シンボリックス株式会社) 「1980年代のLispマシンSymbolicsとその開発環境Genera 付属：NVIDIA GPUによる超並列コンピューティング」 * Chung-Kil Hur (Seoul National University) 「Formal C semantics and LLVM compiler validation」の二件の招待講演を予定しております．暫定プログラムを公開いたしました． http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/programme/tentative.txt カテゴリ1，2，4の採択論文・発表のリストも http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/accepted.html ご参考ください．参加登録の案内ページは http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/registration/ です．参加登録の締切は2月17日（火）です．どうぞお早めのご登録をお願い致します．多くの方々のご参加をお待ちしております． -------------------------------------------------------------------------- 第17回プログラミングおよびプログラミング言語ワークショップ（PPL2015） http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ 参加登録のご案内主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2015年3月4日(水)～3月6日(金) 会場: 愛媛県松山市道後温泉「道後プリンスホテル」 http://www.dogoprince.co.jp/ PPL2015は、プログラミングおよびプログラミング言語に関する研究者が一堂に会し、最新の研究成果の発表、および新たな研究課題についての討論やアイディア交換等を行うことを目的とした、合宿形式のワークショップです． ====================================================================== 参加登録ならびに宿泊予約を2月17日(火)まで日本旅行のWebサービスにて受け付けております． http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/registration/ をご参照いただき，ご登録ください．問い合わせ先：ppl2015-oc [at] kb.is.s.u-tokyo.ac.jp （[at]を@に置き換えてください） ====================================================================== プログラム委員会青戸等人東北大学浅田和之東京大学岩崎英哉電気通信大学鵜川始陽高知工科大学馬谷誠二京都大学 [プログラム共同委員長] 大岩寛産業技術総合研究所亀山幸義筑波大学河内谷清久仁日本IBM 久野靖筑波大学木村大輔国立情報学研究所宋剛秀神戸大学塚田武志 University of Oxford 中田景子 FireEye DresDen 浜名誠群馬大学 [プログラム共同委員長] 平井洋一 FireEye Dresden 平石拓京都大学藤田憲悦群馬大学星野直彦京都大学増原英彦東京工業大学渡部卓雄東京工業大学組織委員会松田一孝東京大学 [組織委員長] 浜名誠群馬大学 [プログラム共同委員長] 馬谷誠二京都大学 [プログラム共同委員長] 末永幸平京都大学上野雄大東北大学海野広志筑波大学木村大輔国立情報学研究所 [ポスターセッション幹事] --------------------------------------------------------------------------

1 0

PPL2015参加募集：第17回プログラミングおよびプログラミング言語ワークショップ
by Kazutaka Matsuda 13 Feb '15

13 Feb '15

logic-mlの皆様，東京大学の松田です．複数受け取られた場合はご容赦ください． 3月4日（水）から3月6日（金）に道後温泉で開催される第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015) の参加募集のご案内をお届けいたします．今回は， * 橋本和幸 (NVIDIA. 元日本シンボリックス株式会社) 「1980年代のLispマシンSymbolicsとその開発環境Genera 付属：NVIDIA GPUによる超並列コンピューティング」 * Chung-Kil Hur (Seoul National University) 「Formal C semantics and LLVM compiler validation」の二件の招待講演を予定しております．また，カテゴリ1，2，4の採択論文・発表のリストは http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/accepted.html からご欄になれます．多くの方々のご参加をお待ちしております．参加登録の案内ページは http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/registration/ です．参加登録の締切は2月17日（火）です．どうぞお早めのご登録をお願い致します．今年は昨年と異なり，*三日目は15:30終了予定*となります．ご注意ください． -------------------------------------------------------------------------- 第17回プログラミングおよびプログラミング言語ワークショップ（PPL2015） http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ 参加登録のご案内主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2015年3月4日(水)～3月6日(金) 会場: 愛媛県松山市道後温泉「道後プリンスホテル」 http://www.dogoprince.co.jp/ PPL2015は、プログラミングおよびプログラミング言語に関する研究者が一堂に会し、最新の研究成果の発表、および新たな研究課題についての討論やアイディア交換等を行うことを目的とした、合宿形式のワークショップです． ====================================================================== 参加登録ならびに宿泊予約を2月17日(火)まで日本旅行のWebサービスにて受け付けております． http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/registration/ をご参照いただき，ご登録ください．問い合わせ先：ppl2015-oc [at] kb.is.s.u-tokyo.ac.jp （[at]を@に置き換えてください） ====================================================================== プログラム委員会青戸等人東北大学浅田和之東京大学岩崎英哉電気通信大学鵜川始陽高知工科大学馬谷誠二京都大学 [プログラム共同委員長] 大岩寛産業技術総合研究所亀山幸義筑波大学河内谷清久仁日本IBM 久野靖筑波大学木村大輔国立情報学研究所宋剛秀神戸大学塚田武志 University of Oxford 中田景子 FireEye DresDen 浜名誠群馬大学 [プログラム共同委員長] 平井洋一 FireEye Dresden 平石拓京都大学藤田憲悦群馬大学星野直彦京都大学増原英彦東京工業大学渡部卓雄東京工業大学組織委員会松田一孝東京大学 [組織委員長] 浜名誠群馬大学 [プログラム共同委員長] 馬谷誠二京都大学 [プログラム共同委員長] 末永幸平京都大学上野雄大東北大学海野広志筑波大学木村大輔国立情報学研究所 [ポスターセッション幹事] --------------------------------------------------------------------------

1 0

講演会(Pawel Parys氏）
by koba 10 Feb '15

10 Feb '15

東京大学の小林と申します。以下のように、ワルシャワ大学のPawel Parys氏を招いて講演会を開催しますので、ふるってご参加ください。 Parysさんは、ここ数年、高階文法、高階プッシュダウンオートマトンなどについて未解決問題を解いたりしてよい仕事をされている方です小林直樹東京大学大学院情報理工学系研究科コンピュータ科学専攻〒113-0033 東京都文京区本郷7-3-1 Phone: 03-5841-4124 Fax: 03-5841-4124 email: koba(a)is.s.u-tokyo.ac.jp ---------------------------------- Time: 2月18日（水） 15:00〜 Place: 理学部7号館 214号室 Title: A Characterization of Lambda-terms Transforming Numbers Speaker: Pawel Parys (Warsaw University) Abstract: It is well known, that simply-typed lambda-terms can be used to represent numbers, as well as some other data types. We show that lambda-terms of each fixed (but possibly very complicated) type can be described by a finite piece of information (a set of appropriately defined intersection types) and by a vector of natural numbers. On one hand the description is compositional: having only the finite piece of information for two closed lambda-terms M and N, we can determine its counterpart for MN, and a linear transformation that applied to the vectors of numbers for M and N gives us the vector for MN. On the other hand, when a lambda-term represents a natural number, then this number is approximated by a number in the vector corresponding to this lambda-term. As a consequence, we prove that in a lambda-term of a fixed type we can store only a fixed number of natural numbers, in such a way that they can be extracted using lambda-terms. More precisely, while representing k numbers in a closed lambda-term of some type we only require that there are k closed lambda-terms M1,...,Mk such that Mi takes as argument the lambda-term representing the k-tuple, and returns the i-th number in the tuple (we do not require that, using lambda-calculus, one can construct the representation of the k-tuple out of the k numbers in the tuple). Moreover, the same result holds when we allow that the numbers can be extracted approximately, up to some error (even when we only want to know whether a set is bounded or not). All the results remain true when we allow the Y combinator (recursion) in our lambda-terms, as well as uninterpreted constants.

1 0

Prof. Georg Moser at NII Logic Seminar
by Makoto Tatsuta 07 Feb '15

07 Feb '15

Prof. Georg Moser at NII Logic Seminar Date: February 13, 2015, 14:00--16:00 Place: National Institute of Informatics, Room 1208 (12th floor) 場所: 国立情報学研究所 12階 1208室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Georg Moser (University of Innsbruck) Title: Amortised Cost Analysis and Term Rewrite Systems Abstract: I will present a univariate resource analysis for typed term rewrite systems based on a potential-based type system. This type system gives rise to polynomial bounds on the innermost runtime complexity. The thus obtained amortised resource analysis relates to polynomial interpretations and we obtain the perhaps surprising result that whenever a rewrite system can be well-typed, then there exists a polynomial interpretation that orients the system. If time permits I'll speak about very recent generalisations to a multivariate analysis. This is a joint work with Martin Hofmann. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

Fwd: [PVS] Topics in Theoretical Computer Science 205 (Tehran, Iran) -- Call for Papers
by Ichiro Hasuo 04 Feb '15

04 Feb '15

みなさま，東京大学の蓮尾です．8月にテヘランで行われる国際会議 TTCS の案内をお送りします．ICALP や TCS のように track A/B に分かれていて，スコープの広い会議です．ぜひ投稿をご検討ください．また，お近くの研究者のみなさん（特にこのメールが届かない，アルゴリズム系のみなさま）にこのメールを転送いただけると助かります．どうかよろしくお願いいたします．蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/ (apologies if you receive multiple copies) ========================================= Topics in Theoretical Computer Science (TTCS 2015) http://www.ttcs.ir/ Institute for Research in Fundamental Sciences (IPM), Tehran, Iran August 26-28, 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 0

ICTAC 2015 First call for papers
by Kohei SUENAGA 04 Feb '15

04 Feb '15

（複数お受け取りの場合はご容赦ください．）皆様，京都大学の末永です．今年10月にコロンビアで開かれる国際会議 ICTAC の論文募集をお送りします．ご投稿をお待ちしております．末永幸平 -- ********************************************************************** CALL FOR PAPERS -- ICTAC 2015 12th International Colloquium on Theoretical Aspects of Computing 29-31 October 2015, Cali, Colombia http://www.ictac2015.co DEADLINE FOR SUBMISSIONS: JUNE 5, 2015. ********************************************************************** ICTAC 2015 will take place at the campus of Universidad Javeriana, Cali, Colombia during October 29-31, 2015. The ICTAC conference series aims at bringing together practitioners and researchers to exchange ideas and experiences addressing challenges in theoretical aspects of computing as well as in exploiting theory through methods and tools for system development. ICTAC also aims to promote cooperation between participants and institutions from developing and industrial countries in research and education. THEMES AND TOPICS OF PAPERS Topics of interest include theories of computation and programming, foundations of software engineering and formal techniques in software design and verification, as well as tools that support formal techniques for software modeling, system design and verification. The topical areas of the conference include, but are not limited to * Automata theory and formal languages; * Principles and semantics of programming languages; * Theories of concurrency, mobility and reconfiguration; * Logics and their applications; * Software architectures, their models, refinement and verification; * Relationship between software requirements, models and code; * Program static and dynamic analysis and verification; * Software specification, refinement, verification and testing; * Model checking and theorem proving; * Models of object and component systems; * Coordination and feature interaction; * Integration of theories, formal methods and tools for engineering computing systems; * Service-oriented architectures: models and development methods; * Models of concurrency, security, and mobility; * Theory of distributed, grid and cloud computing; * Real-time, embedded, hybrid and cyber-physical systems; * Type and category theory in computer science. INVITED SPEAKERS * Jean-Raymond Abrial * Volker Diekert * César Muñoz * Catuscia Palamidessi * Davide Sangiorgi * Moshe Vardi * Glynn Winskel ASSOCIATED EVENTS * ICTAC Summer School on Formal Methods (October 25-27) * DCM 2015: 11th International Workshop on Developments in Computational Models (October 28) PAPER SUBMISSION == Important Dates * Abstract submission: Monday, June 1, 2015. * Paper submission: Friday, June 5, 2015. * Author notification: Monday, July 20, 2015. * Camera ready: Monday, August 3, 2015. == Paper Categories and Format We call for submissions, related to the above areas and topics, according to the following three categories: * Regular papers, with original research contributions; * Short papers, on recent work or proposals of emerging challenges; * Tool papers, on tools that support formal techniques for software modeling, system design and verification. Submissions should adhere to the LNCS format (see http://www.springer.de/comp/lncs/authors.html for details). Regular papers should not exceed 18 pages. Short and tool papers should not exceed 10 pages. Submissions to the colloquium must not have been published or be concurrently considered for publication elsewhere. All submissions will be judged on the basis of originality, contribution to the field, technical and presentation quality, as well as their relevance to the conference. ==Submission Link Papers must be submitted by using www.easychair.org/conferences/?conf=ictac2015. ==Proceedings As for the past editions, the proceedings of ICTAC 2015 will be published by Springer in the series Lecture Notes in Computer Science (LNCS). ==Special Issue Extended versions of selected papers from ICTAC 2015 will be invited to a special issue of Mathematical Structures in Computer Science (http://journals.cambridge.org/action/displayJournal?jid=MSC). GENERAL CHAIRS * Martin Leucker, University of Luebeck (DE). * Camilo Rueda, Pontificia Universidad Javeriana - Cali (CO). * Frank Valencia, CNRS and LIX, Ecole Polytechnique (FR). CONTACT CHAIR * Frank D. Valencia (frank.valencia(a)gmail.com). PROGRAM COMMITTEE * Nazareno Aguirre (AR) * Gerard Assayag (FR) * Mauricio Ayala-Rincón (BR) * Pablo Barceló (CL) * Gustavo Betarte (UY) * Filippo Bonchi (FR) * Marco Carbone (DK) * Ilaria Castellani (FR) * Néstor Cataño (CO) * Gabriel Ciobanu (RO) * Silvia Crafa (IT) * Pedro R. D'Argenio (AR) * Nicolas D'Ippolito (AR) * Stefan Dantchev (UK) * Rocco De Nicola (IT) * Yuxin Deng (CN) * Gilles Dowek (FR) * Moreno Falaschi (IT) * José Luiz Fiadeiro (UK) * Wan Fokkink (NL) * Fabio Gadducci (IT) * Julian Gutierrez (UK) * Stefan Haar (FR) * Thomas Hildebrandt (DK) * Einar Broch Johnsen (NO) * Bartek Klin (PL) * Marta Kwiatkowska (UK) * Kim G. Larsen (DK) * Martin Leucker (DE) (co-chair) * Etienne Lozes (FR) * Larissa Meinicke (AU) * Hernan Melgratti (AR) * Dominique Mery (FR) * Matteo Mio (FR) * Andrzej Murawski (UK) * Vivek Nigam (BR) * Mauricio Osorio (MX) * Prakash Panangaden (CA) * Jorge A. Pérez (NL) * Elaine Pimentel (BR) * António Ravara (PT) * Camilo Rocha (CO) * Camilo Rueda (CO) (co-chair) * Augusto Sampaio (BR) * Vijay Saraswat (US) * Vladimiro Sassone (UK) * Gerardo Schneider (SE) * Alexandra Silva (NL) * Jiri Srba (DK) * Jean-Bernard Stefani (FR) * Perdita Stevens (UK) * Kohei Suenaga (JP) * Alwen Tiu (SG) * Kazunori Ueda (JP) * Frank Valencia (FR) (co-chair) * Vasco T. Vasconcelos (PT) * Kapil Vaswani (IN) * Björn Victor (SE) * Igor Walukiewicz (FR) * Farn Wang (TW) * Alan Wassyng (CA) * Gianluigi Zavattaro (IT) -- Kohei Suenaga (末永幸平), Ph.D Associate professor (准教授) Graduate School of Informatics, Kyoto University (京都大学情報学研究科) ksuenaga(a)gmail.com http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/

1 0

JAIST Logic Workshop Series 2015
by Hajime Ishihara 03 Feb '15

03 Feb '15

皆様来年3月に金沢で開催されるJAIST Logic Workshop Series 2015のお知らせです。ふるってご投稿・ご参加ください。問合せ先：石原　哉・木原貴行・根元多佳子・横山啓太北陸先端科学技術大学院大学情報科学研究科 e-mail: jlws2015(a)jaist.ac.jp -------------------------------------------------------- *Call for Abstracts* JAIST LOGIC WORKSHOP SERIES 2015 Constructivism and Computability 2 March 2015 – 6 March 2015 Shiinoki Cultural Complex, Kanazawa, Japan http://www.jaist.ac.jp/is/labs/ishihara-lab/jlws2015/ -------------------------------------------------------- IMPORTANT DATES November 30 - deadline for abstract submissions December 25 - notification of accepted contributions February 15 - deadline for registrations March 2-6 - Constructivism and Computability workshop TUTORIALS * Giovanni Sambin (University of Padova) * Hideki Tsuiki (Kyoto University) * Stanley Wainer (University of Leeds) INVITED SPEAKERS * Ulrich Berger (Swansea University) * Takayuki Kihara (JAIST) * Graham Leigh (Vienna University of Technology) * Michael Rathjen (University of Leeds) * Masahiko Sato (Kyoto University) * Makoto Tatsuta (National Institute of Informatics) PROGRAM COMMITTEE * Toshiyasu Arai (Chiba University) * Andrej Bauer (University of Ljubljana) * Ulrich Berger (Swansea University) * Hajime Ishihara (co-chair, JAIST) * Masahiro Kumabe (Open University of Japan) * Erik Palmgren (Stockholm University) * Peter Schuster (University of Leeds) * Helmut Schwichtenberg (co-chair, LMU Munich) * Dieter Spreen (University of Siegen, UNISA Pretoria) * Kazuyuki Tanaka (Tohoku University) SUBMISSIONS Submissions of short abstracts (1 page in PDF format) are accepted through easychair.org, see https://easychair.org/conferences/?conf=jlws2015 DESCRIPTION JAIST Logic Workshop Series is a workshop series bringing together researchers from mathematical logic and its application, especially to artificial intelligence and software science. Each workshop has its own focus on a specific area of research in mathematical logic and its application. Previous workshops have been held in Kanazawa 2013, 2014 and 2014: http://www.jaist.ac.jp/~hirokawa/pr2013/ http://www.jaist.ac.jp/~preining/wpp/ http://www.jaist.ac.jp/~v-sano/jw2014/index.html In 2015, JAIST Logic Workshop Series focuses on “Constructivism and Computability” aiming at interaction and knowledge transfer between constructive mathematics and computability theory. The workshop is held being affiliated with EU FP7 Marie Curie Actions IRSES projects COMPUTAL (http://computal.uni-trier.de/) and CORCON (http://corcon.net/), but is open to all researchers in the areas. SCOPE Constructive mathematics and computability, and related areas including but not limited to: intuitionistic logic and type theory, proof theory, constructive analysis and topology, program extraction from proofs, recursion theory, computable analysis and topology, classical/constructive reverse mathematics, algorithmic randomness, real number computation etc. LOCAL ORGANIZERS * Hajime Ishihara (JAIST) * Takayuki Kihara (JAIST) * Takako Nemoto (JAIST) * Keita Yokoyama (JAIST) The workshop is supported by: * Japan Advanced Institute of Science and Technology (JAIST) CO-LOCATED WORKSHOP * JSPS-NUS Joint Workshop in Mathematica Logic and Foundations of Mathematics (6-7 March 2015, at the same venue)

1 2

ICALP 2015 CfP
by Shinya Katsumata 27 Jan '15

27 Jan '15

京都大学の勝股です。投稿締切まで３週間となりましたICALP2015のご案内です。 ---------- ICALP 2015 http://www.kurims.kyoto-u.ac.jp/icalp2015/ Second Call for Papers ====================== The 42nd International Colloquium on Automata, Languages, and Programming (ICALP) will take place in the period 6-10 July 2015 in Kyoto, Japan. The conference will co-locate with LICS 2015, the 30th ACM/IEEE Symposium on Logic in Computer Science. The ICALP 2015 conference chair is Kazuo Iwama (Kyoto University). ICALP is the main conference and annual meeting of the European Association for Theoretical Computer Science (EATCS). As usual, the main conference will be preceded and/or followed by a series of workshops. Important dates --------------- Submission deadline: Tuesday, 17 February 2015, 23:59 PST (Pacific Standard Time, UTC-8) Author notification: 15 April 2015 Final manuscript due: 30 April 2015 Deadlines are firm; late submissions will not be considered. Proceedings ----------- ICALP proceedings are published in the Springer-Verlag ARCoSS (Advanced Research in Computing and Software Science) subseries of LNCS (Lecture Notes in Computer Science). Invited Speakers ================= Ken Kawarabayashi, NII, Japan Valerie King, University of Victoria, Canada Thomas Moscibroda, MSR Asia, China Anca Muscholl, Universite Bordeaux, France (Joint with LICS) Peter O'Hearn, Facebook, UK (Joint with LICS) Invited Tutorial Speakers (Joint with LICS) ------------------------------------------- Piotr Indyk, MIT, USA Andrew Pitts, University of Cambridge, UK Geoffrey Smith, Florida International University, USA Masterclass speaker ------------------- Ryuhei Uehara, JAIST, Japan Topics ====== Papers presenting original research on all aspects of theoretical computer science are sought. Typical but not exclusive topics of interest are: Track A: Algorithms, Complexity and Games ----------------------------------------- * Algorithmic Game Theory * Approximation Algorithms * Combinatorial Optimization * Combinatorics in Computer Science * Computational Biology * Computational Complexity * Computational Geometry * Cryptography * Data Structures * Design and Analysis of Algorithms * Machine Learning * Parallel, Distributed and External Memory Computing * Randomness in Computation * Quantum Computing Track B: Logic, Semantics, Automata and Theory of Programming ------------------------------------------------------------- * Algebraic and Categorical Models * Automata, Games, and Formal Languages * Emerging and Non-standard Models of Computation * Databases, Semi-Structured Data and Finite Model Theory * Principles and Semantics of Programming Languages * Logic in Computer Science, Theorem Proving and Model Checking * Models of Concurrent, Distributed, and Mobile Systems * Models of Reactive, Hybrid and Stochastic Systems * Program Analysis and Transformation * Specification, Refinement, Verification and Synthesis * Type Systems and Theory, Typed Calculi Track C: Foundations of Networked Computation: Models, Algorithms and Information Management ------------------------------------------------------ * Algorithmic Aspects of Networks and Networking * Formal Methods for Network Information Management * Foundations of Privacy, Trust and Reputation in Networks * Mobile and Wireless Networks and Communication * Network Economics and Incentive-Based Computing Related to Networks * Networks of Low Capability Devices * Network Mining and Analysis * Overlay Networks and P2P Systems * Specification, Semantics, Synchronization of Networked Systems * Theory of Security in Networks Submission Guidelines -------------------- Authors are invited to submit an extended abstract of no more than 12 pages, including references, in LNCS style presenting original research on the theory of Computer Science. All submissions will be electronic via the EasyChair page for the conference, with three tracks (A, B and C): https://easychair.org/conferences/?conf=icalp2015 Submissions should be made to the appropriate track of the conference. No prior publication or simultaneous submission to other publication outlets (either a conference or a journal) is allowed. Submissions must adhere to the specified format and length. Submissions that are too long or formatted incorrectly may be rejected immediately. All the technical details that are necessary for a proper scientific evaluation of a submission must be included in a clearly-labelled appendix, to be consulted at the discretion of program committee members. This includes, in particular, the proofs of all the key theorems in a paper. Should I submit my paper to Track A or Track C? ------------------------------------------------ While the scope of Tracks A and B are generally well understood given their long history, the situation for Track C may be less obvious. In particular, some clarifications may be helpful regarding areas of potential overlap, especially between Tracks A and C. The aim for Track C is to be the leading venue for theory papers truly motivated by networking applications, and/or proposing theoretical results relevant to real networking, certified analytically, but not necessarily tested practically. The motivation for the track was the lack of good venues for theory papers motivated by applications in networking. On the one hand, the good networking conferences typically ask for extended experiments and/or simulations, while the TCS community is hardly able to do such experiments or simulations. On the other hand, the good conferences on algorithms tend to judge a paper based only on its technical difficulty and on its significance from an algorithmic perspective, which may not be the same as when judging the paper from the perspective of impact on networks. Several areas of algorithmic study of interest to track C have a broad overlap with track A. Graph algorithmics can belong in either, though if the work is not linked to networking, it is more appropriate in track A. Algorithmic game theory is another area of major overlap. Aspects involving complexity, the computation of equilibria and approximations, belong more in Track A, while results with applications in auctions, networks and some aspects of mechanism design belong in Track C. Finally, it should be noted that algorithms and complexity of message-passing based distributed computing belong squarely in track C, while certain other aspects of distributed computing do not fall under its scope. Best Paper Awards ----------------- As in previous editions of ICALP, there will be best paper and best student paper awards for each track of the conference. In order to be eligible for a best student paper award, a paper should be authored only by students and should be marked as such upon submission. Committees ========== Track A: Algorithms, complexity, and games ------------------------------------------ Peyman Afshani, Aarhus University, Denmark Hee-Kap Ahn, POSTECH, South Korea Hans Bodlaender Utrecht University, The Netherlands Karl Bringmann, Max-Planck Institut für Informatik, Germany Sergio Cabello, University of Ljubljana, Slovenia Ken Clarkson, IBM Almaden Research Center, USA Eric Colin de Verdiere, École Normale Supérieure Paris, France Stefan Dziembowski, University of Warsaw, Poland David Eppstein, University of California at Irvine, USA Dimitris Fotakis, National Technical University of Athens, Greece Paul Goldberg, University of Oxford, UK MohammadTaghi Hajiaghayi, University of Maryland at College Park, USA Jesper Jansson, Kyoto University, Japan Andrei Krokhin, Durham University, UK Asaf Levin, Technion, Israel Inge Li Gortz, Technical University of Denmark, Denmark Pinyan Lu, Microsoft Research Asia, China Frederic Magniez, Universite Paris Diderot, France Kazuhisa Makino, Kyoto University, Japan Elvira Mayordomo, Universidad de Zaragoza, Spain Ulrich Meyer, Goethe University Frankfurt am Main, Germany Wolfgang Mulzer, Free University Berlin, Germany Viswanath Nagarajan, University of Michigan, USA Vicky Papadopoulou, European University Cyprus, Cyprus Michal Pilipczuk, University of Bergen, Norway Liam Roditty, Bar-Ilan University, Israel Ignaz Rutter, Karlsruhe Institute of Technology, Germany Rocco Servedio, Columbia University, USA Jens Schmidt, TU Ilmenau, Germany Bettina Speckmann (chair), TU Eindhoven, The Netherlands Csaba D. Toth, California State University Northridge, USA Takeaki Uno, National Institute of Informatics, Japan Erik Jan van Leeuwen, Max-Planck Institut für Informatik, Germany Rob van Stee, University of Leicester, UK Ivan Visconti, University of Salerno, Italy Track B: Logic, semantics, automata and theory of Programming ------------------------------------------------------------- Andreas Abel, Chalmers and Gothenburg University, Sweden Albert Atserias, Universitat Politècnica de Catalunya, Spain Christel Baier, TU Dresden, Germany Lars Birkedal, Aarhus University, Denmark, Luis Caires, Universidade Nova de Lisboa, Portugal James Cheney, University of Edinburgh, UK Wei Ngan Chin, National University of Singapore, Singapore Ugo Dal Lago, University of Bologna, Italy Thomas Ehrhard, CNRS, Université Paris Diderot, France Zoltan Esik, University of Szeged, Hungary Xinyu Feng, University of Science and Technology of China, China Wan Fokkink, VU University Amsterdam, The Netherlands Shin-ya Katsumata, Kyoto University, Japan Naoki Kobayashi (chair), The University of Tokyo, Japan Eric Koskinen, New York University, USA Antonín Kucera, Masaryk University, Czech Republic Orna Kupferman, Hebrew University, Israel Annabelle Mclver, Macquarie University, Australia Dale Miller, INRIA Saclay, France Markus Mueller-Olm, University of Münster, Germany Andrzej Murawski, Univeristy of Warwick, UK Joel Ouaknine, Univeristy of Oxford, UK Prakash Panangaden, McGill University, Canada Pawel Parys, University. of Warsaw, Poland Reinhard Pichler, TU Vienna, Austria Simona Ronchi Della Rocca, University of Torino, Italy Jeremy Siek, Indiana University, USA Track C: Foundations of networked computation: Models, algorithms and information management ------------------------------------------------------ Ioannis Caragiannis, Univ. Patras, Greece Katarina Cechlarova, Pavol Jozef Safarik Univ., Slovakia Shiri Chechik, Tel Aviv Univ., Israel Yuval Emek, Technion, Israel Sandor Fekete, TU Braunschweig, Germany Pierre Fraigniaud, CNRS and Paris Diderot, France Leszek Gasieniec, Univ. Liverpool, UK Aristides Gionis, Aalto Univ., Finland Magnus M. Halldorsson (chair), Reykjavik Univ, Iceland Monika Henzinger, Univ. Wien, Austria Bhaskar Krishnamachari, USC, USAL Fabian Kuhn, Freiburg, Germany Michael Mitzenmacher, Harvard Univ, USA Massimo Merro, Univ. Verona, Italy Gopal Pandurangan, Univ. Houston, USA Pino Persiano, Salerno, Italy R. Ravi, CMU, USA Ymir Vigfusson, Emory Univ., USA Roger Wattenhofer, ETH Zurich, Switzerland Masafumi Yamashita, Kyushu Univ., Japan

1 0

Kobe Colloquium on Logic, Statistics and Informatics, January 27 (Monroe Eskew)
by Joerg Brendle 25 Jan '15

25 Jan '15

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。日時：2014年1月27日（火）13:20-14:50 講演者：Monroe Eskew （筑波大学）場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室） ============================================================ 題目： A global version of Chang’s conjecture アブストラクト： In the 80s, Foreman showed the consistency of (aleph_{n+1},aleph_n) —>> (aleph_{m+1},aleph_m) holding simultaneously for all natural numbers n > m, starting from a 2-huge cardinal. He asked whether a global version of Chang’s conjecture is consistent. We answer this, showing that it is consistent from the same hypothesis that for all pairs of regular cardinals mu < kappa, (kappa^+,kappa) —>> (mu^+,mu). The method uses a relatively simple forcing iteration, and it answers some technical questions raised by Shioya. We also discuss some related issues about singular cardinals. ============================================================ 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm

1 0

JSPS-NUS Joint Workshop in Logic
by Tanaka Kazuyuki 25 Jan '15

25 Jan '15

JSPS-NUS二国間共同研究のロジック・ワークショップのご案内シンガポールとの二国間交流事業（代表：田中、Chong）の一環として下記の研究会を開催致します。 Workshop in Mathematical Logic and Foundations of Mathematics 日程：2015年3月6日(金) から3月8日(日) まで場所：金沢しいのき迎賓館および金沢東急ホテルこのワークショップは主に共同研究のメンバーによって行われるものですが、ご関心のある方は一般からもご参加いただけます。但し、会場準備の都合上事前登録者に限りますので参加希望の方は SendaiLogic[at]math.tohoku.ac.jp （締切２月８日）までご連絡ください。下記のページで＜英語＞でもご案内しております。 http://www.math.tohoku.ac.jp/~tanaka/kanazawa2015.html よろしくお願いします。　東北大学　田中一之コンタクト：　SendaiLogic[at]math.tohoku.ac.jp

1 0

『第２回山陰基礎論・解析学研究集会』の御案内
by Horihata Yoshihiro 23 Jan '15

23 Jan '15

皆様米子高専の堀畑です．明日と明後日に米子で件名の研究会を開きます．ホームページ https://sites.google.com/site/yonagonctmath/slas2015 参加自由です．よろしくお願いいたします．参加者リスト阿部吉弘（神奈川大学）池上大祐（神戸大学）薄葉季路（神戸大学）嘉田勝（大阪府立大学）木原貴行（ＪＡＩＳＴ）熊本真一郎（金沢大学）倉橋太志（木更津高専）古清水大直（米子高専）小林玉青（米子高専）小浪吉史（島根大学）静間荘司（大阪府立大学）柴田孝祐（米子高専，建築学科５年）高木啓行（信州大学）竹内耕太（筑波大学）根元多佳子（ＪＡＩＳＴ）濱田裕康（佐世保高専）樋口幸治郎（千葉大学）吉居啓輔（沖縄高専）吉田聡（鳥取環境大学）米子高専・数学同好会学生３人世話人：堀畑佳宏 -- 米子工業高等専門学校教養教育科・数学〒683-8502 鳥取県米子市彦名町4448 Tel: 0859-24-5075 E-mail: horihata(a)yonago-k.ac.jp

1 0

Re: [logic-ml] メーリングリストへの配信願い
by Atsushi Igarashi 21 Jan '15

21 Jan '15

logic-ml のみなさま，五十嵐＠logic-ml管理人です．成蹊大学・理工学部・情報科学科の山本様からの依頼での代理投稿です． ---------------------------------------------------------- logic-ml の皆様，成蹊大学・理工学部・情報科学科の山本と申すものです．以下のように，当学科で助教の公募を行っています．募集期間が短く申し訳ありませんが，ご関心のある方々の応募をお待ちしております． 1. 募集人員：助教１名 (任期付き) 2. 所属：理工学部情報科学科 3. 専門分野：計算機科学・情報科学における理論分野全般 4. 着任時期：２０１５年５月１日（金） 5. 応募締切：２０１５年２月１４日（土）（必着）詳細は，下記 URL をご参照下さい． http://www.seikei.ac.jp/gakuen/recruit/teacher/university.html 以上．

1 0

PPL2015参加登録開始がご案内：第17回プログラミングおよびプログラミング言語ワークショップ
by Kazutaka Matsuda 16 Jan '15

16 Jan '15

logic-ml関係者の皆様，東京大学の松田です．複数受け取られた場合はご容赦ください． 3月4日（水）から3月6日（金）に道後温泉で開催される第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015) の参加登録を開始いたしましたで，そのご案内をお届けいたします．今回は， * 橋本和幸 (NVIDIA. 元日本シンボリックス株式会社) 「1980年代のLispマシンSymbolicsとその開発環境Genera 付属：NVIDIA GPUによる超並列コンピューティング」 * Chung-Kil Hur (Seoul National University) 「Formal C semantics and LLVM compiler validation」の二件の招待講演を予定しております．多くの方々のご参加をお待ちしております．参加登録の案内ページは http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/registration/ です．参加登録の締切は2月17日（火）です．どうぞお早めのご登録をお願い致します．今年は昨年と異なり，*三日目は全日開催*となります．ご注意ください．また，カテゴリ2（国外既発表論文），4（サーベイ・チュートリアル）の申し込みは 2015年1月23日(金) 17:00 (JST) まで，カテゴリ3（ポスター・デモ発表）の申し込みは 2015年2月6日(金) 17:00 (JST) まで受け付けております．こちらも http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ をご参照の上，投稿をご検討いただけますと幸いです． -------------------------------------------------------------------------- 第17回プログラミングおよびプログラミング言語ワークショップ（PPL2015） http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ 参加登録のご案内主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2015年3月4日(水)～3月6日(金) 会場: 愛媛県松山市道後温泉「道後プリンスホテル」 http://www.dogoprince.co.jp/ PPL2015は、プログラミングおよびプログラミング言語に関する研究者が一堂に会し、最新の研究成果の発表、および新たな研究課題についての討論やアイディア交換等を行うことを目的とした、合宿形式のワークショップです． ====================================================================== 参加登録ならびに宿泊予約を2月17日(火)まで日本旅行のWebサービスにて受け付けております． http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/registration/ をご参照いただき，ご登録ください．問い合わせ先：ppl2015-oc [at] kb.is.s.u-tokyo.ac.jp （[at]を@に置き換えてください） ====================================================================== プログラム委員会青戸等人東北大学浅田和之東京大学岩崎英哉電気通信大学鵜川始陽高知工科大学馬谷誠二京都大学 [プログラム共同委員長] 大岩寛産業技術総合研究所亀山幸義筑波大学河内谷清久仁日本IBM 久野靖筑波大学木村大輔国立情報学研究所宋剛秀神戸大学塚田武志 University of Oxford 中田景子 FireEye DresDen 浜名誠群馬大学 [プログラム共同委員長] 平井洋一 FireEye Dresden 平石拓京都大学藤田憲悦群馬大学星野直彦京都大学増原英彦東京工業大学渡部卓雄東京工業大学組織委員会松田一孝東京大学 [組織委員長] 浜名誠群馬大学 [プログラム共同委員長] 馬谷誠二京都大学 [プログラム共同委員長] 末永幸平京都大学上野雄大東北大学海野広志筑波大学木村大輔国立情報学研究所 [ポスターセッション幹事] --------------------------------------------------------------------------

1 0

Gilles Dowek教授講演会　１月１６日金曜日　三田ロジックセミナー
by Mitsuhiro Okada 14 Jan '15

14 Jan '15

次のようなセミナートークを予定しておりますのでご案内させていただきます。参加自由です。(日時が次のように変更しています。Please note that　the date/time changed as follows.) 　　　　　　　　慶應義塾大学文学部哲学専攻岡田光弘 ------------------------------ Mita Logic Seminar Jan.16th (Fri) 13:00-14:30 Place: Basement B1 , Meeting Room #3, North Building, Mita campus, Keio University　(Campus Map http://www.keio.ac.jp/en/maps/mita.html) １月１６日金曜日　１３時ー１４時半, 慶應義塾大学三田キャンパス北館地下一階第３会議室　(キャンパスマップhttp://www.keio.ac.jp/ja/access/mita.html） Speaker; Gilles Dowek, INRIA, France Title: Real numbers, chaos, and the principle of a bounded density of information Abstract: Two definitions of the notion of a chaotic transformation are compared: sensitivity to initial conditions and sensitivity to perturbations. Only the later is compatible with the idea that information has a finite density. 連絡先：思考と行動判断の研究拠点事務局（logic(a)abelard.flet.keio.ac.jp) ------------

1 0

PPL2015 ポスター発表申込み締切日訂正
by Makoto Hamana 13 Jan '15

13 Jan '15

皆様、すみませんです、先ほどご案内したPPL2015の案内メールのポスター・デモ発表申込み締切り日に間違いありましたので訂正させていただきます。 [訂正] カテゴリ3（ポスター・デモ発表）締切は 2015年2月6日(金) 17:00 (JST) です。カテゴリ4(サーベイ・チュートリアル)の方は1月23日〆で正しいです。 PPL 2015 Webページ http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ にあるものが正式な情報です。お騒がせして申し訳ありません。どうぞよろしくお願いいたします。 -- 浜名　誠群馬大学理工学府電子情報部門 http://www.cs.gunma-u.ac.jp/~hamana/

1 0

CFP: PPL2015 サーベイ・チュートリアル、ポスター発表募集
by Makoto Hamana 13 Jan '15

13 Jan '15

皆様、群馬大学の浜名です。来年3月に愛媛県松山市道後温泉で開催される第17回プログラミングおよびプログラミング言語ワークショップ PPL'15 2015年3月4日(水)〜3月6日(金) http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ のサーベイ・チュートリアル、ポスター発表申込みの案内をさせていただきます。 * サーベイ・チュートリアル発表 (カテゴリ4）は、今年のPPLからの試みで、プログラミング言語分野の学生、研究者に役立つようなサーベイ・チュートリアル発表を広く募集します。プログラミング言語理論も実装も歴史が深くなってきて、自分の特定専門分野の事は知っていても、なかなか他の小分野の事はよく知らないという事が多くなってきました。そこでプログラミング言語に関わる様々な理論、応用の小分野間の相互理解と全体の底上げとなる事を目指し、設置しました。既発表・未発表の別を問いません(申込みは簡単なアウトラインの提出のみ)。既存発表の解説論文、教科書、セミナーや講義での資料、経験などお持ちの方はそれを用いていただくのも便利かと思います。 - ある専門分野の事を皆にもっと知ってもらいたい！ - 難しい分野と言われているがアイデアはそんなことないから解説したい。 - 現在隆盛を誇っている分野はこんな風に発展してきた。あまり知られていないが自分の専門性から解説したい。 - 解説論文を出版したけど、これを発表で話したことはないな… - 自分もやってる活発な〇〇分野の研究動向をまとめたいけどなかなかきっかけがない。これを機にまとめようか。などいろいろパターン、動機はあるかと思います。上記どれか当てはまるような方、もちろんそれに限らず、ぜひ申込みいただければと思います。通常発表と同様の30分での発表を予定していますが、採択件数によっては発表者との相談で少し時間延長もできるかもしれません。通常研究発表とは違い、ある程度確立した分野の話、専門家の方にお願いできればと思っております。PPLへの関連および関連研究への言及をもとに採録を判定いたします。 * ポスター・デモ発表 (カテゴリ3)は例年盛況な2時間程度のセッション内でのポスター発表またはデモ発表です。既発表・未発表の別を問いません。今年はポスター賞も設置しました。申込み多数の場合はプログラム委員会での選考により採否を決定します。締切はどちら(カテゴリ3,4)も、来週末 2015年1月23日(金) 17:00 (JST) ですので、ぜひ申込みをご検討ください。詳しい申込み方法などは http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ ご参照ください。 -- 浜名　誠群馬大学理工学府電子情報部門 http://www.cs.gunma-u.ac.jp/~hamana/

1 0

KusatsuSeminar3/16--20
by Fujita Kenetsu 13 Jan '15

13 Jan '15

皆様，『ラムダ計算と論理の早春セミナー』のご案内日程：2015年3月16日(月) 午後5時から3月20日(金) 正午まで場所：国立大学草津セミナーハウス　　　〒377-1711 群馬県吾妻郡草津町大字草津字白根737 詳細：http://www.cs.gunma-u.ac.jp/~fujita/2015.03LLSinKusatsu.htm 申込・質問などは藤田（群馬大学）までご連絡をお願いします．興味をお持ちのみなさまのご参加をお待ちしております． ----------- 群馬大学　藤田憲悦

1 0

Ninth NII Type Theory Workshop
by Makoto Tatsuta 11 Jan '15

11 Jan '15

Ninth NII Type Theory Workshop Date: January 15, 2015, 10:20--17:30 Place: National Institute of Informatics, Room 1208 (12th floor) 場所: 国立情報学研究所 12階 1208室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Program: 10:20--11:00 Daisuke Kimura (National Institute of Informatics) Title: A framework of models of functional PTSs 11:00--11:40 Josh Ko (National Institute of Informatics) Title: Relational algebraic ornamentation 11:40--13:10 Lunch Break 13:10--13:50 Makoto Fujiwara (Tohoku University) Title: On the strength of ¥Delta^0_1-LEM over Intuitionistic Analysis 13:50--14:30 Koji Nakazawa (Kyoto University) Title: Confluence of lambda-calculi with permutative conversion 14:30--14:50 Break 14:50--15:30 Mahmudul Faisal Al Ameen (The Graduate University for Advanced Studies) Title: Completeness of Separation Logic with Recursive Procedures 15:30--16:10 Makoto Tatsuta (National Institute of Informatics) Title: Decidability of Separation Logic with Monadic Inductive Definitions 16:10--16:30 Break 16:30--17:30 Stefano Berardi (Torino University) Title: Realizability and Strong Normalization for Heyting Arithmetic with EM1 Abstracts: ---------------------------------------------------------------------- Daisuke Kimura (National Institute of Informatics) Title: A framework of models of functional PTSs Abstract: This talk presents a framework of models of functional PTSs. The class of functional PTSs is a class of PTS which contains well-known type theories such as the simply typed lambda calculus, System F, lambda P (dependent type system), and Calculus of Constructions. This framework of models is obtained by using Cousineau and Dowek's embedding from a functional PTS into a lambda P modulo. As a result of this talk, a semantical condition for a functional PTS to be a strongly normalizing system is given. This result is expected to give a semantical approach to Barendregt-Geuvers-Klop conjecture. ---------------------------------------------------------------------- Josh Ko (National Institute of Informatics) Title: Relational algebraic ornamentation Abstract: Type theory makes it possible to treat programs and proofs uniformly as the same entities. Dependently typed programmers aim to design programs that carry their own correctness proofs, exploiting the coincidence of programs and proofs to the full extent. A generic construction that can help to achieve this is relational algebraic ornamentation, with which we can synthesise datatypes satisfying properties that can be expressed in terms of folds. In this talk I will show how relational algebraic ornamentation can help with designing a dependently typed program for solving the well-known minimum coin change problem. ---------------------------------------------------------------------- Makoto Fujiwara (Tohoku University) Title: On the strength of ¥Delta^0_1-LEM over Intuitionistic Analysis Abstract: Ishihara [2] showed over intuitionistic analysis EL that Markov’s principle MP is equivalent to WMP+¥Pi^0_1-DML(under the name of MP^v). On the other hand, Akama et al. [1] showed that ¥Delta^0_1-LEM is implied from both of MP(under the name of ¥Sigma^0_1-DNE) and ¥Sigma^0_1-DML(under the name of ¥Sigma^0_1-LLPO). In this talk, we show over EL that ¥Delta^0_1-LEM is implied from ¥Pi^0_1-DML and equivalent to ¥Delta^0_1 comprehension axiom, which is from reverse mathematics. In addition, some separation results are also presented. This is a joint work with Hajime Ishihara and Takako Nemoto. References: [1] Y. Akama, S. Berardi, S. Hayashi and U. Kohlenbach, An arithmetical hierarchy of the law of excluded middle and related principles. Proc. of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), pp. 192--201, IEEE Press (2004). [2] H. Ishihara, Markov's principle, Church's thesis and Lindel¥"of theorem, Indag. Math. (N.S.) 4 (1993), pp. 321--325. ---------------------------------------------------------------------- Koji Nakazawa (Kyoto University) Title: Confluence of lambda-calculi with permutative conversion Abstract: We give a new proof of confluence for the lambda and the lambda-mu calculi with permutative conversion for case branching. For such calculi, naive approaches with parallel reductions do not work, and we adopt a proof technique with generalized notions of complete development with the Z property, introduced by Dehornoy and van Oostrom. Our idea also gives a simpler proof for confluence of the first-order classical natural deduction, which has been proved by Ando with more complicated notions. ---------------------------------------------------------------------- Mahmudul Faisal Al Ameen (The Graduate University for Advanced Studies) Title: Completeness of Separation Logic with Recursive Procedures Abstract: This talk proves the completeness of Hoare's Logic extended by separation logic for verification of while programs with pointers and recursive procedures. ---------------------------------------------------------------------- Makoto Tatsuta (National Institute of Informatics) Title: Decidability of Separation Logic with Monadic Inductive Definitions Abstract: This talk shows the decidability of entailments of symbolic heaps in separation logic with monadic inductive definitions under certain conditions. ---------------------------------------------------------------------- Stefano Berardi (Torino University) Title: Realizability and Strong Normalization for Heyting Arithmetic with EM1 Abstract: We present a new Curry-Howard correspondence for HA+EM1, first order constructive Heyting Arithmetic with the excluded middle on Sigma-0-1-formulas. We add to the lambda calculus an operator k_a which represents, from the viewpoint of programming, an exception operator with a delimited scope, and from the viewpoint of logic, a restricted version of the excluded middle. We motivate the restriction of the excluded middle by its use in proof mining; we introduce new techniques to prove strong normalization for HA + EM1 and the witness property for simply existential statements. One may consider our results as an application of the ideas of Interactive realizability, which we have adapted to the new setting and used to prove our main theorems. This technique has been recently extended by F. Aschieri to the entire excluded middle for First Order Arithmetic. This is a joint work with F. Aschieri and G. Birolo. ---------------------------------------------------------------------- 問合せ先　龍田 (tatsuta(a)nii.ac.jp)

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml