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

NIIレクチャーシリーズのお知らせ(Randy Goebel)
by Ken Satoh 11 Jan '13

11 Jan '13

NIIレクチャーシリーズのお知らせ国立情報学研究所(NII)では、海外の情報学に関係する著名研究者を招聘し、レクチャーシリーズを行っております。今回は、ＡＩの黎明期からＡＩの研究をされてきたカナダ・アルバータ大学のRandy Goebel先生の連続レクチャーのお知らせです。今回はＡＩ原理をビッグデータに応用する最先端の研究の講演を行っていただきます。講師:Prof. Randy Goebel (department of Computing Science at the University of Alberta, in Edmkonton, Alberta, Canada) 講義名：Do the emerging tools for managing big data fit with the founding principles of Artificial Intelligence? http://www.nii.ac.jp/en/event/list/0212 場所：国立情報学研究所 20階 2010室講義日：2013/2/12, 20, 26, 3/1 時間: 13:30-15:00 出席は無料で、どなたでも参加できます。参加のご検討よろしくお願いします。佐藤　健国立情報学研究所および総研大 ======= NII Lecture Series Title: Do the emerging tools for managing big data fit with the founding principles of Artificial Intelligence? ideas on the integration of the advice taker, structured inference, reasoning with incomplete information, and building multi-scale models from data. Speaker: Prof. Randy Goebel (department of Computing Science at the University of Alberta, in Edmkonton, Alberta, Canada) He is also vice president of the innovates Centre of Research Excellence (iCORE) at Alberta Innovates Technology Futures (AITF), chair of the Alberta Innovates Academy, and principle investigator in the Alberta Innovates Centre for Machine Learning. He received the B.Sc. (Computer Science), M.Sc. (Computing Science), and Ph.D. (Computer Science) from the Universities of Regina, Alberta, and British Columbia, respectively. At AITF, Randy is in charge of reshaping research investments (graduate student scholarships, research chairs, research centres). His research interests include applications of machine learning to systems biology, visualization, and web mining, as well as work on natural language processing, web semantics, and belief revision. Randy has experience working on industrial research projects in crew scheduling, pipeline scheduling, and steel mill scheduling, as well as scheduling and optimization projects for the energy industry in Alberta. Randy has held appointments at the University of Waterloo, University of Tokyo, Multimedia University (Malaysia), Hokkaido University (Sapporo), and has had research collaborations with DFKI (German Research Centre for Artificial Intelligence), NICTA (National ICT Australia), RWC (Real World Computing project, Japan), ICOT (Institute for New Generation Computing, Japan), NII (National Institute for Informatics, Tokyo), and is actively involved in academic and industrial collaborative research projects in Canada, Australia, Europe, and China. Abstract: The modern discipline of computer science has many facets, but what has clearly emerged in the last decade are three themes based on 1) rapidly accumulating volumes of data, 2) inter- and cross-disciplinary application of computer science to all scientific disciplines, and 3) a renewed interest in the semantics of complex information models, spanning a spectrum from semantic web, natural language, to multi-scale systems biology. This series of four lectures will attempt to knit together these three themes, by presenting the ideas that have emerged in their support: the rapid development and extension of machine learning theory and methods to help make sense of accumulating volumes of data, the application of computer science to nearly all scientific disciplines, especially those whose progress now necessarily relies on the management and interpretation of large data, and finally, the revival of a focus on semantics of information models based on data. Outline: Lecture 1: Connecting Advice Taking and Big Data Lecture 2: Structured inference and incomplete information Lecture 3: Natural Language Processing: Compressing Data to Models Lecture 4: Hypothesis Management with Symbols and Pictures Place: Lecture room 2010, 20th floor, National Institute of Informatics Date: 13:30pm-15:00pm, February 12, 20, 26, March 1, 2013 Lecture 1 Connecting Advice Taking and Big Data Tuesday, February 12, 2013, 13:30 - 15:00 A fundamental premise of Artificial Intelligence (AI) is the ability for a computer program to improve its behaviour by taking advice. Incremental accumulation of advice or knowledge has never been easier than today, when the rate of data capture is higher than ever before, and the management of big data and deployment of machine learning are coupled to help manage the transition from data to knowledge. This lecture uses simple technical concepts from nearly sixty years of AI, to identify some of the research challenges of managing big data, and exploiting knowledge emergent from big data. The goal is to find some important research priorities based on the motivation of the Advice Taker, and the current state of big data management and machine learning. Lecture 2 Structured inference and incomplete information Wednesday. February. 20, 13:30 - 15:00 If the foundation of Artificial Intelligence (AI) is the accumulation and use of knowledge, then a necessary stop is the structuring knowledge to be able to make inferences. The organization structures required to facilitate inference now span a broad spectrum of mathematical methods, including everything from simple propositional logic to sophisticated statistical and probabilistic inference. The two foundational components of computational inference are semantics of formal reasoning, and the development of reasoning methods to deal with incomplete information. This lecture reviews the foundational components of semantics and reasoning systems, including the development of goal-oriented reasoning based on abductive reasoning, the connection between logical and probabilistic systems, and especially how the architecture of reasoning systems can provide the basis for managing hypotheses in the face of incomplete information. Lecture 3 Natural Language Processing: Compressing Data to Models Tuesday. February. 26, 13:30 - 15:00 The problem of machine processing of natural language (NLP) has long been a research focus of artificial intelligence. This is partly because the use of natural language is easily conceived as a cognitive task requiring human-like intelligence. It is also because the rational structures for computer interpretation of language require the full suite of computational tools developed over the last hundred years (grammar, dictionaries, logic, parsing, inference, and context management). Most of the recent practical advances in NLP have arisen in the context of simple machine learning applied to large language corpora, to induce fragments of language models that provide the basis for interpretive and generative manipulation of language. These largely statistical models are arisen in what has been called the "pendulum swing" of NLP, in which statistical models have recently dominated those based on structural linguistics. In this lecture, we look at the concept of noisy corpora and their role in language models, including some interesting alternative sources of data for building language models. The applications range from complex language summary to the information extraction from medical, legal, and historical documents. Lecture 4 Hypothesis Management with Symbols and Pictures Friday. March. 1, 13:30 - 15:00 The current suite of Artificial Intelligence (AI) tools has provided a basis for sophisticated human-computer interfaces based on more than typing in language. In fact, one can develop multi-level representations that provide the basis for direct manipulation of visualizations. By constraining the repertoire of direct manipulations, one can enrich human computer interaction so that both humans and machines can understand and exploit visual interaction. This lecture shows how such direction manipulation requires a large repertoire of formal reasoning methods, and provides the sketch of formal framework and the problems arising in its development.

1 0

Cristian S. Calude氏、Elena Calude氏講演会のお知らせ（中央大学研究開発機構）
by Kohtaro Tadaki 11 Jan '13

11 Jan '13

＜重複してお受け取りの方はご容赦ください＞皆様：中央大学の只木と申します。中央大学研究開発機構では、来週19日土曜日、ニュージーランド研究者Cristian S. Calude氏（オークランド大学）およびElena Calude氏（マッセイ大学）をお招きし、下記要領で講演会を開催します。皆様、奮ってご参加下さい。 ---------------------------------- 只木孝太郎 (Kohtaro Tadaki) 中央大学研究開発機構〒112-8551 東京都文京区春日1-13-27 E-mail: tadaki(a)kc.chuo-u.ac.jp WWW: http://www2.odn.ne.jp/tadaki/ ---------------------------------------------------------- Cristian S. Calude氏、Elena Calude氏講演会 ◆日時： 2013年1月19日（土）15時00分〜 17時30分 ◆場所：中央大学後楽園キャンパス 5号館1階 5138号室（下記参照） ◆参加申込：不要 ---------------------------------------------------------- [ 講演内容 ] ◆15時00分〜16時00分講演題目：The complexity of mathematical problems 講演者：Cristian S. Calude (University of Auckland, NZ) and Elena Calude (Massey University, NZ) 講演要旨： Evaluating (or even guessing) the degree of complexity of an open problem, conjecture or mathematically proven statement is not an easy task not only for beginners, but also for the most experienced mathematicians. Is there a (uniform) method to evaluate, in some objective way, the difficulty of a mathematical statement or problem? The question is not trivial because mathematical problems can be so diverse. But, is there any indication that all, or most, or even a large part of mathematical problems have a kind of "commonality" allowing a uniform evaluation of their complexity? How could one compare a problem in number theory with a problem in complex analysis, a problem in algebraic topology or a theorem in dynamical systems? Surprisingly enough, such "commonalities" do exist for many mathematical problems. One of them is based on the possibility of expressing the problem in terms of (very) simple programs reducible to a (natural) question in theoretical computer science, the so-called "halting problem". A more general "commonality" can be discovered using the inductive type of computation, a computation more general the Turing computability. As a consequence, uniform approaches for evaluating the complexity of a large class of mathematical problems/conjectures/statements can be, and have been, developed. This talks reviews current progress and some open problems. ◆16時30分〜17時30分講演題目： The Kochen-Specker theorem and quantum randomness 講演者： Cristian S. Calude (University of Auckland, NZ) 講演要旨： The Kochen-Specker theorem shows the impossibility for a hidden variable theory to consistently assign values to certain (finite) sets of observables in a way that is noncontextual and consistent with quantum mechanics. If we require noncontextuality, the consequence is that many observables must not have pre-existing definite values. However, the Kochen-Specker theorem does not allow one to determine which observables must be value indefinite. In this talk we present an improvement on the Kochen-Specker theorem which allows one to actually locate observables which are provably value indefinite. Various technical and subtle aspects relating to this formal proof and its connection to quantum mechanics are discussed. This result is then utilized for the proposal and certification of a dichotomic quantum random number generator operating in a three-dimensional Hilbert space. ------------------------------------------------------------ 会場への道順： [中央大学後楽園キャンパスへのアクセスガイド] http://www.chuo-u.ac.jp/chuo-u/access/index_j.html http://www.chuo-u.ac.jp/chuo-u/access/access_korakuen_j.html [中央大学後楽園キャンパスマップ] http://www.chuo-u.ac.jp/chuo-u/campusmap/korakuen_j.html ------------------------------------------------------------

1 0

HAS 2013: Deadline Extended
by Ichiro Hasuo 07 Jan '13

07 Jan '13

みなさま，東京大学の蓮尾です．あけましておめでとうございます．以前お知らせした ETAPS 併設ワークショップの HAS，締切が 1/21 に延長になりました．Post-proceeding ですので，論文の preliminary version でも大歓迎，とのことです．ご投稿を検討いただければ幸いです．どうかよろしくお願いいたします．それでは！蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ =========================== [Apologies for multiple copies] [Please note: submission deadline extended to January, 12] ************************************************************************************************************ ********* CALL FOR PAPERS Third Workshop on Hybrid Autonomous Systems (HAS 2013) A satellite event of European Joint Conferences on Theory and Practice of Software, ETAPS 2013 March 17, 2013, Rome, Italy http://www2.warwick.ac.uk/fac/sci/maths/people/staff/bujorianu/has2013/ ************************************************************************************************************ ********* SCOPE: The interest on autonomous systems is increasing both in industry and academia. Such systems must operate with limited human intervention in a changing environment and must be able to compensate for significant system failures without external intervention. The hybrid discrete-continuous models constitute appropriate models of autonomous systems . Hybrid systems have behaviours characterised by the interaction between continuous and discrete dynamics and research in the area is driven by several school of thoughts. One approach is mainly focussed on applications to automation systems and the models and methods are centred on the concept of hybrid automaton (deterministic or probabilistic). A distinct school of thought interprets hybrid systems as control systems with regime change. Such systems are highly adaptive and suitable for modelling autonomic behaviours. The most prominent models of this approach are the stochastic hybrid systems and the mixed logical and dynamical systems. There is a clear research opportunity to combine these approaches for developing models, methods, techniques, methodologies, tools and environments for autonomous systems engineering. This workshop brings together researchers interested in all aspects of autonomy and resilience of hybrid systems. TOPICS: Topics include (but are not limited to): Ø new modelling paradigms for autonomous systems; Ø verification and safety certification techniques; Ø modelling, analysis and control of hybrid systems; Ø uncertainty and stochastic modelling; Ø multi-agent systems; Ø algebraic and categorical methods; Ø interaction between hybrid modelling and complexity science; Ø reports on case studies and practical experiments; Ø autonomous systems in natural science (e.g. from biology, ecology, climate). INVITED SPEAKERS: * Maria Domenica di Benedetto, L'Aquila University, IT * Radu Grosu, Vienna University of Technology, AU * Rafael Wisniewski, Aalborg University, DEN SUBMISSIONS: In order to encourage participation and discussion, this workshop solicits the submission of regular papers, which must contain original work, and must not have been previously published, nor be under consideration for publication elsewhere. The accepted submissions should clearly indicate the membership to one of the following categories: - technical contributions; - tutorials on a topic of importance; - surveys on large extent cross-disciplinary research (e.g., project outcomes);wor - reports on early stage or ongoing work. For each category of submission the novelty of the submission has to be clearly stated and the page limit should vary between 6 and 15 pages. All submissions must be in PDF format and use the EPTCS latex style, see http://style.eptcs.org/. Submissions can be made on the following website: https://www.easychair.org/conferences/login_as_yes.cgi?a=3413468 The workshop PC will review all regular paper submissions to select appropriate ones, ones for acceptance in each category, based on their relevance, merit, originality, and technical content. The authors of accepted submissions are expected to present and discuss their work at the workshop. Accepted regular papers will be published in the Electronic Proceedings in Theoretical Computer Science (EPTCS). A special issue in a journal is under consideration. IMPORTANT DATES: Submission (regular paper): *extended* January 12, 2013 Notification: January 24, 2013 Final version (ETAPS proceedings): February 14, 2013 Workshop: March 17, 2013 Final version (EPTCS post proceedings): TBA ORGANIZATION: PC Chairs: * Luca Bortolussi, University of Trieste, IT * Manuela Bujorianu, University of Warwick, UK * Giordano Pola, University of L’Aquila, IT Program Committee: * Ezio Bartocci, TU Wien, AU * Maria Domenica di Benedetto, L'Aquila University, IT * Luca Bortolussi, University of Trieste, IT (co-Chair) * Manuela Bujorianu, University of Warwick, UK (co-Chair) * Alberto Casagrande, Univeristy of Trieste, IT * Thao Dang, Verimag, FR * Louise Dennis, University of Liverpool, UK * Clare Dixon, University of Liverpool, UK * Alexandre Donzé, UC Berkeley, US * Martin Fränzle, Carl von Ossietzky Universität, DE * Ichiro Hasuo, University of Tokio, JP * Agung Julius, Rensselaer Polytechnic Institute, US * Toshimitsu Ushio, Osaka University, JP * Giordano Pola, L'Aquila University, IT (co-Chair) * Rom Langerak, University of Twente, NL * David Parker, University of Birmingham, UK * Guido Sanguinetti, University of Edinburgh, UK * Olaf Stursberg, University of Kassel, DE

1 0

CALCO 2013: Second Call for Papers
by Ichiro Hasuo 04 Jan '13

04 Jan '13

みなさま，こんにちは！東京大学の蓮尾です．国際会議 CALCO 2013 の案内を（再度）お送りします．トピックは代数・余代数・形式検証の理論一般，開催地はポーランド・ワルシャワ，締切は2月末です．どうか投稿をご検討ください．それでは！蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/ [Apologies for multiple copies] ========================================================================= SECOND CALL FOR PAPERS: CALCO 2013 5th International Conference on Algebra and Coalgebra in Computer Science September 3 - 6, 2013 Warsaw, Poland http://coalg.org/calco13/ ========================================================================= Abstract submission: February 22, 2013 Paper submission: March 1, 2013 Author notification: May 6, 2013 Final version due: June 3, 2013 ========================================================================= -- 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) and Winchester (UK, 2011). The fifth edition will be held in Warsaw, the capital of Poland. -- INVITED SPEAKERS -- Andrej Bauer - University of Lubljana, Sl Miko??aj Boja??czyk - Warsaw University, PL Neil Ghani - University of Strathclyde, UK Damien Pous - CNRS, ENS-Lyon, F -- 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 - Adhesive categories * 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 -- NEW TOPICS -- This edition of CALCO will feature two new topics, and submission of papers on these topics is especially encouraged. * 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 -- 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. As with previous editions, the proceedings will be published in the Springer LNCS series. Final papers should be no more than 15 pages long in the format specified by Springer (see http://www.springer.de/comp/lncs/authors.html). 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=calco2013 -- BEST PAPER AND BEST PRESENTATION AWARDS -- For the first time, this edition of CALCO will feature two kinds of 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: February 22, 2013 Paper submission: March 1, 2013 Author notification: May 6, 2013 Final version due: June 3, 2013 -- PROGRAMME COMMITTEE -- Luca Aceto - Reykjavik University, Iceland Ji???? Ad??mek - TU Braunschweig, D Lars Birkedal - IT University of Copenhagen, DK Filippo Bonchi - CNRS, ENS-Lyon, F Corina Cirstea - University of Southhampton, UK Bob Coecke - University of Oxford, UK Andrea Corradini - University of Pisa, I Mai Gehrke - Universit?? Paris Diderot - Paris 7, F H. Peter Gumm - Philipps University Marburg, D Gopal Gupta - University of Texas at Dallas, USA Ichiro Hasuo - Tokyo University, Japan Reiko Heckel - University of Leicester, UK (cochair) Bart Jacobs - Radboud University Nijmegen, NL Ekaterina Komendantskaya - University of Dundee, Scotland, UK Barbara K??nig - University of Duisburg-Essen, D Jos?? Meseguer - University of Illinois, Urbana-Champaign, USA Marino Miculan - University of Udine, I Stefan Milius - Friedrich-Alexander Universit??t Erlangen-N??rnberg, D (cochair) Larry Moss - Indiana University, Bloomington, USA Till Mossakowski - DFKI Lab Bremen and University of Bremen, D Prakash Panangaden - McGill University, Montreal, Canada Dirk Pattinson - Imperial College London, UK Dusko Pavlovic - Royal Holloway, University of London, UK Daniela Petrisan - University of Leicester, UK John Power - University of Bath, UK Jan Rutten - CWI Amsterdam and Radboud University Nijmegen, NL Lutz Schr??der - Friedrich-Alexander Universit??t Erlangen-N??rnberg, D Monika Seisenberger - Swansea University, UK Sam Staton - University of Cambridge, UK Alexandra Silva - Radboud University Nijmegen and CWI Amsterdam, NL Pawel Sobocinski - University of Southampton, UK Yde Venema - University of Amsterdam, NL Uwe Wolter - University of Bergen, NO -- ORGANISING COMMITTEE -- Bartek Klin (University of Warsaw, Poland) Andrzej Tarlecki (University of Warsaw, Poland) -- LOCATION -- Warsaw, the capital of Poland, is a lively city with many historic monuments and sights, but also with a thriving business district. It is easily accessible via two airports: the main Chopin Airport, used by most international carriers, and the recently open Warsaw Modlin Airport (30 minutes away by rail), used by budget airlines. -- SATELLITE WORKSHOPS -- CALCO 2013 will be preceded by the CALCO Early Ideas Workshop, chaired by Monika Seisenberger (Swansea University). The workshop is dedicated to presentation 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 - it is anticipated that many CALCO conference participants will want to attend the CALCO Early Ideas workshop (and vice versa). A workshop dedicated to tools based on algebraic and/or coalgebraic principles, CALCO Tools, will be held alongside the main conference, chaired by Lutz Schr??der (Friedrich Alexander Universit??t Erlangen-N??rnberg). Papers of this workshop will be included in the CALCO proceedings. -- 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 2013 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 available at the workshop. Submissions will be handled via EasyChair https://www.easychair.org/conferences/?conf=calcoearlyideas2013 The use of LNCS style is strongly encouraged. After the workshop, authors will have the opportunity to submit a full 10-15 page paper on the same topic. The reviewing will be carried out by the CALCO Early Ideas PC, with the support of the CALCO PC. The volume of selected papers will be available online. Authors will retain copyright, and are also encouraged to disseminate the results by subsequent publication elsewhere. http://coalg.org/calco13/workshops.html#ei -- CALCO Early Ideas Dates -- 2-page short contribution submission: May 27, 2013 Notification for short contribution: June 24, 2013 Final short contribution due: July 15, 2013 CALCO Early Idead Workshop: September 2, 2013 10-15 page paper submission: October 15, 2013 Notification for paper: December 15, 2013 Final paper version due: January 15, 2014 -- CALCO Early Ideas Program Committee -- Bartek Klin, University of Warsaw, Poland John Power, University of Bath, UK Monika Seisenberger, Swansea University, UK (chair) -- CALCO-Tools Overview -- CALCO-Tools will take place on the same dates as the main CALCO conference, with no overlap between the technical programmes of the two events. Topics of interest include systems, prototypes, and tools developed specifically for the design, checking, execution, and verification of (co)algebraic specifications, but also tools targeting different application domains while making core or interesting use of (co)algebraic techniques. Tool submissions should not exceed 5 pages in LNCS format. The accepted tool papers will be included in the final proceedings of the conference. The tools should be made available on the web at the time of submission. Each submission will be evaluated by at least three reviewers; one or more of the reviewers will be asked to download and use the tool. At least one of the authors of each tool paper must attend the conference to demo the tool. http://coalg.org/calco13/workshops.html#tools -- CALCO-Tools Dates -- Paper submission: April 8, 2013 Author notification: May 6, 2013 Final version due: June 3, 2013 -- CALCO-Tools Programme Committee -- Einar Broch Johnsen, University of Oslo, Norway Mark Hills, CWI Amsterdam, The Netherlands Barbara K??nig, University of Duisburg-Essen, Germany Dorel Lucanu, Alexandru Ioan Cuza University, Romania Dominik Luecke, CWI Amsterdam, The Netherlands Till Mossakowski, DFKI, Germany Lutz Schr??der, Friedrich-Alexander Universit??t Erlangen-N??rnberg, Germany (chair) Alexandra Silva, Radboud University Nijmegen and CWI Amsterdam, The Netherlands -- FURTHER INFORMATION -- Queries related to submission, reviewing, and programme should be sent to the relevant conference or workshop chairs. Queries related to the organisation should be emailed to calco2013(a)mimuw.edu.pl . [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

ESSS 2013 -- submission deadline extended
by 山形賴之 26 Dec '12

26 Dec '12

ESSS 2013の論文投稿締め切りが延長されました。皆様の投稿をお待ちしております。 ================================================== 2nd International Workshop on Engineering Safety and Security Systems March 18, 2013, Luxembourg Co-located with ICST 2013 in Luxembourg, March 18-22, 2013 More information: http://www.comp.nus.edu.sg/~pat/esss2013/ =================================================== Important dates ----------------- * January 6th 2013: Submission deadline (extended) * February 11th 2013: Notification of acceptance/rejection (extended) * March 18th 2013: Workshop Introduction of the Workshop ----------------- The International Workshop on Engineering Safety and Security Systems (ESSS) aims at contributing to the challenge of constructing reliable and secure systems. The workshop covers areas such as formal specification, (extended) type checking, model checking, program analysis/transformation, model-based testing and model-driven software construction. The workshop will bring together researchers and industry R&D expertise together to exchange their knowledge, discuss their research findings, and explore potential collaborations. Theme of the Workshop ----------------- The main theme of the workshop is methods and techniques for constructing large reliable and secure systems. The goal of the workshop is to establish a platform for the exchange of ideas, discussion, cross-fertilization, inspiration, co-operation, and dissemination. The topics of the workshop include, but are not limited to: -- methods, techniques and tools for system safety and security -- methods, techniques and tools for analysis, certification, and debugging of complex safety and security systems -- model-based and verification-based testing -- emerging application domains such as cloud computing and cyber-physical systems -- case studies and experience reports on the use of formal methods for analyzing safety and security systems Submissions guidelines ----------------- Paper submissions must be original, unpublished work. Submissions should be in made via the Easychair site: https://www.easychair.org/conferences/?conf=esss2013. Submitted manuscripts should be in English and formatted in the style of the IEEE Computer Society Proceedings Format (see http://www.ieee.org/conferences_events/conferences/publishing/templates.html ). Papers should not exceed 6 pages for full papers and 2 pages for short papers, including figures, references, and appendices. All submissions should be in PDF format. Submissions not adhering to the specified format and length may be rejected immediately, without review. All workshop papers will be published in the IEEE Digital Library in the form of a post-proceedings. A pre-workshop version of the papers will be available on the workshop website prior. Publication of accepted articles requires the commitment of one of the authors to register for the workshop and present the paper. General chair ----------------- Sjouke Mauw, University of Luxembourg, Luxembourg Program chairs ----------------- Yang Liu, Nanyang Technological University, Singapore Jun Pang, University of Luxembourg, Luxembourg Program committee ----------------- Etienne Andre, Universite Paris 13, France Cyrille Artho, AIST, Japan Marieke Huisma, University of Twente, The Netherlands Weiqiang Kong, Kyushu University, Japan Keqin Li, SAP Research, France Yang Liu, Nanyang Technological University, Singapore Zhiming Liu, UNU/IIST Macao, China Sjouke Mauw, University of Luxembourg, Luxembourg Jun Pang, University of Luxembourg, Luxembourg Geguang Pu, East China Normal University, China Mohammad Torabi Dashti, ETH Zurich, Switzerland Anton Wijs, Eindhoven University of Technology Yoriyuki Yamagata, AIST, Japan -- 山形頼之独立行政法人産業技術総合研究所研究員 E-mail: yoriyuki.yamagata(a)aist.go.jp http://staff.aist.go.jp/yoriyuki.yamagata/

1 0

QIT28のご案内
by NISHIMURA Harumichi 26 Dec '12

26 Dec '12

logic-mlの皆様，来年５月に開催される第２８回量子情報技術研究会（QIT28）のご案内をQIT28世話人に代わって投稿させていただきます．よろしくお願いいたします．名古屋大学大学院情報科学研究科西村治道 http://www.math.cm.is.nagoya-u.ac.jp/~hnishimura/ --- 第28回量子情報技術研究会研究会の内容情報科学と量子力学を融合させた新しい分野、量子情報科学に関する研究会です。情報を担う物理系の量子力学的側面を積極的に活かした新しい情報処理原理の研究とそこから開かれる新しい学問体系の構築および新しい情報技術パラダイムの創生を目指して、情報科学、物理学、光エレクトロニクスを含む理学、工学、数理科学に携わる研究者間に自由な討論の場を提供し、この研究分野の発展を図ることを目的としています。期日 2013年5月27日（月）, 28日（火）会場北海道大学創成科学研究棟大会議室（〒001-0021 札幌市北区北21条西10丁目）発表募集内容発表募集分野（申込状況によっては査読可能性あり）：量子情報、量子計算、量子暗号など広く量子情報技術に関わる理論的研究、実験的研究、計算機科学的研究、数学的研究、およびその他関連分野定員 150名参加費事前振込み一般6,000円, 学生1,000円． (当日会場払いは一般7,000円, 学生2,000円) (懇親会は別途）研究会参加申込要領参加申込は下記Webにて受付けます． http://staff.aist.go.jp/s-kawabata/qit/ 講演（口頭，ポスター）申込，予稿集原稿PDF提出は電子情報通信学会のWebシステムを使用する予定．【講演申込締切】 2013年4月12日（金）；口頭講演 2013年4月26日（金）；ポスター講演【予稿集原稿提出】 2013年4月26日（金）【参加申込締切】 2013年5月2日（木）【問合先】富田章久（北海道大学大学院情報科学研究科）竹内繁樹（北海道大学電子科学研究所/大阪大学産業科学研究所）長谷川俊夫（三菱電機株式会社情報技術総合研究所） E-mail: qit28(a)ml.hokudai.ac.jp 主催量子情報技術時限研究専門委員会 (委員長枝松圭一(東北大)) 共催応用物理学会量子エレクトロニクス研究会物質・デバイス領域共同研究拠点北海道大学電子科学研究所

1 0

SAT 2013 Call For Papers
by Naoyuki Tamura 25 Dec '12

25 Dec '12

# 重複の場合はご容赦ください．神戸大学の田村と申します．メーリングリストをお借りして，来年7月にヘルシンキで開催されます SAT 2013 の Call For Papers をお送りします． -- 田村直之 (tamura(a)kobe-u.ac.jp) 神戸大学情報基盤センター〒657-8501 神戸市灘区六甲台町1-1 Phone: 078-803-5364, Fax: 078-803-5375 http://bach.istc.kobe-u.ac.jp/tamura-jp.html COPRIS+SCALA+CSP=SOLVER ------------------------------------------------------------------------- 1st CALL FOR PAPERS Sixteenth International Conference on THEORY AND APPLICATIONS OF SATISFIABILITY TESTING --- SAT 2013 --- Helsinki, Finland, July 8-12, 2013 http://sat2013.cs.helsinki.fi/ Abstract submission deadline: February 1, 2013 Paper submission deadline: February 8, 2013 ------------------------------------------------------------------------- The International Conference on Theory and Applications of Satisfiability Testing (SAT) is the primary annual meeting for researchers studying the theory and applications of the propositional satisfiability problem, broadly construed. Besides plain propositional satisfiability, it includes Boolean optimization (including MaxSAT and Pseudo-Boolean (PB) constraints), Quantified Boolean Formulas (QBF), Satisfiability Modulo Theories (SMT), and Constraint Programming (CP) for problems with clear connections to Boolean-level reasoning. Many hard combinatorial problems can be encoded as SAT instances, in the broad sense mentioned above, including problems in formal verification (hardware and software), artificial intelligence, and operations research. More recently, biology, cryptology, data mining, machine learning, and mathematics have been added to the growing list. The SAT conference aims to further advance the field by soliciting original theoretical and practical contributions in these areas with a clear connection to satisfiability. SAT 2013 takes place in Helsinki, the capital of Finland. Helsinki is a vibrant Scandinavian and international city with a lot to offer to visitors. SAT 2013 takes place during the main summer season, allowing one to experience the whitenights during which the sun almost never sets. IMPORTANT DATES =============== (Follow http://sat2013.cs.helsinki.fi/ for updates.) February 1, 2013: Abstract Submission February 8, 2013: Paper Submission March 18, 2013 (approx.): Response from Authors begins, lasts 72 hours April 3, 2013: Acceptance Notifications April 22, 2013: Final Camera-Ready Versions July 8, 2013: Workshops begin July 9-12, 2013: Main Conference SCOPE ===== SAT 2013 welcomes scientific contributions addressing different aspects of the satisfiability problem. interpreted in a broad sense. Domains include MaxSAT and Pseudo-Boolean (PB) constraints, Quantified Boolean Formulae (QBF), Satisfiability Modulo Theories (SMT), Constraint Satisfaction Problems (CSP). Topics include (but are not restricted to) Theoretical advances (including exact algorithms, proof complexity, and other complexity issues); Practical search algorithms; Knowledge compilation; Implementation-level details of SAT solving tools and SAT-based systems; Problem encodings and reformulations; Applications (including both novel applications domains and improvements to existing approaches); Case studies and reports on insightful findings based on rigorous experimentation. OUT OF SCOPE ============ Papers claiming to resolve a major long-standing open theoretical question in mathematics or computer science (such as those for which a Millennium Prize is offered, see http://www.claymath.org/millennium) are outside the scope of the conference because there is insufficient time in the schedule to referee such papers; instead, such papers should be submitted to an appropriate technical journal. SUBMISSIONS =========== Submissions to SAT 2013 are solicited in three paper categories, describing original contributions: REGULAR PAPERS (9 to 15 pages, excluding references) Regular papers should contain original research, with sufficient detail to assess the merits and relevance of the contribution. For papers reporting experimental results, authors are strongly encouraged to make their data and implementations available with their submission. Submissions reporting on case studies are also encouraged, and should describe details, weaknesses, and strengths in sufficient depth. SHORT PAPERS (up to 8 pages, excluding references) The same evaluation criteria apply to short papers as to regular papers. They will be reviewed to the same standards of quality as regular papers, but will naturally contain less quantity of new material. Short papers will have the same status as regular papers and be eligible for the same awards (to be announced later). TOOL PAPERS (up to 6 pages, excluding references) A tool paper should describe the implemented tool and its novel features. Here "tools" are interpreted in a broad sense, including descriptions of implementations of core SAT solving techniques (solvers, preprocessors, etc.), systems exploiting SAT solvers or their extensions for solving interesting problem domains, etc. A demonstration is expected to accompany a tool presentation. Papers describing tools that have already been presented previously are expected to contain significant and clear enhancements to the tool. The software for the tool should be made publicly available, for accepted tool papers, and should at least be available to reviewers for evaluation during the review period. Evaluation criteria will include (but not be limited to) accurate documentation, usability, and potential for furthering the state of the art. For the latter criterion, availability of source code will be a significant factor. This is an evolving category, and technical issues involving software availability should be discussed with the program chairs. Be sure to check the conference web page for updates on this category. Papers describing unpublished tool-related work, providing details on a system and the novel algorithms it implements, as well as an experimental evaluation of the system's performance, can also be submitted as regular papers. For all paper categories, the page limits stated above do not include references, but do include all other material intended to appear in the conference proceedings. An additional technical appendix may be included, but it must be clearly labeled as supplementary material and may or may not be examined during review based of the considerations of individual reviewers. The appendix may contain detailed proofs, examples, descriptions of publicly available software related to the submission, or other information that does not fit the page limit. However, the appendix will not be included in the conference proceedings. The main contributions should be made accessible within the page limits, without having to rely on the appendix. Submissions should not be under review elsewhere nor be submitted elsewhere while under review for SAT 2013, and should not consist of previously published material. Submissions must use the Springer LNCS style without modifications, and must be written in English. All papers submissions are done exclusively via the SAT 2013 EasyChair Conference Service at http://www.easychair.org/conferences/?conf=sat2013 . PROCEEDINGS =========== All accepted papers will be published in the proceedings of the conference, which will be published within the Springer LNCS series. PROGRAM CHAIRS ============== Matti Jarvisalo University of Helsinki, Finland Allen Van Gelder University of California at Santa Cruz, USA PROGRAM COMMITTEE ================= Gilles Audemard Fahiem Bacchus Armin Biere Maria Luisa Bonet Lucas Bordeaux Uwe Bubeck Samuel Buss Nadia Creignou Leonardo de Moura John Franco Enrico Giunchiglia Ziyad Hanna Marijn Heule Holger H. Hoos Jinbo Huang Tommi Junttila Matti Jarvisalo Arist Kojevnikov Daniel Kroening Oliver Kullmann Daniel Le Berre Florian Lonsing Ines Lynce Joao Marques-Silva Alexander Nadel Jakob Nordstrom Albert Oliveras Ramamohan Paturi Jussi Rintanen Olivier Roussel Ashish Sabharwal Lakhdar Sais Roberto Sebastiani Bart Selman Peter Stuckey Stefan Szeider Naoyuki Tamura Allen Van Gelder Toby Walsh ================================================================

1 0

[CFP] ATVA 2013 (Hanoi, 10/15-18, 2013)
by Ogawa Mizuhito 23 Dec '12

23 Dec '12

$B3'MM(B $B!v!vJ#?t<u$1<h$i$l$?J}$O$4MF<O$/$@$5$$!#!v!v(B $B>.@n!w(BJAIST $B$G$9!#(B2013$BG/(B10$B7n$K%O%N%$$G9T$o$l$^$99q:]2q5D(BATVA$B$N(B 1st call for paper $B$r$*Aw$j$$$?$7$^$9!#O@J8Ej9FDy$a@Z$j$O(B4$B7n(B6$BF|(B $B$H$^$@@h$G$9$,!"(B10$B7n$N%O%N%$$OAV$d$+$J;~4|$G$9!#$U$k$C$FEj9F$r(B $B$47W2h$/$@$5$$!#(B $B>.@n?p;K(B (JAIST) http://www.jaist.ac.jp/~mizuhito --------------------------------------------------------------- CALL FOR PAPERS ATVA 2013 11th International Symposium on Automated Technology for Verification and Analysis October 15 - 18, 2013, Hanoi, Vietnam ==================== The ATVA series of symposia is intended to promote research in theoretical and practical aspects of automated analysis, verification and synthesis in Asia by providing a forum for interaction between the regional and international research communities and industry in the field. The previous editions of the symposium were held in Taiwan, Beijing, Tokyo, Seoul, Macao, Singapore, Taipei and Thiruvananthapuram. Organised by the University of Engineering and Technology VNU Hanoi, ATVA 2013 will be held in the campus of Vietnam National University, Hanoi from October 15th to October 18th, 2013. SCOPE ATVA 2013 solicits high quality submissions in areas related to the theory and practice of automated analysis and verification of hardware and software systems. Topics of interest include, but are not limited to: - Formalisms for modeling hardware, software and embedded systems - Specification and verification of finite-state, infinite-state and parameterized system - Program analysis and software verification - Analysis and verification of hardware circuits, systems-on-chip and embedded systems - Analysis of real-time, hybrid, priced/weighted and probabilistic systems - Deductive, algorithmic, compositional and abstraction/refinement techniques for analysis and verification - Analytical techniques for safety, security, and dependability - Testing and runtime analysis based on verification technology - Analysis and verification of parallel and concurrent hardware/software systems - Verification in industrial practice - Applications and case studies Theory papers should preferably be motivated by practical problems, and applications should be based on sound theory and should solve problems of practical interest. SUBMISSION Submissions are invited in two categories: regular research papers and tool papers. Submitted papers must present original and unpublished work, and must not be concurrently submitted to any other conference or journal. Regular paper submissions are restricted to 15 pages inSpringer's LNCS format, and tool paper submissions are restricted to 4 pages in the same format. Proofs and details omitted due to space constraints may be put in an appendix. Any such additional material will be read by reviewers/program committee members at their discretion. Authors are therefore urged to include details necessary for evaluation of the technical merit of their work within the prescribed page limits. Tool papers must include information about a URL from where the tool can be downloaded or accessed on-line for evaluation. The URL must also contain a set of examples, and a user's manual that describes usage of the tool through examples. In case the tool needs to be downloaded and installed, the URL must also contain a document clearly giving instructions for installation of the tool on Linux/Windows/MacOS. Authors must upload PDF files of their papers throughEasyChair at: https://www.easychair.org/conferences/?conf=atva2013 Accepted papers in both categories will be published by Springer as a LNCS volume. At least one author of each accepted paper must also register for the conference and present the paper. KEYNOTE TALKS AND TUTORIALS Keynote talks and tutorials will be given by: - Alessandro Cimatti (ITC-IRST, Italy) - Marta Kiwakowska (Oxford, UK) - Jerome Leroux (Bordeaux, France) IMPORTANT DATES - April 06, 2013: Paper submission deadline - Jun 1, 2013: Paper acceptance/rejection notification - July 5, 2013: Camera-ready copy deadline - October 15 - 18, 2013: Main conference & Tutorials ORGANIZING COMMITTEES General Chair - Nguyen Ngoc Binh (UET-VNU Hanoi, Vietnam) Steering Committee - E. Allen Emerson (U. of Texas-Austin, USA) - Teruo Higashino (Osaka Univeristy, Japan) - Insup Lee (U. of Pennsylvania, USA) - Doron A. Peled (Bar Ilan University, Israel) - Farn Wang (National Taiwan University, Taiwan) - Hsu-Chun Yen (National Taiwan University, Taiwan) Programme Committee Co-Chairs - Hung Dang-Van (UET-VNU Hanoi, Vietnam) - Mizuhito Ogawa (JAIST, Japan) Publicity Chair - Thao Dang (Verimag, France) Finance/Registration Chair - Thanh-Tho Quan (HCMUT, Vietnam) Local Chair - Hoang Truong (UET-VNU Hanoi, Vietnam) PROGRAMME COMMITTEE - Christel Baier (Germany) - Jonathan Billington (Australia) - Gianpiero Cabodi (Italy) - Supratik Chakraborty (India) - Wei-Ngan Chin (Singapore) - Thao Dang (France) - Hung Dang-Van (Vietnam, Co-chair) - Deepak D'Souza (India) - E.Allen Emerson (USA) - Martin Frnzle (Germany) - Masahiro Fujita (Japan) - Susanne Graf (France) - Teruo Higashino (Japan) - Alan Hu (Canada) - Franjo Ivancic (USA) - Jie-Hong Roland Jiang (Taiwan) - Joost-Pieter Katoen (Germany) - Zurab Khasidashvili (Israel) - Moonzoo Kim (Korea) - Gerwin Klein (Australia) - Fribourg Laurent (France) - Insup Lee (USA) - Xuandong Li (China) - Annabelle McIver (Australia) - Madhavan Mukund (India) - Pham Ngoc-Hung (Vietnam) - Thanh-Binh Nguyen (Vietnam) - Viet-Ha Nguyen (Vietnam) - Mizuhito Ogawa (Japan, Co-chair) - Thanh-Tho Quan (Vietnam) - Venkatesh R (India) - Ganesan Ramalingam (India) - Abhik Roychoudhury (Singapore) - Hiroyuki Seki (Japan) - Martin Steffen (Norway) - Sofiene Tahar (Canada) - Hoang Truong (Vietnam) - Mahesh Viswanathan (USA) - Farn Wang (Taiwan) - Bow-Yaw Wang (China) - Ji Wang (China) - Hsu-Chun Yen (Taiwan) - Wang Yi (Sweden) - Shoji Yuen (Japan) - Wenhui Zhang (China) CONFERENCE VENUE Historical Campus, Vietnam National University, 19 Le Thanh Tong street, Hoan Kiem district, Hanoi, Vietnam.

1 0

LICS 2013 Last Call for Papers
by Kazushige TERUI 20 Dec '12

20 Dec '12

LAST CALL FOR PAPERS Twenty-Eighth Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2013) June 25-28, 2013, New Orleans, USA http://lii.rwth-aachen.de/lics/lics13/ LICS 2013 will be hosted by Tulane University, in New Orleans, LA USA, from June 25th to 28th, 2013. LICS 2013 will be co-located with MFPS13 (23-25 June) and CSF13 (28-30 June). The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic, broadly construed. We invite submissions on topics that fit under that rubric. Suggested, but not exclusive, topics of interest include: automata theory, automated deduction, categorical models and logics, concurrency and distributed computation, constraint programming, constructive mathematics, database theory, decision procedures, description logics, domain theory, finite model theory, theory of automatic structures, formal aspects of program analysis, formal methods, foundations of computability, higher-order logic, lambda and combinatory calculi, linear logic, logic in artificial intelligence, logic programming, logical aspects of bioinformatics, logical aspects of computational complexity, logical aspects of quantum computation, logical frameworks, logics of programs, modal and temporal logics, model checking, probabilistic systems, process calculi, programming language semantics, proof theory, real-time systems, reasoning about security, rewriting, type systems and type theory, and verification. Important Dates: Authors are required to submit a paper title and a short abstract of about 100 words in advance of submitting the extended abstract of the paper. Titles & Short Abstracts Due : January 7, 2013 Extended Abstracts Due : January 14, 2013 Author Notification (approximate) : March 22, 2013 Final Versions Due for Proceedings: April 26, 2013 Deadlines are firm; late submissions will not be considered. All submissions will be electronic via http://easychair.org/conferences/?conf=lics2013. Submission Instructions: Every extended abstract must be submitted in the IEEE Proceedings 2-column 10pt format and may not be longer than 10 pages, including references. LaTeX style files will be available on the conference website. The extended abstract must be in English and provide sufficient detail to allow the program committee to assess the merits of the paper. It should begin with a succinct statement of the issues, a summary of the main results, and a brief explanation of their significance and relevance to the conference and to computer science, all phrased for the non-specialist. Technical development directed to the specialist should follow. References and comparisons with related work must be included. (If necessary, detailed proofs of technical results may be included in a clearly-labeled appendix, to be consulted at the discretion of program committee members.) Extended abstracts not conforming to the above requirements will be rejected without further consideration. Papers selection will be merit-based, with no a priori limit on the number of accepted papers. Results must be unpublished and not submitted for publication elsewhere, including the proceedings of other symposia or workshops. The program chair must be informed, in advance of submission, of any closely related work submitted or about to be submitted to a conference or journal. Authors of accepted papers are expected to sign copyright release forms. One author of each accepted paper is expected to present it at the conference. Short Presentations: A session of short presentations, intended for descriptions of student research, works in progress, and other brief communications, is planned. These abstracts will not be published. Dates and guidelines will be posted on the LICS website. Kleene Award for Best Student Paper: An award in honor of the late Stephen C. Kleene will be given for the best student paper(s), as judged by the program committee. Special Issues: Full versions of up to three accepted papers, to be selected by the program committee, will be invited for submission to the Journal of the ACM. Additional selected papers will be invited to a special issue of Logical Methods in Computer Science. Sponsorship: The symposium is sponsored by the IEEE Technical Committee on Mathematical Foundations of Computing and by ACM SIGACT, in cooperation with the Association for Symbolic Logic and the European Association for Theoretical Computer Science. Program Chair: Orna Kupferman, Hebrew University Program Committee: Parosh A. Abdulla, Uppsala University Amal Ahmed, Northeastern Universtiy Sergei Artemov, City University of New York Andrei Bulatov, Simon Fraser University Yijia Chen, Shanghai Jiao Tong University Veronique Cortier, CNRS, Loria Mariangiola Dezani-Ciancaglini, Univ. di Torino Thomas Ehrhard, CNRS, Universite Paris Diderot Javier Esparza, Technische Universitaet Muenchen Kousha Etessami, University of Edinburgh Maribel Fernandez, King’s College London Santiago Figueira, University of Buenos Aires Simon Gay, University of Glasgow Martin Grohe, Humboldt-Universitaet zu Berlin Martin Hofmann, LMU Munich Petr Jancar, Technical University Ostrava Barbara Jobstmann, CNRS, Verimag and Jasper DA Patricia Johann, University of Strathclyde Bakhadyr Khoussainov, The University of Auckland Antonina Kolokolova, University of Newfoundland Victor Marek, University of Kentucky Angelo Morzenti, Politecnico di Milano Lawrence Moss, Indiana University Madhavan Mukund, Chennai Math. Institute Anca Muscholl, Universite Bordeaux Mogens Nielsen, Aarhus University Catuscia Palamidessi, INRIA, Ecole Polytechnique Luc Segoufin, INRIA, ENS Cachan Natarajan Shankar, SRI International Alexandra Silva, Radboud University Nijmegen Balder ten Cate, UC Santa Cruz Kazushige Terui, Kyoto University Ron van der Meyden, Univ. of New South Wales Jeannette M. Wing, Carnegie Mellon University Nobuko Yoshida, Imperial College London Conference Chair: Mike Mislove, Tulane University Workshop Chair: Patricia Bouyer-Decitre, CNRS, ENS Cachan Publicity Chair: Andrzej Murawski, University of Leicester General Chair: Luke Ong, University of Oxford Organizing Committee: Martin Abadi, Luca Aceto, Rajeev Alur, Franz Baader, Paul Beame, Patricia Bouyer-Decitre, Adriana Compagnoni, Anuj Dawar, Nachum Dershowitz, Martin Escardo, Maribel Fernandez, Martin Grohe, Orna Grumberg, Jean-Pierre Jouannaud, Phokion Kolaitis, Orna Kupferman, Benoit Larose, Vlatko Lipovac, Michael Mislove, Georg Moser, Andrzej Murawski, Luke Ong (chair), Andre Scedrov, Philip Scott, David Shmoys, Matt Valeriote Advisory Board: Martin Abadi, Samson Abramsky, Rajeev Alur, Bob Constable, Thierry Coquand, Thomas Henzinger, Phokion Kolaitis, Dexter Kozen, Dale Miller, John Mitchell, Prakash Panangaden, Andrew Pitts, Gordon Plotkin, Moshe Vardi, Glynn Winskel ------------------------------------------ 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

First Announcement ― TACL 2013
by Hiroakira Ono 18 Dec '12

18 Dec '12

[Apologies for multiple copies] ====================================================== TOPOLOGY, ALGEBRA AND CATEGORIES IN LOGIC (TACL 2013) ====================================================== July 28 - August 1, 2013 Department of Mathematics, Vanderbilt University Nashville, Tennessee USA http://www.math.vanderbilt.edu/~tacl2013/ The Sixth International Conference on Topology, Algebra and Categories in conjunction with the 28th Annual Shanks Lecture Series Scope --------- Studying logics via semantics is a well-established and very active branch of mathematical logic, with many applications, in computer science and elsewhere. The area is characterized by results, tools and techniques stemming from various fields, including universal algebra, topology, category theory, order, and model theory. The program of the conference TACL 2013 will focus on three interconnecting mathematical themes central to the semantical study of logics and their applications: algebraic, categorical, and topological methods. This is the sixth conference in the series Topology, Algebra and Categories in Logic (TACL, formerly TANCL). Earlier installments of this conference have been organized in Tbilisi (2003), Barcelona (2005), Oxford (2007), Amsterdam (2009), Marseilles (2011). Confirmed invited speakers ------------------------------------- Vladimir Voevodsky, Institute for Advanced Studies, USA (Shanks Lecturer) Nick Bezhanishvili, Utrecht University, The Netherlands Leo Cabrer, University of Oxford, UK Silvio Ghilardi, University of Milan, Italy George Metcalfe, University of Bern, Switzerland Alex Simpson, University of Edinburgh, UK Featured topics --------------------- Contributed talks can deal with any topic dealing with the use of algebraic, categorical or topological methods in either logic or computer science. This includes, but is not limited to, the following areas: * Algebraic structures in CS * Algebraic logic * Coalgebra * Categorical methods in logic * Domain theory * Lattice theory * Lattices with operators * Many-valued and fuzzy logics * Modal logics * Non-classical logics * Ordered topological spaces * Ordered algebraic structures * Pointfree topology * Proofs and Types * Residuated structures * Semantics * Stone-type dualities * Substructural logics * Topological semantics of modal logic Submissions ----------------- Contributed presentations will be of two types: o 20 minutes long presentations in parallel sessions and o featured, 30 minutes long, plenary presentations. The submission of an abstract will be required to be selected for a contributed presentation of either kind. While preference will be given to new work, results that have already been published or presented elsewhere will also be considered. More information on the submission procedure, as well as a link to the EasyChair system, can be found at the conference web site. Important dates ---------------------- April 1, 2013: Abstract submission deadline May 1, 2013: Notification to authors July 28-August 1, 2013: Conference Program Committee --------------------------- Steve Awodey, Carnegie Mellon University Guram Bezhanishvili, New Mexico State University David Gabelaia, Razmadze Mathematical Institute, Tbilisi Nick Galatos (co-chair), University of Denver Mai Gehrke, LIAFA, University of Paris Diderot Rob Goldblatt, Victoria University, Wellington John Harding, New Mexico State University Ramon Jansana, University of Barcelona Peter Jipsen, Chapman University Achim Jung, University of Birmingham Alexander Kurz (co-chair), University of Leicester Vincenzo Marra, University of Milan Hiroakira Ono, Japan Advanced Institute of Science and Technology Alessandra Palmigiano, University of Amsterdam Hilary Priestley, St Anne's College, Oxford James Raftery, University of KwaZulu-Natal, Durban Thomas Streicher, Technical University of Darmstadt Kazushige Terui, Kyoto University Constantine Tsinakis, Vanderbilt University Yde Venema, University of Amsterdam Michael Zakharyaschev, Birkbeck College, University of London Organizing Committee ------------------------------- Chris Conidis, Vanderbilt University Lianzhen Liu, Jiangnan University, China Warren McGovern, Florida Atlantic University Francesco Paoli, University of Cagliari Rebecca Steiner, Vanderbilt University Constantine Tsinakis (chair), Vanderbilt University William Young, Vanderbilt University Expression of interest ------------------------------ We would greatly appreciate your taking two minutes to express your level of interest in the conference by filling out a simple form on the conference web site under "Express Interest". This will help the Organizing Committee with their planning. You can also opt-out from receiving future announcements by clicking the link at the bottom of this email. More Information ----------------------- TACL 2013 web site: http://www.math.vanderbilt.edu/~tacl2013/ Use this site for local information, including hotel accommodations, for travel information and registration, and for submitting a request for financial support. Any queries for the Program Committee (such as usage of the EasyChair conference system, abstract submission guidelines, conference program, etc.) should be sent to tacl2013(a)gmail.com. Queries for the local Organizing Committee (registration, hotel accommodations, financial support and reimbursements, technology infrastructure, etc.) should be sent to tacl2013oc(a)vanderbilt.edu.

1 0

First Announcement — TACL 2013 TACL 2013
by Kent, Curt 18 Dec '12

18 Dec '12

[Apologies for multiple copies] ====================================================== TOPOLOGY, ALGEBRA AND CATEGORIES IN LOGIC (TACL 2013) ====================================================== July 28 - August 1, 2013 Department of Mathematics, Vanderbilt University Nashville, Tennessee USA http://www.math.vanderbilt.edu/~tacl2013/ The Sixth International Conference on Topology, Algebra and Categories in conjunction with the 28th Annual Shanks Lecture Series Scope --------- Studying logics via semantics is a well-established and very active branch of mathematical logic, with many applications, in computer science and elsewhere. The area is characterized by results, tools and techniques stemming from various fields, including universal algebra, topology, category theory, order, and model theory. The program of the conference TACL 2013 will focus on three interconnecting mathematical themes central to the semantical study of logics and their applications: algebraic, categorical, and topological methods. This is the sixth conference in the series Topology, Algebra and Categories in Logic (TACL, formerly TANCL). Earlier installments of this conference have been organized in Tbilisi (2003), Barcelona (2005), Oxford (2007), Amsterdam (2009), Marseilles (2011). Confirmed invited speakers ------------------------------------- Vladimir Voevodsky, Institute for Advanced Studies, USA (Shanks Lecturer) Nick Bezhanishvili, Utrecht University, The Netherlands Leo Cabrer, University of Oxford, UK Silvio Ghilardi, University of Milan, Italy George Metcalfe, University of Bern, Switzerland Alex Simpson, University of Edinburgh, UK Featured topics --------------------- Contributed talks can deal with any topic dealing with the use of algebraic, categorical or topological methods in either logic or computer science. This includes, but is not limited to, the following areas: * Algebraic structures in CS * Algebraic logic * Coalgebra * Categorical methods in logic * Domain theory * Lattice theory * Lattices with operators * Many-valued and fuzzy logics * Modal logics * Non-classical logics * Ordered topological spaces * Ordered algebraic structures * Pointfree topology * Proofs and Types * Residuated structures * Semantics * Stone-type dualities * Substructural logics * Topological semantics of modal logic Submissions ----------------- Contributed presentations will be of two types: o 20 minutes long presentations in parallel sessions and o featured, 30 minutes long, plenary presentations. The submission of an abstract will be required to be selected for a contributed presentation of either kind. While preference will be given to new work, results that have already been published or presented elsewhere will also be considered. More information on the submission procedure, as well as a link to the EasyChair system, can be found at the conference web site. Important dates ---------------------- April 1, 2013: Abstract submission deadline May 1, 2013: Notification to authors July 28-August 1, 2013: Conference Program Committee --------------------------- Steve Awodey, Carnegie Mellon University Guram Bezhanishvili, New Mexico State University David Gabelaia, Razmadze Mathematical Institute, Tbilisi Nick Galatos (co-chair), University of Denver Mai Gehrke, LIAFA, University of Paris Diderot Rob Goldblatt, Victoria University, Wellington John Harding, New Mexico State University Ramon Jansana, University of Barcelona Peter Jipsen, Chapman University Achim Jung, University of Birmingham Alexander Kurz (co-chair), University of Leicester Vincenzo Marra, University of Milan Hiroakira Ono, Japan Advanced Institute of Science and Technology Alessandra Palmigiano, University of Amsterdam Hilary Priestley, St Anne's College, Oxford James Raftery, University of KwaZulu-Natal, Durban Thomas Streicher, Technical University of Darmstadt Kazushige Terui, Kyoto University Constantine Tsinakis, Vanderbilt University Yde Venema, University of Amsterdam Michael Zakharyaschev, Birkbeck College, University of London Organizing Committee ------------------------------- Chris Conidis, Vanderbilt University Lianzhen Liu, Jiangnan University, China Warren McGovern, Florida Atlantic University Francesco Paoli, University of Cagliari Rebecca Steiner, Vanderbilt University Constantine Tsinakis (chair), Vanderbilt University William Young, Vanderbilt University Expression of interest ------------------------------ We would greatly appreciate your taking two minutes to express your level of interest in the conference by filling out a simple form on the conference web site under "Express Interest". This will help the Organizing Committee with their planning. You can also opt-out from receiving future announcements by clicking the link at the bottom of this email. More Information ----------------------- TACL 2013 web site: http://www.math.vanderbilt.edu/~tacl2013/ Use this site for local information, including hotel accommodations, for travel information and registration, and for submitting a request for financial support. Any queries for the Program Committee (such as usage of the EasyChair conference system, abstract submission guidelines, conference program, etc.) should be sent to tacl2013(a)gmail.com<mailto:tacl2013@gmail.com>. Queries for the local Organizing Committee (registration, hotel accommodations, financial support and reimbursements, technology infrastructure, etc.) should be sent to tacl2013oc(a)vanderbilt.edu<mailto:tacl2013oc@vanderbilt.edu>. To unsubscribe from this list, please send an email to LISTSERV(a)LIST.VANDERBILT.EDU<mailto:LISTSERV@LIST.VANDERBILT.EDU> with "SIGNOFF TACL2013" as the body of message.

1 0

ESSLLI Student Seminar 2013 - First Call for Papers
by Mauricio Hernandes 17 Dec '12

17 Dec '12

mlの皆様, As asked by the Chair of the Student Seminar I am forwarding the information below. Regards Mauricio Hernandes First Call for Papers ESSLLI 2013 STUDENT SESSION Held during The 25th European Summer School in Logic, Language and Information Düsseldorf, Germany, August 5-16, 2013 Deadline for submissions: April 1st, 2013 https://www.easychair.org/conferences/?conf=essllistus2013 *ABOUT*: The Student Session of the 25th European Summer School in Logic, Language, and Information (ESSLLI) will take place in *Düsseldorf, Germany on August 5-16, 2013*. We invite submissions of original, unpublished work from students in any area at the intersection of Logic & Language, Language & Computation, or Logic & Computation. Submissions will be reviewed by several experts in the field, and accepted papers will be presented orally or as posters and will appear in the student session proceedings in Springer. This is an excellent opportunity to receive valuable feedback from expert readers and to present your work to a diverse audience. *A SEPARATE POSTER SESSION*: Note that this year there are two separate kinds of submissions, one for the oral presentations and one for the posters. This means that papers can be directly submitted as posters. Reviewing and ranking will be done separately. We particularly encourage submissions for posters. More detailed guidelines regarding submission can be found on the Student Session website: http://stus2013.loriweb.org/, (links to previous years' proceedings are also available there). Please direct inquiries about submission procedures or other matters relating to the Student Session to margotcolinet(a)gmail.com For general inquiries about ESSLLI 2013, please consult the main ESSLLI 2013 page, http://esslli2013.de/. Kind regards, *The ESSLLI 2013 Student Session Organization Committee*, Chair: Margot Colinet (Université Paris Diderot-Paris 7) LOCO (LOgic and Computation) co-chairs: Ronald de Haan (Technische Universität Wien) Michał Zawidzki (Uniwersytet Łódzki) LOLA (LOgic and LAnguage) co-chairs: Agata Renans (Universität Potsdam) Barbara Tomaszewicz (University of Southern California) LACO (LAnguage and Computation) co-chairs: Pierre Bourreau (Heinrich-Heine-Universität Düsseldorf) Julia Zinova (Heinrich-Heine-Universität Düsseldorf)

1 0

*** 場所と時間を変更しました *** Talk by Keiko Nakata (Tallinn U of Tech), Tue 18 December 2012
by Ichiro Hasuo 17 Dec '12

17 Dec '12

みなさま，念のため，明日の中田景子さんのご講演について場所と時間の変更のご案内を再度お送りします．どうかよろしくお願いいたします！蓮尾一郎 ---------- Forwarded message ---------- From: Ichiro Hasuo <ichiro(a)is.s.u-tokyo.ac.jp> Date: Thu, Dec 13, 2012 at 9:06 AM Subject: *** Time & Venue Changed *** Talk by Keiko Nakata (Tallinn U of Tech), Tue 18 December 2012 To: logic-ml <logic-ml(a)sato.kuis.kyoto-u.ac.jp>, sonoteno <sonoteno(a)m.aist.go.jp>, jssst-ppl(a)kb.ecei.tohoku.ac.jp みなさま，こんにちは！東京大学の蓮尾と申します．先日お知らせした，タリン工科大学の中田景子さんによるご講演ですが，＊＊時間と場所を変更＊＊させてください．（日程は同じです）急なお知らせで申し訳ありません．また，会場の国立情報学研究所では，中田さんのご講演の前（13:30-15:30）に ToPS セミナーが開催されます．そちらにも是非どうぞ！ http://takeichi.ipl-lab.org/~tops/upcoming_seminar.html 蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/ ============================================= Tue 18 December 2012, 16:00-17:30 Keiko Nakata (Tallinn University of Technology), 2 Talks 国立情報学研究所 12階 1208号室 Rm. 1208, 12F, National Institute of Informatics Access: http://www.nii.ac.jp/en/about/access *** 場所・時間が変わりました *** *** The time and venue have been changed *** 中田さんのご講演の前（13:30-15:30）に，同じ場所で ToPS セミナーが開催されます．そちらにも是非どうぞ！http://takeichi.ipl-lab.org/~tops/upcoming_seminar.h… Prior to Dr. Nakata’s talk there will be a “ToPS seminar” at the same location. The talks will be of similar research interests. http://takeichi.ipl-lab.org/~tops/upcoming_seminar.html Talk 1: Proving open induction using delimited control operators Open Induction (OI) is a principle classically equivalent to Dependent Choice, which is, unlike the later, closed under double-negation translation and A-translation. In the context of Constructive Reverse Mathematics, Wim Veldman has shown that, in presence of Markov's Principle, OI on Cantor space is equivalent to Double-negation Shift (DNS). With Danko Ilik, we have reworked Veldman's proof to give a constructive proof of OI, where DNS is interpreted using delimited control operators. Joint work with Danko Ilik. Talk 2: Walking through infinite trees with mixed induction and coinduction: A Proof Pearl with the Fan Theorem and Bar Induction. We study temporal properties over infinite binary red-blue trees in the setting of constructive type theory. We consider several familiar path-based properties, typical to linear-time and branching-time temporal logics like LTL and CTL*, and the corresponding tree-based properties, in the spirit of the modal mu-calculus. We conduct a systematic study of the relationships of the path-based and tree-based versions of ``eventually always blueness '' and mixed inductive-coinductive ``almost always blueness'' and arrive at a diagram relating these properties to each other in terms of implications that hold either unconditionally or under specific assumptions (Weak Continuity for Numbers, the Fan Theorem, Lesser Principle of Omniscience, Bar Induction). Joint work with Marc Bezem and Tarmo Uustalu.

1 0

Logic Zoo Workshop 2013 (Jan. 31, Tokyo)
by Yoichi Hirai 13 Dec '12

13 Dec '12

みなさま東京大学萩谷研の平井洋一より、Logic Zooワークショップのご案内です。 2013年1月31日(木)東京開催です(前日30日には平井洋一の博士論文公聴会)。講演・前日夕食の申込は 2013年1月15日(火) 締切です。詳細及び申込 http://logiczoo13.pira.jp 論理をみつける話から論理を調べる話、論理を使う話までご講演、ご参加をお待ちしております。平井洋一 Logic Zoo Workshop 2013 (Jan. 31, Tokyo) ======================================== A workshop on living, playing or working logics. Topics include: - substructural and more exotic logics - type systems - programming languages - mathematics on non-classical logics - software verification - logics for social, economical, legal or linguistic analysis. Organizer: Yoichi Hirai yh(a)lyon.is.s.u-tokyo.ac.jp Schedule and Location --------------------- - 2013 Jan. 31 (Thu), 10:00--17:00 - Room 236, through Science Bldg. 7, 理学部7号館2階より化東236室 Hongo campus, the Univ. of Tokyo 東京大学本郷キャンパス - with four blackboards 黒板4枚あり Registration ------------ Please register for your talk slot and/or dinner by Jan. 15, 2013. A talk will be 30-minute long (tentative estimation). Fill this form and send it to yh(a)lyon.is.s.u-tokyo.ac.jp ================================== Logic Zoo (Jan. 31) Registration name: affiliation: eve-dinner on 30th: yes / no / not decided giving a talk: yes / not decided title: TBD or a title ================================== Some Other Events ----------------- 2013-01-30 (Wed): Defense and Dinner 12:00--14:00 Yoichi Hirai's defense (first half is public): Hyper-Lambda Calculi Room 102, Science Bldg. 7, Hongo campus, the Univ. of Tokyo 19:00--21:00 Dinner: Logic Zoo Eve nearby restaurant 2013-01-31 (Thu): Workshop 10:00--17:00 Logic Zoo Workshop Room 236, through Science Bldg. 7, Hongo campus, the Univ. of Tokyo

1 0

*** Time & Venue Changed *** Talk by Keiko Nakata (Tallinn U of Tech), Tue 18 December 2012
by Ichiro Hasuo 13 Dec '12

13 Dec '12

みなさま，こんにちは！東京大学の蓮尾と申します．先日お知らせした，タリン工科大学の中田景子さんによるご講演ですが，＊＊時間と場所を変更＊＊させてください．（日程は同じです）急なお知らせで申し訳ありません．また，会場の国立情報学研究所では，中田さんのご講演の前（13:30-15:30）に ToPS セミナーが開催されます．そちらにも是非どうぞ！ http://takeichi.ipl-lab.org/~tops/upcoming_seminar.html 蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/ ============================================= Tue 18 December 2012, 16:00-17:30 Keiko Nakata (Tallinn University of Technology), 2 Talks 国立情報学研究所 12階 1208号室 Rm. 1208, 12F, National Institute of Informatics Access: http://www.nii.ac.jp/en/about/access *** 場所・時間が変わりました *** *** The time and venue have been changed *** 中田さんのご講演の前（13:30-15:30）に，同じ場所で ToPS セミナーが開催されます．そちらにも是非どうぞ！http://takeichi.ipl-lab.org/~tops/upcoming_seminar.h… Prior to Dr. Nakata’s talk there will be a “ToPS seminar” at the same location. The talks will be of similar research interests. http://takeichi.ipl-lab.org/~tops/upcoming_seminar.html Talk 1: Proving open induction using delimited control operators Open Induction (OI) is a principle classically equivalent to Dependent Choice, which is, unlike the later, closed under double-negation translation and A-translation. In the context of Constructive Reverse Mathematics, Wim Veldman has shown that, in presence of Markov's Principle, OI on Cantor space is equivalent to Double-negation Shift (DNS). With Danko Ilik, we have reworked Veldman's proof to give a constructive proof of OI, where DNS is interpreted using delimited control operators. Joint work with Danko Ilik. Talk 2: Walking through infinite trees with mixed induction and coinduction: A Proof Pearl with the Fan Theorem and Bar Induction. We study temporal properties over infinite binary red-blue trees in the setting of constructive type theory. We consider several familiar path-based properties, typical to linear-time and branching-time temporal logics like LTL and CTL*, and the corresponding tree-based properties, in the spirit of the modal mu-calculus. We conduct a systematic study of the relationships of the path-based and tree-based versions of ``eventually always blueness '' and mixed inductive-coinductive ``almost always blueness'' and arrive at a diagram relating these properties to each other in terms of implications that hold either unconditionally or under specific assumptions (Weak Continuity for Numbers, the Fan Theorem, Lesser Principle of Omniscience, Bar Induction). Joint work with Marc Bezem and Tarmo Uustalu.

1 0

講演のお知らせ
by minami＠kurt.cla.kobe-u.ac.jp 12 Dec '12

12 Dec '12

皆様，重複してお受け取りの際はご容赦ください。以下の要領で名古屋数学基礎論/集合論セミナーを開催します．興味のある方は是非参加を検討ください．日時：12月14日（金）15：30〜場所：場所：名古屋大学情報科学（研究科）棟1階105 講演者：嘉田勝（大阪府立大学）講演タイトル：強制拡大で位相空間の性質は保存されるか位相空間論の未解決問題に集合論的手法でアプローチするうえで、「強制拡大で位相空間の性質が保存されるか否か」が重要な鍵となることがある。ここで、位相空間の性質の保存とは、基底モデルに属する位相空間に対して、その強制拡大における対応物として「同一の点集合と開基で定まる位相空間」を考えるときに、基底モデルでみたされる空間の性質が強制拡大でもみたされることを意味するものとする。本講演では、半順序がみたす性質と、その半順序による強制拡大で保存される位相空間の性質との関係について、いくつかの結果を紹介する。 ================================================= アクセス：地下鉄名城線名古屋大学駅から徒歩5〜10分． http://www.nagoya-u.ac.jp/global-info/access-map/higashiyama/index.html http://www.is.nagoya-u.ac.jp/intro/contact.html この講演に関する情報は以下のHPでもご覧になれます． http://researchmap.jp/cardinal_invariants/research-blog/

1 0

Kobe Colloquium on Logic, Statistics and Informatics, Dec. 10 (David Aspero)
by Joerg Brendle 07 Dec '12

07 Dec '12

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。日時：2012年12月10日（月）13:20-14:50 場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室）講演者：David Aspero (Technische Universitaet Wien, Austria) ======================================================================== 題目：Some set theory with restricted choice アブストラクト：I am planning to present the proofs of three theorems involving set theory without the Axiom of Choice or with just restricted forms of AC. One is an observation of mine concerning very large cardinals in a ZF context, another one is a result from a paper by P. Larson and Shelah, and another one a result of Shelah from [Sh835]. ======================================================================== 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm 連絡先：ブレンドレヨーグ brendle(a)kurt.scitec.kobe-u.ac.jp

1 0

Post-doc position available at AIST Kansai: Test generation/optimization
by Takashi KITAMURA 05 Dec '12

05 Dec '12

みなさま、こんにちは。産総研の北村崇師と申します。本研究所の Cyrille Artho に代わり、ポスドク募集のご案内させて頂きます。応募のご検討、及び、関係各位へのご周知をいただけますと幸いです。 ==================================================== Post-doc position available at AIST Kansai: Test generation/optimization ==================================================== Research related to: • Test generation using model-based testing/constraint solving. • Test case minimization using heuristics like delta debugging. Start: 2013 (ideally April, but can be adjusted). Duration: 1 year (extensible dep. on evaluation and restrictions below). • Location: AIST Amagasaki, Japan (20 minutes from Osaka); Research Institute for Secure Systems, System Life-cycle Group. http://www.risec.aist.go.jp/ • Requirements: – Ph.D.at the time when the contract starts; degree must have been awarded less than 7 years ago. – Strong know-how in software analysis and algorithms. – Experience with Java or Scala, and C. – Good written and spoken communication in English. • If interested, please submit your résumé with your publications and a list software projects in which you have participated. • Contact:c.artho@aist.go.jp -- Takashi KITAMURA t.kitamura(a)aist.go.jp, http://staff.aist.go.jp/t.kitamura/ Research Institute for Secure Systems (RISEC) National Institute of Advanced Industrial Science and Technology (AIST)

1 0

55th Tokyo Programming Seminar (Dec 18)
by Kazuyuki ASADA 05 Dec '12

05 Dec '12

[Apologies for multiple copies] Dear all, I am pleased to announce the 55th Tokyo Programming Seminar, which will be held at NII on December 18th (Tue). Oleg Kiselyov Non-deterministic choice in a conventional programming language: Enough for logic programming? Hugo Pacheco Bidirectional Data Transformation by Calculation A detailed program is attached below. I'm looking forward to meeting you at the seminar. Best regards, Kazuyuki Asada ---- The 55th ToPS http://takeichi.ipl-lab.org/~tops/upcoming_seminar.html Time: December 18th (Tue) 2012, 13:30--15:30 Place: Rm. 1208, 12F, National Institute of Informatics Speaker: 1. Oleg Kiselyov Non-deterministic choice in a conventional programming language: Enough for logic programming? Abstract: Logic programming is a fascinating approach, especially for AI and natural language processing. It is greatly appealing to declaratively state the properties of the problem and let the system find the solution. Most intriguing is the ability to run programs `forwards' and `backwards'. However, the built-in search methods of logic programming systems don't fit all problems and hardly if at all customizable. Mainly, quite many computations and models are mostly deterministic. Implementing them in a logic programming language is significantly inefficient and requires extensive use of problematic features such as cut. Another problem is interfacing logic programs with mainstream language libraries: if mode analysis is not available (as is often the case), one has to live with run-time instantiatedness errors. An alternative to logic programming, where non-determinism is default, is a deterministic programming system (such as Scheme, OCaml, Scala or Haskell -- or even C) with (probabilistic) non-determinism as an option. Is this a good alternative? We explore this question. We will use Hansei -- a probabilistic programming system implemented as a library in OCaml -- to solve a number of classic logic programming problems, from zebra to scheduling, to parser combinators, to reversible type checking. http://okmij.org/ftp/kakuritu/logic-programming.html 2. Hugo Pacheco Bidirectional Data Transformation by Calculation Abstract: The advent of bidirectional programming, in recent years, has led to the development of a vast number of approaches from various computer science disciplines. These are often based on domain-specific languages in which a program can be read both as a forward and a backward transformation that satisfy some desirable consistency properties. Despite the high demand and recognized potential of intrinsically bidirectional languages, they have still not matured to the point of mainstream adoption. We contemplate some usually disregarded features of bidirectional transformation languages that are vital for deployment at a larger scale. The first concerns efficiency. Most of these languages provide a rich set of primitive combinators that can be composed to build more sophisticated transformations. Although convenient, such compositional languages are plagued by inefficiency and their optimization is mandatory for a serious application. The second relates to configurability. As update translation is inherently ambiguous, users shall be allowed to control the choice of a suitable strategy. The third regards genericity. Writing a bidirectional transformation typically implies describing the concrete steps that convert values in a source schema to values a target schema, making it impractical to express very complex transformations, and practical tools shall support concise and generic coding patterns.

1 0

RTA 2013: Second Call for Papers
by Nao Hirokawa 04 Dec '12

04 Dec '12

皆様 RTA 2013 の論文募集をご案内致します。今回の RTA はオランダ Eindhoven で行われ、TLCA 2013 との共催となっています。ぜひ投稿をご検討下さい。廣川　直 (JAIST) ************************************************************************* RTA 2013: SECOND CALL FOR PAPERS 24th International Conference on Rewriting Techniques and Applications June 24 - 26, 2013 Eindhoven, The Netherlands collocated with TLCA 2013 as part of RDP 2013 http://rta2013.few.vu.nl/ ************************************************************************* abstract submission February 1 2013 paper submission February 5 2013 rebuttal period March 18-21 2013 notification April 4 2013 final version April 26 2013 ************************************************************************* The 24th International Conference on Rewriting Techniques and Applications (RTA 2013) is organized as part of the Federated Conference on Rewriting, Deduction, and Programming (RDP 2013), together with the 11th International Conference on Typed Lambda Calculi and Applications (TLCA 2013), and several workshops. RDP 2013 will be held at the Eindhoven University of Technology in the Netherlands. *** INVITED SPEAKERS (NEW) *** - Simon Peyton-Jones (Microsoft Research, UK) joint invited speaker for TLCA+RTA 2013 - Jarkko Kari (University of Turku, Finland) invited speaker for RTA 2013 - Mitsu Okada (Keio University, Japan) invited speaker for RTA 2013 *** TOPICS OF INTEREST *** RTA is the major forum for the presentation of research on all aspects of rewriting. Typical areas of interest include (but are not limited to): Applications: case studies; analysis of cryptographic protocols; rule-based (functional and logic) programming; symbolic and algebraic computation; SMT solving; theorem proving; system synthesis and verification; proof checking; reasoning about programming languages and logics; program transformation; XML queries and transformations; systems biology; homotopy theory; implicit computational complexity; Foundations: equational logic; universal algebra; rewriting logic; rewriting models of programs; matching and unification; narrowing; completion techniques; strategies; rewriting calculi; constraint solving; tree automata; termination; complexity; modularity; Frameworks: string, term, and graph rewriting; lambda-calculus and higher-order rewriting; constrained rewriting/deduction; categorical and infinitary rewriting; stochastic rewriting; net rewriting; binding techniques; Petri nets; higher-dimensional rewriting; Implementation: implementation techniques; parallel execution; rewrite and completion tools; certification of rewriting properties; abstract machines; explicit substitutions; automated (non)termination and confluence provers; automated complexity analysis. *** PUBLICATION *** The proceedings will be published by LIPIcs (Leibniz International Proceedings in Informatics). LIPIcs is open access, meaning that publications will be available online and free of charge, and authors keep the copyright for their papers. LIPIcs publications are indexed in DBLP. For more information about LIPIcs please consult: <http://www.dagstuhl.de/en/publications/lipics> *** SUBMISSION GUIDELINES *** Submissions must be - original and not submitted for publication elsewhere, - written in English, - a research paper, or a problem set, or a system description, - in pdf prepared with pdflatex using the LIPIcs stylefile: <http://drops.dagstuhl.de/styles/lipics/lipics-authors.tgz>, - at most 10 pages for system description, at most 15 pages for the other two types of submissions - submitted electronically through the EasyChair system at: <https://www.easychair.org/conferences/?conf=rta2013>. The page limit and the deadline for submission are strict. Additional material for instance proof details, may be given in an appendix which is not subject to the page limit. However, submissions must be self-contained within the respective page limit; reading the appendix should not be necessary to assess the merits of a submission. *** PROGRAMME COMMITTEE CHAIR *** Femke van Raamsdonk (VU University Amsterdam, The Netherlands) *** PROGRAMME COMMITTEE *** Eduardo Bonelli National University of Quilmes, Argentina Byron Cook Microsoft Research Cambridge, UK Stephanie Delaune ENS Cachan, France Gilles Dowek Inria Paris-Rocquencourt, France Maribel Fernandez King's College London, UK Nao Hirokawa JAIST Ishikawa, Japan Delia Kesner University Paris-Diderot, France Helene Kirchner Inria Paris-Rocquencourt, France Barbara Koenig University Duisburg Essen, Germany Temur Kutsia Johannes Kepler University Linz, Austria Aart Middeldorp University of Innsbruck, Austria Vincent van Oostrom Utrecht University, The Netherlands Femke van Raamsdonk VU University Amsterdam, The Netherlands Kristoffer Rose IBM Research New York, USA Manfred Schmidt-Schauss Goethe University Frankfurt, Germany Peter Selinger Dalhousie University, Canada Paula Severi University of Leicester, UK Aaron Stump The University of Iowa, USA Tarmo Uustalu Institute of Cybernetics Tallinn, Estonia Roel de Vrijer VU University Amsterdam, The Netherlands Johannes Waldmann HTWK Leipzig, Germany Hans Zantema Eindhoven University of Technology, The Netherlands *** CONFERENCE CHAIR *** Hans Zantema (Eindhoven University of Technology, The Netherlands) *** STEERING COMMITTEE *** Mauricio Ayala-Rincon Brasilia University, Brasilia Frederic Blanqui INRIA Tsinghua University Beijing, China Salvador Lucas Technical University of Valencia, Spain Georg Moser (chair) University of Innsbruck, Austria Masahiko Sakai Nagoya University, Japan Sophie Tison University of Lille, France *** FURTHER INFORMATION *** Questions related to submission, reviewing, and programme should be sent to the programme committee chair Femke van Raamsdonk, email femke at few.vu.nl.

1 0

Talk by Keiko Nakata (Tallinn University of Technology), Tue 18 December 2012
by Ichiro Hasuo 03 Dec '12

03 Dec '12

みなさま，東京大学の蓮尾と申します．来る12月18日，タリン工科大学の中田景子さんをお迎えしてご講演いただきます．（2題，連続講演です）詳細は以下です．ご興味のある方はぜひお越しください！蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/ -------------------------------------------------------------------------------------------------------------- Tue 18 December 2012, 16:40-18:10 Keiko Nakata (Tallinn University of Technology), 2 titles 理学部7号館1階 102教室 Room 102, School of Science Bldg. No. 7 Title Proving open induction using delimited control operators Abstract Open Induction (OI) is a principle classically equivalent to Dependent Choice, which is, unlike the later, closed under double-negation translation and A-translation. In the context of Constructive Reverse Mathematics, Wim Veldman has shown that, in presence of Markov's Principle, OI on Cantor space is equivalent to Double-negation Shift (DNS). With Danko Ilik, we have reworked Veldman's proof to give a constructive proof of OI, where DNS is interpreted using delimited control operators. Joint work with Danko Ilik. --- Title Walking through infinite trees with mixed induction and coinduction: A Proof Pearl with the Fan Theorem and Bar Induction. Abstract We study temporal properties over infinite binary red-blue trees in the setting of constructive type theory. We consider several familiar path-based properties, typical to linear-time and branching-time temporal logics like LTL and CTL*, and the corresponding tree-based properties, in the spirit of the modal mu-calculus. We conduct a systematic study of the relationships of the path-based and tree-based versions of ``eventually always blueness '' and mixed inductive-coinductive ``almost always blueness'' and arrive at a diagram relating these properties to each other in terms of implications that hold either unconditionally or under specific assumptions (Weak Continuity for Numbers, the Fan Theorem, Lesser Principle of Omniscience, Bar Induction). Joint work with Marc Bezem and Tarmo Uustalu.

1 0

PPL2013論文募集
by Shinya Katsumata 01 Dec '12

01 Dec '12

（重複の場合はご容赦ください．）東京工業大学の権藤と京都大学の勝股と申します．来年3月に福島県会津若松東山温泉で開催される第15回プログラミングおよびプログラミング言語ワークショップ (PPL2013) のご案内（2回目）です．みなさまのご投稿，ご参加をお待ちしております．論文投稿・発表申込方法の詳細と招待講演者の情報を追加いたしました．カテゴリ1はeasy chairを通して，カテゴリ2, 3は下記投稿用メールアドレスまでお申込ください． -------------------------------------------------------------------------- 第15回プログラミングおよびプログラミング言語ワークショップ（PPL2013） http://www.pllab.riec.tohoku.ac.jp/ppl2013/ 論文募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2013年3月4日(月)〜3月6日(水) 会場: 福島県会津若松東山温泉「御宿東鳳」http://www.onyado-toho.co.jp/ PPL2013は，プログラミングおよびプログラミング言語に関する研究者が一堂に会し，最新の研究成果の発表，および新たな研究課題についての討論やアイディア交換等を行うことを目的とした，合宿形式のワークショップです．プログラミングおよびプログラミング言語の理論・設計・実装・処理系などに関する研究発表を，カテゴリ別に幅広く募集します．カテゴリ１: 国内外で未発表の論文の発表カテゴリ２: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ３: ポスター・デモ発表（既発表・未発表の別を問いません） ※ショートプレゼンテーションは行いませんカテゴリ１の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また，ポスター・デモを含む全発表のなかから，聴衆の投票により，最も優秀なプレゼンテーションに発表賞（一般の部，学生の部）を授与する予定です．カテゴリ１（国内外未発表論文） ------------------------------ 完成した理論やシステムの研究発表のみならず，萌芽的なアイディアや問題点の提示等も歓迎します．発展途上の研究内容も積極的に採録する方針です（ただし，PPLでの発表として相応しくないと判断される場合は，この限りではありません）．また，カテゴリ1で発表された研究については，会場での討議や査読コメントをもとにその完成度を高め，将来の学術雑誌・会議等での業績に結び付けることを奨励しています．そのため，予稿集の配布は参加者のみへの限定的なものとする予定です．採録された論文は，PPL2013参加者に配布される予稿集に掲載され，参加者のみがアクセス可能な形でWEB上で公開されます（論文へのリンク集ページを作成し，閲覧に必要なパスワードを参加者に連絡します）．カテゴリ１で発表された研究のうち，PPL2013プログラム委員会として優れていると認めるものは，PPL2013終了後（2013年4月下旬予定），「コンピュータソフトウェア」誌PPL2013推薦論文としての投稿が可能です．推薦論文は，PPL プログラム委員が引き続き査読を行うことによる，迅速な査読プロセスを特長としています．カテゴリ２（国外既発表論文） ---------------------------- 査読付の国際会議または学術雑誌等で既発表であるが，国内では未発表な研究の紹介をする場です．採録決定済みの研究も含みます．PPLへの関連をもとに採録を判定いたします．カテゴリ３（ポスター・デモ発表） ------------------------------------------ ２時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採録を判定いたします．また，申込多数の場合は抽選によって採否を決定する可能性があります．なお，PPL2013 ではポスターやデモによる活発な意見交換を促進したいという観点から，ショートプレゼンテーションのセッションは設けません．招待講演 -------- 鍋島英知 (山梨大学) 村主崇行 (京都大学) 以上のお二方の招待講演を予定しています． ====================================================================== 投稿・発表申込要領３つのカテゴリそれぞれに対して，投稿は以下のように行って下さい．最新の情報は上記Webページでご確認下さい．カテゴリ１（国内外未発表論文） ------------------------------ 投稿手続きは二段階です．発表申込を行った上で論文提出を行って下さい．発表申込先： https://www.easychair.org/conferences/?conf=ppl2013 発表申込締切：2012年12月21日(金) 17:00 (JST) 著者名，所属，論文タイトル，論文概要（日本語300〜400字程度もしくは英語200 words程度）を提出してください．論文提出締切：2013年1月11日(金) 17:00 (JST) 10ページ程度（最大15ページ）の論文（英語もしくは日本語，PDF形式）を提出して下さい．採否通知：2013年2月4日(月) 最終原稿提出締切：2013年2月15日(金) 17:00 (JST) 採録された論文の最終原稿の提出方法は，採否通知にてお知らせいたします． (注) カテゴリ１への投稿論文と類似の論文を，他の会議（予稿集を出版するもの）・論文誌などに同時投稿する場合は，査読の有無に関わらず，その旨を発表申込および論文提出の際に明記して下さい．PPLでは同時投稿の事実のみをもって論文を不採録とすることはありませんが，採否の決定に利用する場合があります（他の会議との重複を避けるため，発表内容についての条件付採録とすることもあります）．カテゴリ２（国外既発表論文） ---------------------------- 昨年同様，カテゴリ2の申込締切が少し早くなっていますのでご注意ください．発表申込時に採録が決定している国際会議または学術雑誌等の発表論文が対象です．理論系だけではなく実装系の論文の投稿も歓迎いたします．発表申込先： submit-ppl2013 [at] kurims.kyoto-u.ac.jp （[at]を@に置き換えて下さい）発表申込締切：2013年1月23日(水) 17:00 (JST) 原論文（ページ数不問，PDF形式）とabstract（テキスト形式）を，著者名，所属，論文タイトル，原論文の出典（発表会議名，掲載済／予定の別等）と併せて上記申込先宛にお送り下さい．採否通知：2013年2月4日(月) 最終原稿提出締切：2013年2月15日(金) 17:00 (JST) カテゴリ３（ポスター・デモ発表） ------------------------------------------ ポスター・デモの区別を行なわずに募集いたします．デモを行なう場合は，発表概要においてその旨をご説明ください．発表申込先： submit-ppl2013 [at] kurims.kyoto-u.ac.jp （[at]を@に置き換えて下さい）発表申込締切：2013年2月6日(水) 17:00 (JST) 著者名，所属，発表タイトル，発表概要（200〜300字程度），希望する発表形態（ポスター・デモの別），をテキスト形式で上記申込先宛にお送り下さい．採否通知：2013年2月15日(金) 問い合わせ先：oc-ppl2013 [at] kurims.kyoto-u.ac.jp （[at]を@に置き換えて下さい） ====================================================================== プログラム委員会青木利晃 (北陸先端科学技術大学院大学) 青谷知幸 (北陸先端科学技術大学院大学) 天野俊一 (IBM東京基礎研究所) 磯部祥尚 (産業技術総合研究所) 岩見宗弘 (島根大学) 角谷良彦 (東京大学) 勝股審也 (京都大学) [プログラム共同委員長] 小宮常康 (電気通信大学) 権藤克彦 (東京工業大学) [プログラム共同委員長] 田浦健次朗 (東京大学) 高田喜朗 (高知工科大学) 田辺良則 (国立情報学研究所) 中田景子 (Institute of Cybernetics at Tallinn University of Technology) 中野圭介 (電気通信大学) 長谷部浩二 (筑波大学) 番原睦則 (神戸大学) 松崎公紀 (高知工科大学) 実行委員会上野雄大 (東北大学電気通信研究所) [実行委員長] 鵜川始陽 (電気通信大学) [実行副委員長] 勝股審也 (京都大学) [プログラム共同委員長] 権藤克彦 (東京工業大学) [プログラム共同委員長] --------------------------------------------------------------------------

1 0

Talk by Kazushige Terui (11:00-, 29 Nov)
by Shinya Katsumata 28 Nov '12

28 Nov '12

京都大学数理解析研究所の勝股です。 11月29日11:00から、当研究所の照井一成氏が以下の講演をいたしますので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 29 Nov, 2012 Place: Rm 478, Research Building 2, Main Campus, Kyoto University http://www.kyoto-u.ac.jp/en/access/campus/main.htm (See 34) 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speaker: Kazushige Terui (RIMS, Kyoto University) Title: Herbrand's theorem via hypercanonical extensions Abstract: よく知られているエルブランの定理を代数的に捉えたい。そのために古典論理のみならず、部分構造論理一般について考える。（様相などの単調／反単調な演算子を追加してもよい。たとえば直観主義論理、単調様相論理、線形論理、ファジー論理など）。 Lをそのような命題論理とし、その最小述語拡大をQLとすると、QLについてエルブランの定理が成り立つための代数的十分条件として、Lに対応する代数のクラスがコンパクトな完備化について閉じていることが挙げられる。そのような完備化の代表例はストーン双対性に基づくものであり、その一般化は正準拡大（canonical extensions）と呼ばれ広く研究されている。しかし部分構造論理の観点から興味深い代数のクラスの多くは、正準拡大について閉じているかどうか定かではない。そこで本講演では、新たなコンパクト完備化として超正準拡大（hypercanonical extensions）を導入する。これは非古典論理証明論における「シークエント計算⇒超シークエント計算」という発想に基づいて正準拡大を一般化したものである。それによりゲーデル＝ダメット論理、monoidal t-norm logicをはじめとする多くの論理についてエルブランの定理が系統的に成り立つことを示す。（今年度MLGにおける講演と同内容）

1 0

【訂正】Computability Theory and Foundations of Mathematics (CTFM)
by Naohi Eguchi 26 Nov '12

26 Nov '12

Logic-ml の皆様，先日ご案内しました計算可能性，逆数学等に関する研究会 Computability Theory and Foundations of Mathematics (CTFM) (2013年2月18日(月)〜2月20日(水)，東京工業大学大岡山キャンパス) http://sendailogic.math.tohoku.ac.jp/CTFM/ につきまして，講演申し込み締め切りが2013年12月18日となっていましたが*2012年*12月18日(火)の誤りでした．訂正してお詫び申し上げます．江口直日　(CTFM プログラム委員) 問い合わせ先　CTFM(a)math.tohoku.ac.jp ============================================================ Computability Theory and Foundations of Mathematics (Tokyo Institute of Technology, Tokyo, Japan, February 18 - 20, 2013) http://sendailogic.math.tohoku.ac.jp/CTFM/ ============================================================ Computability Theory and Foundations of Mathematics (CTFM) aims to develop computability theory and logical foundations of Mathematics. The scope involves the topics Computability Theory, Reverse Mathematics, Nonstandard Analysis, Proof Theory, Constructive Mathematics, Theory of Randomness and Computational Complexity Theory. This is a successor workshop to Workshop on Proof Theory and Computability Theory 2012 - Philosophical Frontiers in Reverse Mathematics (February 20 - 23, 2012, Tokyo, Japan). -------------------------------------------- Deadline of Submission for Presentations: December 18, 2013 /*2012*/ -------------------------------------------- Invited Speakers: Chi Tat Chong (National University of Singapore) Erik Palmgren (Stockholm University) Michael Rathjen (University of Leeds) Helmut Schwichtenberg (LMU Munich) Stephen G. Simpson (Pennsylvania State University) Yang Yue (National University of Singapore) Wu Guohua (Nanyang Technological University) -------------------------------------------- Programme Committee: Toshiyasu Arai (Chiba) Naohi Eguchi (Tohoku) Hajime Ishihara (JAIST) Ryo Kashima (Tokyo Institute of Technology) Sam Sanders (Ghent) Kazuyuki Tanaka (Tohoku, Co-chair) Andreas Weiermann (Ghent, Co-chair) Takeshi Yamazaki (Tohoku) Keita Yokoyama (Tokyo Institute of Technology) --------------------------------------------

1 0

Postdoc positions, Tokyo/Kyoto, Computation Theory
by Akitoshi Kawamura 26 Nov '12

26 Nov '12

皆様東京大学の河村と申しますメーリングリストをお借りして新学術領域研究「計算限界解明」（代表：渡辺治）の研究員の公募（締切12月20日）について御案内させて頂きます計算量理論の諸問題への挑戦を目標とする研究領域ですがウェブページにありますように数理論理学的手法も中心テーマの一つでございます国内外を問わず皆様の周りの方々に広くお知らせ頂ければ幸いです -- 河村彰星東京大学大学院情報理工学系研究科コンピュータ科学専攻　助教 http://www-imai.is.s.u-tokyo.ac.jp/~kawamura/index_j.html ％％％％％％％％％％％％％％％％％％％％％％％％％％％ポスドク募集文部科学省科学研究費補助金新学術領域研究　「多面的アプローチの統合による計算限界の解明」代表者：渡辺治 (東京工業大学） http://www.al.ics.saitama-u.ac.jp/elc/ では、下記のように4名の研究員を募集いたします。国際公募する予定で英語での文章しかございませんが、ご容赦下さい。よろしくお願いいたします。 --------------------------------------------------------------------- Two-year post-doctoral positions, Tokyo and Kyoto, Computation Theory --------------------------------------------------------------------- http://www.al.ics.saitama-u.ac.jp/elc/en/?pd The newly established Center for Exploring the Limits of Computation (CELC, Tokyo, Japan) seeks applications for four post-doctoral fellow positions in Computational Complexity Theory and related areas. The appointments are for two years starting in April 2013 (or as soon as possible). A monthly salary of approximately 350,000 Japanese yen plus a research allowance will be offered. Applicants should hold a PhD in theoretical computer science or related fields (or be expected to do so by July 2013). Two of the fellows will be based at the Tokyo site (Tokyo Institute of Technology and the CELC) and two at the Kyoto site (Kyoto University). Collaboration with other research groups of the ELC project (including visits for several months) will be encouraged and supported. Applications should include * a curriculum vitae, * list of publications, * a research statement, and * three letters of referees (to be sent directly from the referees). Applications and letters of referees should be sent via email to elc-pd-application(a)is.titech.ac.jp. Priority will be given to applications received by December 20, 2012. Applicants may be invited to an interview in early 2013 (the travel expenses will be covered). --------- About ELC --------- Exploring the Limits of Computation (ELC) is a five-year research project funded by the Japanese Ministry of Education, Culture, Sports, Science and Technology. Project Title (formal): A multifaceted approach toward understanding the limitations of computation Short Title: Exploring the Limits of Computation (ELC) Project Term: 2012.7 - 2017.3 Researchers have proposed various techniques for investigating the limits of computation, many of which have been sharpened in depth during the last two decades. We may soon be entering the stage of expecting some big breakthrough results toward understanding the limits of computation. In this project, we investigate these techniques and relationships among them with the goal of finding the next steps toward a big breakthrough. We propose the following three lines of research, each of which will be conducted by three core research groups (i.e., nine core research groups altogether). A. Team for pushing the current frontier of research on the limits of computation. B. Team for investigating the limits of computation by using various algorithmic/optimization techniques (even by using supercomputers). C. Team for introducing new approaches to and interpretations of the existing techniques for investigating the limits of computation. We also create a research center (CELC) in Tokyo for investigating computational complexity theory by stimulating worldwide collaborations among researchers based on our core research groups, hosting short/long term visitors and postdoctoral researchers, and organizing various meetings and workshops. We welcome researchers working on subjects related to computational complexity theory to join us for various occasions. Project webpage http://www.al.ics.saitama-u.ac.jp/elc/en/

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml