Logic-ml December 2012

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

15 participants
17 discussions

*** 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 06 Dec '12

06 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 03 Dec '12

03 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 02 Dec '12

02 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

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml December 2012