Logic-ml

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

7 participants
1772 discussions

[Second Call for Paper] LORI-VI: The Sixth International Conference on Logic, Rationality and Interaction, September 11-14, 2017, Hokkaido University, Sapporo, Japan
by Katsuhiko Sano 13 Mar '17

13 Mar '17

Second Call for Papers LORI-VI: The Sixth International Conference on Logic, Rationality and Interaction September 11-14, 2017, Hokkaido University, Sapporo, Japan http://golori.org/lori2017/ [About LORI] The International Conference on Logic, Rationality and Interaction (LORI) conference series aims at bringing together researchers working on a wide variety of logic-related topics that concern the understanding of rationality and interaction. The series aims at fostering a view of Logic as an interdisciplinary endeavour, and supports the creation of an East-Asian community of interdisciplinary researchers. [News] *** 60,000 yen (approx 500 Euro) prize for best student paper *** The best student paper will be selected from the contributed student papers accepted for presentation at LORI VI, and be awarded the prize of 60,000 Japanese Yen (approximately 500 Euro). For more details, see http://golori.org/lori2017/award.html . [Call for Papers] We invite submission of contributed papers on any of the broad themes of LORI series; specific topics of interest include, but are not limited to, formal approaches to ・ agency ・ argumentation and agreement ・ belief representation ・ cooperation ・ belief revision and belief merging ・ strategic reasoning ・ games ・ decision making and planning ・ knowledge and action ・ epistemology ・ dynamics of informational attitudes ・ speech acts ・ knowledge representation ・ interaction ・ norms and normative systems ・ natural language ・ rationality ・ philosophy and philosophical logic ・ preference and utility ・ social choice ・ probability and uncertainty ・ social interaction ・ intentions, plans, and goals Submitted papers should be at most 12 pages long, with one additional page for references, in PDF format following the Springer LNCS style. Please submit your paper by Friday March 31, 2017, via EasyChair : http://easychair.org/conferences/?conf=lori6 . [Publication] Accepted papers will be collected as a volume in the FoLLI Series on Logic, Language and Information, and authors may be later invited to submit extended versions of their papers in a special issue of a prestigious journal. [Website] For detailed conference information and registration, please visit http://golori.org/lori2017/ . [Invited Speakers] Mike Dunn: Indiana University, U.S.A. Alan Hajek: Australian National University, Australia Nina Gierasimczuk: Technical University of Denmark, Denmark Willemien Kets: Northwestern University, U.S.A Sara Negri: University of Helsinki, Finland Hiroakira Ono: JAIST, Japan [PC Chairs] Alexandru Baltag: University of Amsterdam, The Netherlands Jeremy Seligman: University of Auckland, New Zealand [Conference Organiser] Tomoyuki Yamada: Hokkaido University, Japan [Sponsors] LORI Tsinghua University - University of Amsterdam Joint Research Centre for Logic Hokkaido University [Contacts] Programme: The PC Chairs <lori6(a)easychair.org> Conference: Tomoyuki Yamada <tomoyuki.s.yamada(a)gmail.com>

1 0

JAIST Logic Seminar Series
by Takako Nemoto 10 Mar '17

10 Mar '17

皆様 Ludwig-Maximilians-Universität München の Josef Berger 博士の講演のお知らせです。どうぞふるってご参加ください。問い合わせ先：根元　多佳子北陸先端科学技術大学院大学　情報科学系 email: t-nemoto(a)jaist.ac.jp --------------------------------------------- *JAIST Logic Seminar Series* Date: Thursday 16 March, 2017, 15:20-17:00 Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Josef Berger (udwig-Maximilians-Universität München, Germany) (joint work with Gregor Svindland) Brouwer's fan theorem and convexity In the framework of Bishop's constructive mathematics, we introduce a correspondence between sets B of finite binary sequences on the one hand and uniformly continuous functions f on the unit interval on the other hand. This correspondence is compatible with basic properties of the involved objects as follows: i) B is a bar if and only if the corresponding f is positive-valued ii) B is a uniform bar if and only if f has positive infimum iii) B is weakly convex if and only f is weakly convex. This simplifies and generalises a result in William H. Julian and Fred Reichmann, A uniformly continuous function on [0, 1] that is everywhere different from its infimum. Pacific Journal of Mathematics 111, No 2 (1984) 333–340

1 0

QIT36のご案内
by NISHIMURA Harumichi 08 Mar '17

08 Mar '17

logic-mlの皆様 QIT36世話人に代わりまして第36回量子情報技術研究会(QIT36)の会告を以下の通り投稿させていただきます．どうぞよろしくお願いいたします．名古屋大学大学院情報科学研究科西村治道 ---------------- 第36回量子情報技術研究会(QIT36) 研究会の内容：情報科学と量子力学を融合させた新しい分野，量子情報科学に関する研究会です．情報を担う物理系の量子力学的側面を積極的に活かした新しい情報処理原理の研究とそこから開かれる新しい学問体系の構築および新しい情報技術パラダイムの創生を目指して，情報科学，物理学，光エレクトロニクスを含む理学，工学，数理科学に携わる研究者間に自由な討論の場を提供し，この研究分野の発展を図ることを目的としています．第36回研究会を下記のように開催いたします．現在この分野で活躍する研究者は勿論，自分の研究資産が何らかの形で使えそうだと予感している研究者・技術者など，広く関連する分野の研究者・技術者からの発表を募集致します．聴講のみの参加も歓迎致しますので，奮ってお申し込みください．日時: 2017年5月29日(月)～30日(火) 会場: 立命館大学朱雀キャンパス５階大講義室（ホール） (〒604-8520 京都市中京区西ノ京朱雀町１）発表募集分野 (申し込み状況によっては査読の可能性あり)：量子情報，量子計算，量子暗号など広く量子情報技術に関わる理論的研究，実験的研究，計算機科学的研究，数学的研究，および，その他関連分野．定員: 200名参加費: 事前振込み一般2,000円，学生1,000円（当日会場払いは一般3,000円，学生2,000円．学生に限り予稿集なしで当日無料参加可能です．）懇親会費：事前振り込み一般4,000円，学生2,000円．（当日会場払いは一般5,000円，学生3,000円．）招待・チュートリアル講演：笹川崇男（東京工業大学）：CRESTプロジェクト「トポロジカル量子計算の基盤技術構築」の研究構想について田家慎太郎（京都大学）：光格子を用いた実験による、量子磁性や高温超伝導といった固体電子系の物理に対する量子シミュレーションに関した最近の成果と展望について谷誠一郎（NTT）：機能制限された量子計算モデルの能力について並木亮（学習院大学）：連続量量子チャンネルの最近の理論展開について研究会参加申込要領：参加申込は下記 Web にて受付けます： http://staff.aist.go.jp/s-kawabata/qit/ 講演 (口頭，ポスター) の申込，予稿集原稿 PDF の提出は，電子情報通信学会の Web システムを使用する予定．【口頭講演申込締切】2017年4月7日(金) 【ポスター講演申込締切】2017年4月21日(金) 【予稿原稿提出締切】2017年4月21日(金) 【参加申込締切】2017年4月28日(金) 【問合せ先】山下茂（立命館大学）中西正樹（山形大学) 添田彬仁（東京大学) Email: qit36(a)ngc.is.ritsumei.ac.jp 主催: 量子情報技術時限研究専門委員会 (委員長: 竹内繁樹 (京都大学)) 共催: 応用物理学会量子エレクトロニクス研究会立命館大学情報理工学部

1 0

First NII Programming and Logic Workshop
by Makoto Tatsuta 27 Feb '17

27 Feb '17

First NII Programming and Logic Workshop Date: March 2--3, 2017 Place: National Institute of Informatics, Room 2006 (20th floor) 場所: 国立情報学研究所 20階 2006室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Program: March 2 10:20--11:00 Wei-Ngan Chin (National University of Singapore) Title: Automated Verification and Analysis of Expressive Specifications 11:00--11:40 Zhenjiang Hu (National Institute of Informatics) Title: Towards Change-Oriented Programming 11:40--11:55 Break 11:55--12:35 Makoto Tatsuta (National Institute of Informatics) Title: Presburger and Mutual Inductive Definitions 12:35--14:00 Lunch Break 14:00--14:40 Quang Loc Le (Singapore University of Technology and Design / National University of Singapore) Title: A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic 14:40--15:20 Hsiang-Shang Ko (National Institute of Informatics) Title: An Axiomatic Basis for Bidirectional Programming 15:20--15:35 Break 15:35--16:15 Daisuke Kimura (Toho University) Title: Decidability of Entailments in Separation Logic with Arrays 16:15--16:55 Mahmudul Faisal Al Ameen (National University of Singapore) Title: Separation-Logic-Based Analyzer for Detecting Memory Errors March 3 10:15--10:55 Koji Nakazawa (Nagoya University) Title: Cyclic-Proof-Based Decision Procedure for Symbolic Heaps and Inductive Definitions 10:55--11:35 Shin-Cheng Mu (Academia Sinica) Title: Towards Derivation of Monadic Programs: A Case Study of States and Nondeterminism 11:35--11:50 Break 11:50--12:30 Andreea Costea National University of Singapore) Title: Automated Reasoning for Race-Free Channels with Explicit Synchronization and Precise Disjunction Abstracts: ---------------------------------------------------------------------- Speaker: Wei-Ngan Chin (National University of Singapore) Title: Automated Verification and Analysis of Expressive Specifications Abstract: The last two decades have seen a proliferation of research activities in methodologies, techniques and systems for automated verification and analysis of software programs. One driving force in this direction has been the deployment of expressive logics that are able to capture specifications of programs in a concise and precise manner. One of these logics that my research group has been pre-occupied with in the last decade is separation logic itself, made popular by seminal works of John Reynolds and Peter O’Hearn. Separation logic is a sub-structural which treats memory locations as resources that can be transferred, borrowed or consumed. Such a resource logic allows must-aliasing and updates to be succinctly expressed. We have looked into various extensions to support expressive specification logics. We have also explored automated verification techniques that work with inductive predicates. We have proposed and evaluated decision procedures on satisfiability and entailment on some fragments of our logics. We have moreover extended our approach to support incremental specification inference with the help of second-order unknown predicates. These works have challenged us to go beyond properties that guarantee memory safety and correctness, to include also termination, immutability infinity, deeper sharing, communication and concurrency. We shall describe several aspects of our recent endeavours here. ---------------------------------------------------------------------- Speaker: Zhenjiang Hu (National Institute of Informatics) Title: Towards Change-Oriented Programming Abstract: Change is essential and expensive in software development. Although a significant amount of work has been done on software change, its status as a scientific discipline is still an open challenge. In this talk, I will show that it is possible to treat software change as a first-class citizen in software development. The success of this work could lead to change-oriented programming, a new programming paradigm that can effectively cope with software dynamics. ---------------------------------------------------------------------- Speaker: Makoto Tatsuta (National Institute of Informatics) Title: Presburger and Mutual Inductive Definitions Abstract: This talk proposes some restrictions for a system of Presburger arithmetic and mutual inductive definitions and proves the decidability of truth in the system. To prove it, this talk shows that every inductively defined predicate in the system represents a semilinear set. Since inductively defined predicates can be eliminated, the truth is decided in the arithmetic. This system is an extension of the system given in our APLAS 2016 paper but more expressive as it can handle mutual inductive definitions and more than one induction steps in inductive definitions. ---------------------------------------------------------------------- Speaker: Quang Loc Le (Singapore University of Technology and Design / National University of Singapore) Title: A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic Abstract: We consider the satisfiability problem for a fragment of separation logic including inductive predicates with shape and arithmetic properties. We show that the fragment is decidable if the arithmetic properties can be represented as semilinear sets. Our decision procedure is based on a novel algorithm to infer a finite representation for each inductive predicate which precisely characterises its satisfiability. Our analysis shows that the proposed algorithm runs in exponential time in the worst case. To show the feasibility of our proposal, we have implemented our decision procedure, integrated it into an existing verification system and evaluated the solver on a set of satisfiability problems which is generated from the verification of heap-manipulated programs. ---------------------------------------------------------------------- Speaker: Hsiang-Shang Ko (National Institute of Informatics) Title: An Axiomatic Basis for Bidirectional Programming Abstract: Among the frameworks of bidirectional transformations proposed for addressing various synchronisation problems, Foster et al.’s lenses have influenced the design of a generation of bidirectional programming languages. Most of these languages are highly declarative, and only allow the programmer to specify a consistency relation with limited control over the behaviour of the automatically derived consistency restorer. However, synchronisation problems are diverse and require vastly different consistency restoration strategies, and the programmer must be empowered to fully control and reason about the consistency restoration behaviour of their bidirectional programs. The putback-based approach to bidirectional programming was proposed to address this issue once and for all, and this talk will present the latest result along this line of research: a Hoare-style logic for the putback-based language BiGUL. With this Hoare-style logic, the BiGUL programmer can precisely understand the bidirectional behaviour of their programs by reasoning solely in the putback direction. The theory underlying the Hoare-style logic has been formalised and checked in the dependently typed language Agda, but this talk will give a semi-formal presentation of the logic suitable for human reasoning. ---------------------------------------------------------------------- Speaker: Daisuke Kimura (Toho University) Title: Decidability of Entailments in Separation Logic with Arrays Abstract: We show decidability of validity of entailments in symbolic-heap fragment of separation logic with arrays, which is designed for verifying array-manipulating imperative programs. Our proof is given by translating entailments into formulas of Presburger Arithmetic, which is known to be decidable. Finally we provide an implementation of our decision procedure, in which Presburger-formulas are decided by an internally called SMT-solver. ---------------------------------------------------------------------- Speaker: Mahmudul Faisal Al Ameen (National University of Singapore) Title: Separation-Logic-Based Analyzer for Detecting Memory Errors Abstract: This talk discusses an implementation of a separation-logic-based analyzer for memory errors. This system is based on symbolic heap with presburger arithmetic. This implementation extracts errors by analyzing the strongest postcondition. The system abstracts all the existentially quantified pointers. A while loop is analyzed using fixed point analysis and it uses an arithmetic decision procedure. It is also intended to analyze array and inter-procedure analysis. ---------------------------------------------------------------------- Speaker: Koji Nakazawa (Nagoya University) Title: Cyclic-Proof-Based Decision Procedure for Symbolic Heaps and Inductive Definitions Abstract: We introduce a new cyclic-proof system CSLID_omega for separation logic with inductively defined predicates. CSLID_omega is complete and gives decision procedure for entailment checking based on the unfold-match approach. ---------------------------------------------------------------------- Speaker: Shin-Cheng Mu (Academia Sinica) Title: Towards Derivation of Monadic Programs: A Case Study of States and Nondeterminism Abstract: Equational reasoning is among the most important tools that functional programming provides us. Curiously, relatively little attention has been paid on reasoning about monadic programs. In this talk we propose some theorems and patterns useful for derivation of monadic programs, focusing on non-determinism and states. ---------------------------------------------------------------------- Speaker: Andreea Costea National University of Singapore) Title: Automated Reasoning for Race-Free Channels with Explicit Synchronization and Precise Disjunction Abstract: The usage of the message passing for inter-process communication leveraged the performance and scalability of computing platforms leading to a rise in the level of concurrency. Together with its benefits though, message passing also places a burden on the safety and correctness verification process of concurrent system, which was already a challenging task even in the absence of message passing. The current state of the art tackles this problem of safe message communication assuming the systems rely solely of message passing in order to obtain concurrency. However, this is generally not true, since existing software tend to use a combination of synchronization mechanisms. Our aim is to break the assumption of unique synchronization mechanisms, and step further into reasoning about hybrid communication system, where different concurrency instruments intermingle. We therefore present a multiparty session logic which vows to marry the message passing model with explicit synchronization mechanisms, such as CountDownLatch. In this context, we consider how to ensure well-formedness of the session logic, and how to build summaries that can help ensure race-freedom and type safety amongst shared channels. ---------------------------------------------------------------------- 問合せ先　龍田 (tatsuta(a)nii.ac.jp)

1 0

DICE-FOPARA 2017: deadline extension
by Nao Hirokawa 21 Feb '17

21 Feb '17

皆様 DICE-FOPARA 2017 の論文募集の案内をお送り致します。投稿締切が延長され、3月5日になっております。廣川 [Apologies for cross-postings.] ------------------------------------------------------------------------------------------- 8th Workshop on Developments in Implicit Computational complExity and 5th Workshop on Foundational and Practical Aspects of Resource Analysis (DICE-FOPARA 2017) Affiliated with ETAPS 2017 April 22 - 23, 2017, Uppsala, Sweden http://cbr.uibk.ac.at/events/dice-fopara ------------------------------------------------------------------------------------------- OBJECTIVES The first joint international workshop on Developments in Implicit Computational complExity and FOundational and Practical Aspects of Resource Analysis (DICE-FOPARA) will be held in Uppsala, Sweden, from April 22-23, 2017 as part of ETAPS. DICE-FOPARA serves as a forum for presenting results relevant to the implicit computational complexity theory *and* to the analysis of resource consumption by computer programs (e.g. time, space, energy). The workshop brings together researchers that work on foundational issues with researchers that focus more on practical results. For further information, kindly see the workshop's website. INVITED SPEAKERS Elvira Albert (Complutense University of Madrid) Kerstin I. Eder (University of Bristol) Lars Kristiansen (University of Oslo) Jan Reinecke (Universität Saarland) SUBMISSIONS We ask for submission of *regular papers* describing original work (10-15 pages) or *extended abstracts* (2-6 pages) presenting already published work or work in progress. Regular papers must be prepared using the LaTeX EPTCS class (see http://eptcs.org/). Accepted regular papers will appear in an EPTCS volume. Papers should be submitted electronically via the submission page: https://easychair.org/conferences/?conf=dicefopara2017 IMPORTANT DATES Paper submission March 5, 2017 (extended) Notification March 19, 2017 Final versions due March 26, 2017 Workshop date April 22-23, 2017 CONFERENCE VENUE The workshop will be held as a satellite workshop of European Joint Conferences on Theory and Practice of Software 2017 (ETAPS 2017) which takes place in Uppsala, Sweden. PROGRAM COMMITTEE Beniamino Accattoli (Paris) Guillaume Bonfante (Nancy, co-chair) Marko van Eekelen (Nijmegen) Marco Gaboardi (Buffalo) Dan Ghica (Birmingham) Clemens Grelck (Amsterdam) Charles Grellois (Bologna) Nao Hirokawa (JAIST) Jan Hoffmann (CMU) Thomas Jensen (Rennes) Björn Lisper (Mälardalen) Hans-Wolfgang Loidl (Edinburgh) Georg Moser (Innsbruck, co-chair) Kazushige Terui (Kyoto) Simon Wegener (Saarbrücken) Florian Zuleger (Vienna)

1 0

JAIST Logic Seminar Series
by Takako Nemoto 14 Feb '17

14 Feb '17

皆様ベルン大学の Silvia Steila 博士の講演のお知らせです。どうぞふるってご参加ください。問い合わせ先：根元　多佳子北陸先端科学技術大学院大学　情報科学系 email: t-nemoto(a)jaist.ac.jp --------------------------------------------- *JAIST Logic Seminar Series* Date: Tuesday 28 February, 2017, 15:20-17:00 Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Silvia Steila (University of Bern, Switzerland) Title: The strength of the SCT criterion (Joint work with Emanuele Frittaion and Keita Yokoyama). In 2001 Lee, Jones and Ben-Amram introduced the notion of size-change termination (SCT) for first order functional programs, a sufficient condition for termination. They proved that a program is size-change terminating if and only if it satisfies a certain property which can be statically verified from the recursive definition of the program. We call this equivalence SCT criterion. We undertake the study of size-change analysis in the context of Reverse Mathematics. In particular, we prove that the SCT criterion is equivalent to $\Sigma_2$-induction over RCA$_{0}$.

1 0

CCA 2017 (Computability and Complexity in Analysis): 2nd call for papers
by Daniel Graça 11 Feb '17

11 Feb '17

______________________________________________________________ Second Call for Papers Fourteenth International Conference on Computability and Complexity in Analysis (CCA 2017) http://cca-net.de/cca2017/ July 24-27, 2017, Daejeon, Republic of Korea (South Korea) Submission deadline: April 3, 2017 ______________________________________________________________ Topics * Computable analysis * Complexity on real numbers * Constructive analysis * Domain theory and analysis * Effective descriptive set theory * Theory of representations * Computable numbers, subsets and functions * Randomness and computable measure theory * Models of computability on real numbers * Realizability theory and analysis * Reverse analysis * Real number algorithms * Implementation of exact real number arithmetic Invited Speakers * Hee-Kap Ahn (Pohang, Republic of Korea) * Verónica Becher (Buenos Aires, Argentina) * Anders Hansen (Cambridge, UK) * Takayuki Kihara (Berkeley, USA) * Amaury Pouly (Max Planck Institute, Germany) * Linda Brown Westrick (Connecticut, USA) Scientific Programme Committee * Johanna Franklin (Hempstead, USA) * Daniel Graça, chair (Faro, Portugal) * Vassilios Gregoriades (Turin, Italy) * Peter Hertling (Munich, Germany) * Gyesik Lee (Anseong, Republic of Korea) * Alexander Melnikov (Auckland, New Zealand) * Takako Nemoto (Ishikawa, Japan) * Arno Pauly (Brussells, Belgium) * Cristóbal Rojas (Santiago, Chile) * Frank Stephan (Singapore) * Klaus Weihrauch (Hagen, Germany) Organising Committee * Sunyoung Kim (Yonsei University, Republic of Korea) * Sewon Park (KAIST, Republic of Korea) * Martin Ziegler, chair (KAIST, Republic of Korea) Submissions Authors are invited to submit 1-2 pages abstracts in PDF format, including references via the following web page: https://easychair.org/conferences/?conf=cca2017 If full versions of papers are already available as technical report or arXiv version, then corresponding links should be added to the reference list. Final versions of abstracts might be distributed to participants in hardcopy and/or in electronic form. Dates * Submission deadline: April 3, 2017 * Notification of authors: May 1, 2017 * Final version: May 29, 2017 Conference Web Page http://cca-net.de/cca2017/ A co-located "Workshop on Real Verification" will take place on Friday, July 28, jointly organized by: * Gyesik Lee (Hankyong National University, Republic of Korea) * Martin Ziegler (KAIST, Republic of Korea) https://complexity.kaist.edu/CCA2017/workshop.html

1 0

DICE-FOPARA 2017 - Second Call for Papers
by Nao Hirokawa 10 Feb '17

10 Feb '17

皆様 ETAPS に併設されます DICE-FOPARA 2017 の論文募集案内をお送り致します。投稿締切は2月19日です。ぜひご投稿をご検討下さい。廣川 (JAIST) ------------------------------------------------------------------------------------------- 8th Workshop on Developments in Implicit Computational complExity and 5th Workshop on Foundational and Practical Aspects of Resource Analysis (DICE-FOPARA 2017) Affiliated with ETAPS 2017 April 22 - 23, 2017, Uppsala, Sweden http://cbr.uibk.ac.at/events/dice-fopara ------------------------------------------------------------------------------------------- OBJECTIVES The first joint international workshop on Developments in Implicit Computational complExity and FOundational and Practical Aspects of Resource Analysis (DICE-FOPARA) will be held in Uppsala, Sweden, from April 22-23, 2017 as part of ETAPS. DICE-FOPARA serves as a forum for presenting results relevant to the implicit computational complexity theory *and* to the analysis of resource consumption by computer programs (e.g. time, space, energy). The workshop aims to bring together the researchers that work on foundational issues with the researchers that focus more on practical results. INVITED SPEAKERS Elvira Albert (Complutense University of Madrid) Kerstin I. Eder (University of Bristol) Lars Kristiansen (University of Oslo) Jan Reinecke (Universität Saarland) SUBMISSIONS We ask for submission of *regular papers* describing original work (10-15 pages) or *extended abstracts* (2--6 pages) presenting already published work or work in progress. Regular papers must be prepared using the LaTeX EPTCS class (see http://eptcs.org/). Accepted regular papers will appear in an EPTCS volume. Papers should be submitted electronically via the submission page: https://easychair.org/conferences/?conf=dicefopara2017 IMPORTANT DATES Paper submission February 19, 2017 Notification March 19, 2017 Final versions due March 26, 2017 Workshop date April 22-23, 2017 CONFERENCE VENUE The workshop will be held as a satellite workshop of European Joint Conferences on Theory and Practice of Software 2017 (ETAPS 2017) which takes place in Uppsala, Sweden. PROGRAM COMMITTEE Beniamino Accattoli (Paris) Guillaume Bonfante (Nancy, co-chair) Marko van Eekelen (Nijmegen) Marco Gaboardi (Buffalo) Dan Ghica (Birmingham) Clemens Grelck (Amsterdam) Charles Grellois (Bologna) Nao Hirokawa (JAIST) Jan Hoffmann (CMU) Thomas Jensen (Rennes) Björn Lisper (Mälardalen) Hans-Wolfgang Loidl (Edinburgh) Georg Moser (Innsbruck, co-chair) Kazushige Terui (Kyoto) Simon Wegener (Saarbrücken) Florian Zuleger (Vienna)

1 0

Summer School in Dynamic Epistemic Logic, Sapporo (Japan), 14-25 Aug 2017
by Katsuhiko Sano 07 Feb '17

07 Feb '17

The Department of Philosophy at Hokkaido University (Sapporo, Japan) will hold a two-week summer school in dynamic epistemic logic and its applications, jointly with three guest lecturers from ILLC (University of Amsterdam) from August 14 to August 25 as part of Hokkaido Summer Institute (HSI) 2017. The following two intensive courses are scheduled to be offered during the summer school. Course 1 (August 14 to August 18): Introduction to Logic (For details, see http://hokkaidosummerinstitute.oia.hokudai.ac.jp/courses/CourseDetail=G070) Course 2 (August 21 to August 25): Dynamic Epistemic Logic and its Applications (For details, see http://hokkaidosummerinstitute.oia.hokudai.ac.jp/courses/CourseDetail=G074 ) The main lecturer of Course 1 is Katsuhiko Sano (Department of Philosophy, Hokkaido University). The main lectures of Course 2 are Alexandru Baltag and Sonja Smets (ILLC, University of Amsterdam). There will be a special live on-line lecture by Johan van Benthem (University of Amsterdam, Stanford University, and Tsinghua University) during Course 2. Tomoyuki Yamada and Yasushi Nomura (Hokkaido University) will also join the classes to help students follow the lectures, and communicate with the lecturers. The courses are intended for graduate students. Course 1 is meant for students without prior knowledge of logic and will prepare them for Course 2. Each course is designed to be independent from the other course. Those students who have some familiarity with basics of propositional logic, first order logic, and modal logic can skip Course 1, and those who wish to take only Course 1 can learn basics of logic. Application period for students from universities other than Hokkaido University is from February 1 to February 28 2017. For more details about applications, please check the HSI official website: https://hokkaidosummerinstitute.oia.hokudai.ac.jp/applications/ As the summer in Sapporo is beautiful and pleasant, it's a good idea to learn logic this summer in Sapporo. Tomoyuki Yamada Department of Philosophy Hokkaido University

1 0

早稲田大学江田勝哉先生最終講義
by Toshimichi Usuba 06 Feb '17

06 Feb '17

（このお知らせを重複して受け取られた方はご容赦ください）皆様、早稲田大学の薄葉です。本年3月をもちまして、早稲田大学基幹理工学部数学科江田勝哉先生がご退職されますことに伴い、 3月11日（土）に最終講義が行われることをお知らせいたします。日時：3月11日（土）13時〜14時30分題目：Speckerの定理（双対定理）をめぐって場所：早稲田大学西早稲田キャンパス52号館101教室最終講義に関する問い合わせは薄葉 <usuba(a)waseda.jp> までお願いいたします。皆様のご参加をお待ちしております。 -- Toshimichi USUBA School of Fundamental Science and Engineering, Waseda University

1 0

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml