Logic-ml June 2016

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

6 participants
8 discussions

homotopy type theory
by logic＠math.tsukuba.ac.jp 30 Oct '16

30 Oct '16

> 圏論に関して質問があります。 > 種々の圏の存在はどのようにして主張されますか？ > > 例えば、公理的集合論では、論理式f(x),集合Xに関して、Xの元xでf(x)を満たすもの > から成る集合{x \in X|f(x)}が存在することが分出公理によって言えますが、圏論に > おいても、圏の存在を主張する公理群が定められていますか？ > 上記のような質問をいただいていますが、これはこの質問者以外の広い範囲の方に関心があることと思われますので、ここにお答えします。質問者の名前等は削除してあります。まず質問を Homotopy type theoryはZFCにかわる数学の基礎づけになるという話であるが、集合論はたとえばComprehensionのような豊かな構成原理をもっているが、HTTはどうなのか？と変形させていただきます。まずHTTのなかではn-typeというHierarchyが定義されます。ｎは−２以上の整数です。これはHomotopy theoryから借用された概念で、n-typeというのはｎを越える次元ではhomotopicalにはtrivialであることを意味します。Homotopy theoryの言葉づかいで言うならば、ｎを越える次元のhomotopy groupsはすべてtrivialであることを意味します。０-typeがいわゆるsetで、ここに話を限定するならば comprehensionをはじめとする集合論的構成はだいたいそのまま行えます。一般にはdependent function typeやdependent pair typeという構成原理を最初から内臓していますが、これだけではもちろん足りません。HTTがもつ強力な構成原理はinductionで、特に higher inductionが重要な役割を演じます。計算機言語のCOQや AGDAは通常にinductionを組み込んでいますが、higher inductive typesはまだ持っておりません。少しslogan的な言い方を許していただければ、 inductive typesはfree monadsに、higher inductive typesはmonadsの表現に対応します。 Inductiveな構成のいい例はCauchy realsの構成です。自然数から有理数を作るのは、古典的な話とあまりかわりません。それで有理数から実数を作るには、Dedekindのやり方とCauchyのやり方がありますが、後者の構成をinductiveにやるとどうなるかが、 https://homotopytypetheory.org/book/ の１１．３節に縷説されています。あるいはcirclesやspheresやsuspensionsはどのようにinductiveに構成されるか、第６章に縷説されています。是非ご覧になってください。にしむら筑波大学数学追伸：オマケです。手持無沙汰な折にどうぞ。 https://www.youtube.com/watch?v=VY01dVHvlFE

2 2

JAIST Logic Seminar Series
by Hajime Ishihara 28 Jun '16

28 Jun '16

皆様ジェノヴァ大学のEugenio Moggi先生の特別集中講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学系 e-mail: ishihara(a)jaist.ac.jp ----------------------------------------------- * JAIST Logic Seminar Series * * This series of lectures is held as a part of JSPS Core-to-Core Program, A. Advanced Research Networks, and EU FP7 Marie Curie Actions IRSES project CORCON. (http://www.jaist.ac.jp/logic/ja/core2core, https://corcon.net/) Dates: Tuesday 2 August, 2016, 13:30-15:10 Thursday 4 August, 2016, 13:30-15:10 Friday 5 August, 2016, 10:50-12:30 Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Eugenio Moggi (University of Genova) *Tuesday 2 August, 2016, 13:30-15:10* LECTURE 1: Categories of Classes for Collection Types ABSTRACT. Collection types have been proposed by Buneman and others (in the '90) as a way to capture database query languages in a typed setting. In 1998 Manes introduced the notion of collection monad on the category S of sets as a suitable semantics for collection types. The canonical example of collection monad is the finite powerset monad Pf. In order to account for the algorithmic aspects of database languages, the category S is unsuitable, and should be replaced with other categories, whose arrows are maps computable by "low complexity" algorithms. We propose "realizability for DSL" (Domain Specific Languages), where the starting point is a monoid C of endomaps on a set D, instead of a combinatory algebra on D, as a way to get such categories by constructions like the category A[C] of "assemblies". To get Pf in a systematic way we borrow ideas from AST (Algebraic Set Theory, started by Joyal and Moerdijk in the '90), where they fix a notion of "small" map in a category of "classes", and read "small" as "finite". *Thursday 4 August, 2016, 13:30-15:10* LECTURE 2: Hybrid System Trajectories as Partial Continuous Maps ABSTRACT. Hybrid systems (HS) are dynamic systems that exhibit both continuous and discrete dynamic behavior: they can flow (according to a differential equation) and jump (according to a transition relation). HS can be used for modeling rigid body dynamics with impacts, and more generally Cyber-Physical Systems. HS can exhibit Zeno behaviors, that arise naturally in rigid body dynamics with impacts, but are absent from purely discrete or purely continuous systems. Dealing properly with these behaviors is a prerequisite to give sound definitions of concepts such as reachability. We propose the use of partial continuous maps (PCM) as trajectories that describe how a HS evolves over time. PCMs enable a notion of trajectory that can go beyond Zeno points. *Friday 5 August, 2016, 10:50-12:30* LECTURE 3: Models, Over-approximations and Robustness ABSTRACT. Hybrid systems, and related formalisms, have been successfully used to model Cyber- Physical Systems. The usual definition of "reachability", in terms of the reflexive and transitive closure of a transition relation, is unsound for Zeno systems. We propose "safe reachability", which gives an over-approximation of the set of states that are "reachable in finite time" from a set of initial states. Moreover, mathematical models are always a simplification of the system they are meant to describe, and one must be aware of this mismatch, when using these models for system analyses. In safety analysis it is acceptable to use over-approximations of the system behavior, indeed they are the bread and butter of counterexample guided abstraction refinement (CEGAR). We propose a notion of safe (time-bounded) reachability, which is also robust wrt arbitrary small overapproximations, and argue that it is particularly appropriate for safety analysis.

1 0

CFP: PEPM 2017
by Ryosuke SATO 27 Jun '16

27 Jun '16

皆様、（複数受け取られた場合はご容赦ください。）東京大学の佐藤亮介です。来年1月に POPL 併設で開催される PEPM 2017 の CFP をお送りいたします。日程は次の通りです。 * Abstract submission: Tue, 13 Sep, 2016 * Paper submission: Fri, 16 Sep, 2016 * Author notification: Mon, 24 Oct, 2016 * Camera ready: Mon, 28 Nov, 2016 レギュラー論文の他に、ショート論文、ポスターも受け付けております。是非，投稿をご検討ください。 -- 東京大学大学院情報理工学系研究科佐藤亮介 ryosuke(a)kb.is.s.u-tokyo.ac.jp ------------------------------------------------------------------- CALL FOR PAPERS Workshop on Partial Evaluation and Program Manipulation (PEPM 2017) Paris, France, January 16th – 17th, 2017 http://conf.researchr.org/home/PEPM-2017 PEPM 2017 in Paris, co-located with POPL 2017. The PEPM Symposium/Workshop series aims at bringing together researchers and practitioners working in the areas of program manipulation, partial evaluation, and program generation. PEPM focuses on techniques, theory, tools, and applications of analysis and manipulation of programs. PEPM 2017 will be based on a broad interpretation of semantics-based program manipulation, reflecting the expanded scope of PEPM in recent years beyond the traditionally covered areas of partial evaluation and specialization. Specifically, PEPM 2017 will include practical applications of program transformations such as refactoring tools, and practical implementation techniques such as rule-based transformation systems. In addition, the scope of PEPM covers manipulation and transformations of program and system representations such as structural and semantic models that occur in the context of model-driven development. In order to maintain the dynamic and interactive nature of PEPM and to encourage participation by practitioners, we also solicit submissions of short papers, including tool demonstrations, and of posters. SCOPE Topics of interest for PEPM 2017 include, but are not limited to: * Program and model manipulation techniques such as: supercompilation, partial evaluation, fusion, on-the-fly program adaptation, active libraries, program inversion, slicing, symbolic execution, refactoring, decompilation, and obfuscation. * Program analysis techniques that are used to drive program/model manipulation such as: abstract interpretation, termination checking, binding-time analysis, constraint solving, type systems, automated testing and test case generation. * Techniques that treat programs/models as data objects including metaprogramming, generative programming, embedded domain-specific languages, program synthesis by sketching and inductive programming, staged computation, and model-driven program generation and transformation. * Application of the above techniques including case studies of program manipulation in real-world (industrial, open-source) projects and software development processes, descriptions of robust tools capable of effectively handling realistic applications, benchmarking. Examples of application domains include legacy program understanding and transformation, DSL implementations, visual languages and end-user programming, scientific computing, middleware frameworks and infrastructure needed for distributed and web-based applications, embedded and resource-limited computation, and security. This list of categories is not exhaustive, and we encourage submissions describing applications of semantics-based program manipulation techniques in new domains. If you have a question as to whether a potential submission is within the scope of the workshop, please contact the programme chairs. SUBMISSION CATEGORIES AND GUIDELINES Three kinds of submissions will be accepted: Regular Research Papers, Short Papers and Posters. * Regular Research Papers should describe new results, and will be judged on originality, correctness, significance and clarity. Regular research papers must not exceed 12 pages in ACM Proceedings style (including appendix). * Short Papers may include tool demonstrations and presentations of exciting if not fully polished research, and of interesting academic, industrial and open-source applications that are new or unfamiliar. Short papers must not exceed 6 pages in ACM Proceedings style (including appendix). * Posters should describe work relevant to the PEPM community, and must not exceed 2 pages in ACM Proceedings style. We invite poster submissions that present early work not yet ready for submission to a conference or journal, identify new research problems, showcase tools and technologies developed by the author(s), or describe student research projects. At least one author of each accepted contribution must attend the workshop and present the work. In the case of tool demonstration papers, a live demonstration of the described tool is expected. Suggested topics, evaluation criteria, and writing guidelines for both research tool demonstration papers will be made available on the PEPM 2017 web site. Student participants with accepted papers can apply for a SIGPLAN PAC grant to help cover travel expenses and other support. PAC also offers other support, such as for child-care expenses during the meeting or for travel costs for companions of SIGPLAN members with physical disabilities, as well as for travel from locations outside of North America and Europe. For details on the PAC programme, see its web page. PUBLICATION AND SPECIAL ISSUE All accepted papers, short papers and posters included, will appear in formal proceedings published by ACM Press. Accepted papers will be included in the ACM Digital Library. Authors of selected papers from PEPM 2016 and PEPM 2017 will also be invited to expand their papers for publication in a special issue of the journal Computer Languages, Systems and Structures (COMLAN, Elsevier). BEST PAPER AWARD PEPM 2017 continues the tradition of a Best Paper award. The winner will be announced at the workshop. IMPORTANT DATES Abstract submission: Tue, 13 Sep, 2016 Paper submission: Fri, 16 Sep, 2016 Author notification: Mon, 24 Oct, 2016 Camera ready: Mon, 28 Nov, 2016 INVITED SPEAKERS to be announced PROGRAM CHAIRS Jeremy Yallop (University of Cambridge) Ulrik Pagh Schultz (Unversity of Southern Denmark) PROGRAM COMMITTEE to be announced

1 0

第二十七回 ALGI（代数，論理，幾何と情報科学研究集会）の講演募集の再アナウンス
by 西澤弘毅 23 Jun '16

23 Jun '16

logic-mlメーリングリストの皆様，神奈川大学の西澤弘毅と申します。第二十七回 ALGI（代数，論理，幾何と情報科学研究集会）の開催と講演募集の再アナウンスをさせていただきます。 < 重複してお受け取りの節はご容赦願います。> 下記にも記しましたが、二日目には、代数トポロジーに関する１時間程度の特別講演を信州大学理学部の玉木大先生にお願いしております。ご参加をお待ちしております。 --------------------------------------------------------------------- **************************************************************** * 第二十七回 ALGI（代数，論理，幾何と情報科学研究集会） * * * * 2016年8月27日（土）午後～8月28日（日） * * 信州大学松本キャンパス人文学部・経法学部新棟1階第1講義室 * * * * 開催のお知らせと講演の募集 * **************************************************************** ALGI (Algebra, Logic, Geometry and Informatics) は、代数学や論理学、幾何学の情報科学への応用について、および情報科学の代数学や論理学、幾何学への応用についての研究集会で、年一回の頻度で開催されています。 ALGIの趣旨や過去の集会の情報がウェブページ http://sakura.imi.kyushu-u.ac.jp/algi/ にありますので、参考までに御覧ください。このたび、第二十七回ALGIを開催することになりました。会場の手配などは信州大学の田中康平先生にお願いしています。開催場所は下記のとおりです。信州大学松本キャンパス人文学部・経法学部新棟1階第1講義室 http://www.shinshu-u.ac.jp/guidance/maps/map05.html http://www.shinshu-u.ac.jp/general/extension-courses/pdf/map01-02.pdf 講演を希望される方は、・題目・講演者名・e-mail address ・所属・梗概・希望時間・講演に必要な道具などの情報を nishizawa(a)kanagawa-u.ac.jp までお寄せください。「講演したいと思っている」程度の不完全情報でも結構です。時間の空きがある限り、開催直前まで講演申込を受け付けるつもりですが、申込順に発表時間を割り当てていきますので、講演をお考えの方は、なるべくお早めにお知らせいただけますようにお願い致します。初日は午後から開催いたします。夕方には松本駅周辺で懇親会を計画しています。二日目には、代数トポロジーに関する１時間程度の特別講演を信州大学理学部の玉木大先生にお願いしております。また、今回のALGIの前後には次のような集会も予定されています。併せて参加をご検討下さい。 2016年度 SLACS(記号論理と情報科学研究集会) 日時：2016年8月25日(木),26日(金) 会場：名古屋大学VBL(ベンチャービジネスラボラトリー)3階ベンチャーホール詳細：http://www.seto.nanzan-u.ac.jp/~sasaki/SLACS2016.html 「空間の代数的・幾何的モデルとその周辺」日時：2016年8月29日（月）午後 ? 8月31日（水）午前会場：信州大学理学部講義棟第一講義室詳細：決まり次第アナウンス予定 ALGIは申し込み不要で自由にご参加いただけます。ただし懇親会については事前に詳細を告知し参加申し込みを受け付けます。できるだけ多くの皆さんのご講演・ご参加をお待ちしております。西澤弘毅（神奈川大学工学部）古澤仁（鹿児島大学大学院理工学研究科） ----------------------------------------------------------- -- 西澤弘毅神奈川大学工学部情報システム創成学科〒221-8686 神奈川県横浜市神奈川区六角橋3-27-1 nishizawa(a)kanagawa-u.ac.jp TEL（代表）045-481-5661 （内線：3378）

1 0

IWC 2016 - 2nd Call for Papers
by Nao Hirokawa 14 Jun '16

14 Jun '16

皆様 9月にオーストリアで開催されます「合流性に関するワークショップ IWC 2016」の二回目の論文募集をご案内致します。 - 開催日が 9月8日〜9日に決定致しました。 - 招待講演者は Florent Jacquemard 氏 (INRIA) と Paul-Andre Mellies 氏です。ぜひ投稿・参加をご検討下さい。廣川 (JAIST) ============================================================== Second Call for Papers IWC 2016 5th International Workshop on Confluence Sep 8-9, 2016, Obergurgl, Austria, Part of Computational Logic in the Alps CLA 2016 http://www.csl.sri.com/~tiwari/iwc2016/ ============================================================== Confluence provides a general notion of determinism and is widely viewed as one of the central properties of rewriting. Confluence relates to many topics of rewriting (completion, modularity, termination, commutation, etc.) and had been investigated in many formalisms of rewriting such as first-order rewriting, lambda-calculi, higher-order rewriting, constrained rewriting, conditional rewriting, etc. Recently there is a renewed interest in confluence research, resulting in new techniques, tool support, certification as well as new applications. The International Workshop on Confluence (IWC) aims at promoting further research in confluence and related properties. IWC 2016 is part of the Computational Logic in the Alpsevent to be held in Obergurgl, Austria, during the week Sep 4-10, 2016. Previous editions of the workshop were held in Nagoya (2012), Eindhoven (2013), Vienna (2014), and Berlin (2015). During the workshop, the 5th Confluence Competition (CoCo 2016) takes place. IMPORTANT DATES: * submission June 22, 2016 * notification July 12, 2016 * final version Aug 03, 2016 * workshop Sep 4-10, 2016 TOPICS: Specific topics of interest include: * confluence and related properties (unique normal forms, commutation, ground confluence) * completion * critical pair criteria * decidability issues * complexity issues * system descriptions * certification * applications of confluence INVITED SPEAKERS: * Florent Jacquemard (INRIA) * Paul-Andre Mellies (CNRS & Paris Diderot University) PROGRAM COMMITTEE: * Beniamino Accattoli (INRIA) * Bertram Felgenhauer (University of Innsbruck) * Yves Guiraud (INRIA & Paris Diderot University) * Nao Hirokawa (JAIST) * Koji Nakazawa (Nagoya) * Ashish Tiwari (Menlo Park) SUBMISSION: We solicit short papers or extended abstracts of at most five pages. There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers submitted elsewhere. The program committee checks relevance and may provide additional feedback. The accepted papers will be made available electronically before the workshop. The page limit for papers is 5 pages in EasyChair style. Short papers or extended abstracts must be submitted electronically through the EasyChair system at: https://www.easychair.org/conferences/?conf=iwc2016

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 08 Jun '16

08 Jun '16

皆様オークランド大学のBakhadyr Khoussainov先生の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学系 e-mail: ishihara(a)jaist.ac.jp ----------------------------------------------- * JAIST Logic Seminar Series * Date: Monday 20 June, 2016, 15:20-17:00 Place:JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Bakhadyr Khoussainov (University of Auckland) Title: Computably Enumerable Structures: Domain dependency Abstract: Computably enumerable structures arise naturally in algebra and computer science. In algebra examples include finitely presented universal algebras such as finitely presented groups. In computer science, these are abstract data types defined by equational or quasi-equational specifications. The domains of these algebraic structures are quotient sets of the form $\omega/E$, where $\omega$ is the set of natural numbers and $E$ is a computably enumerable (c.e.) equivalence relations. We consider c.e. structures whose domains are of the form $\omega/E$ and study various properties of these structures and their dependence on the domain $\omega/E$

1 0

Talk by Sato Tetsuya, 14 Tue Jun
by Takumi Akazaki 08 Jun '16

08 Jun '16

皆様、(重複して受け取られた方はご容赦ください) 東京大学蓮尾研の赤崎と申します。以下の要領で、来週の火曜日に、京大数理研の佐藤哲也さんをお招きして講演をしていただきます。ぜひご参加くださいませ。日時: 6月14日 13:00-15:00 場所: 東京大学理学部7号館102教室 --------- Tue 14 June 2016, 13:00–15:00 理学部7号館102 Room 102, School of Science Bldg. No. 7 Tetsuya Sato <http://www.kurims.kyoto-u.ac.jp/~satoutet/> (RIMS, Kyoto University), 差分プライバシーの圏論的特徴づけと、その検証差分プライバシー[Dwork, ICALP 2006]は、確率的プログラムで与えられたデータベース・クエリーに関するプライバシー保護の定義／基準で、背景知識攻撃に対する安全性を数学的に保証するという特長を持ち、近年でも盛んに研究されている。 Bartheによる Approximate Relational Hoare Logic (apRHL) [Barthe et al., POPL 2012]は、クエリーの差分プライバシーを形式的に検証するための枠組みで、差分プライバシーの概念を、圏Set上の確率分布モナドのパラメトリックな二項関係持ち上げによって与えるというアイデアに基づいて構成されている。本講演で紹介する Continuous apRHL はapRHLの測度論的拡張と呼ぶべきもので、連続分布型の確率的プログラムであるクエリーの差分プライバシーの検証を可能とする。構成はまず、クエリーの差分プライバシーを、Giryモナドのgradedな二項関係持ち上げによって特徴づけ、それらでjudgementの解釈を与え直すことでapRHLを拡張するという流れである。[Sato, MFPS 2016] 可能であれば、これからの発展などについてもお話ししたい。 -- /_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/ Dept. of Computer Science Graduate School of Information Science and Technology The University of Tokyo Akazaki Takumi mail :<ultraredrays(a)gmail.com> mobile : <090-5379-4901> /_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/

1 0

Talk by Bakhadyr Khoussainov (* 7 Jun 11:00- *)
by Tetsuya Sato 02 Jun '16

02 Jun '16

京都大学数理解析研究所の佐藤です。来週の *火曜日*、6月7日11:00から、オークランド大学のBakhadyr Khoussainov先生に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 7 Jun, 2016 Place: Rm 478, Research Building 2, Main Campus, Kyoto University 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speaker: Bakhadyr Khoussainov (University of Auckland) Title: Open questions in the theory of automatic structures. Abstract: In this talk, we introduce the notion of automatic structure (defined by the speaker and Nerode). Informally, these are infinite algebraic structures (such as graphs, trees, groups, linear orders) that can be presented by automata. We present many examples, several basic results, formulate and discuss some open questions in the area.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml June 2016