Logic-ml February 2017

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

8 participants
9 discussions

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

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

04 Feb '17

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

1 0

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

03 Feb '17

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

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml February 2017