Logic-ml July 2016

10 participants
11 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

Call for Participation: ICFP 2016
by Jacques Garrigue 26 Jul '16

26 Jul '16

みなさま、9月に奈良で開催される ICFP 2016 の案内を転送します。早期参加申し込みの〆切は8月17日になっております。 5年ぶりの日本開催で、ご参加をお待ちしています。 ===================================================================== Call for Participation ICFP 2016 21st ACM SIGPLAN International Conference on Functional Programming and affiliated events September 18 - September 24, 2016 Nara, Japan http://conf.researchr.org/home/icfp-2016 ===================================================================== ICFP provides a forum for researchers and developers to hear about the latest work on the design, implementations, principles, and uses of functional programming. The conference covers the entire spectrum of work, from practice to theory, including its peripheries. A full week dedicated to functional programming: 1 conference, 1 symposium, 10 workshops, tutorials, programming contest results, student research competition, and mentoring workshop * Overview and affiliated events: http://conf.researchr.org/home/icfp-2016 * Program: http://conf.researchr.org/program/icfp-2016/program-icfp-2016 * Accepted Papers: http://conf.researchr.org/track/icfp-2016/icfp-2016-papers#event-overview * Registration is available via: https://regmaster4.com/2016conf/ICFP16/register.php Early registration is due 17 August, 2016. * Programming contest, 5-8 August, 2016: http://2016.icfpcontest.org/ * Student Research Competition (deadline: 3 August, 2016): http://conf.researchr.org/info/icfp-2016/student-research-competition * Follow @icfp_conference on twitter for the latest news: http://twitter.com/icfp_conference There are several events affiliated with ICFP: Sunday, September 18 Workshop on Higher-order Programming with Effects Workshop on Type-Driven Development Scheme and Functional Programming Workshop Programming Languages Mentoring Workshop Monday, September 19 – Wednesday, September 21 ICFP Thursday, September 22 Haskell Symposium – Day 1 ML Family Workshop Workshop on Functional High-Performance Computing Commercial Users of Functional Programming – Day 1 Friday, September 23 Haskell Symposium – Day 2 OCaml Workshop Erlang Workshop Commercial Users of Functional Programming – Day 2 Saturday, September 5 Commercial Users of Functional Programming – Day 3 Haskell Implementors Workshop Functional Art, Music, Modeling and Design Conference Organizers General Co-Chairs: Jacques Garrigue, Nagoya University Gabriele Keller, University of New South Wales Program Chair: Eijiro Sumii, Tohoku University Local Arrangements Co-Chairs: Shinya Katsumata, Kyoto University Susumu Nishimura, Kyoto University Industrial Relations Chair: Rian Trinkle, Obsidian Systems LLC Workshop Co-Chairs: Nicolas Wu, University of Bristol Andres Loeh, Well-Typed LLP Programming Contest Chair: Keisuke Nakano, The University of Electro-Communications Student Research Competition Chair: David Van Horn, University of Maryland, College Park Mentoring Workshop Co-Chairs: Amal Ahmed, Northeastern University Robby Findler, Northwestern University Atsushi Igarashi, Kyoto Universty Publicity Chair: Lindsey Kuper, Intel Labs Video Chair: Iavor Diatchki, Galois Jose Calderon, Galois Student Volunteer Co-Chairs: Yosuke Fukuda, Kyoto University Yuki Nishida, Kyoto University Gabriel Scherer, INRIA Industrial partners: Platinum partners Jane Street Capital Ahrefs Gold partners Mozilla Research Silver partners Ambiata Tsuru Capital Bronze partners Awake Networks Microsoft Research =====================================================================

1 0

Glynn Winskel "Formal Semantics of Programming Languages" の翻訳をお手伝いいただける方を探しています
by Kohei SUENAGA 22 Jul '16

22 Jul '16

皆様，京都大学の末永です．メーリングリストをお借りして，教科書の翻訳をお手伝いいただける方を募集させていただければと思います．重複して受け取られた場合はご容赦ください． Glynn Winskel "Formal Semantics of Programming Languages " の翻訳出版の話が来ていて，お手伝いいただける方を探しています． https://www.amazon.com/dp/0262731037 プログラム意味論の世界で一番有名な教科書の一つです．トピックはプログラムの意味を数学を使って厳密に与える様々な方法や，与えた意味論を使ってプログラミング言語の性質を証明する方法です．興味のある方は末永 ksuenaga(a)kuis.kyoto-u.ac.jp までメールをいただければと思います．書誌情報に訳者として名前を載せられるのは数人らしいのですが，お手伝いいただいた方には謝辞などでお名前を出させていただきます．また，些少ながら原稿料も出るようです．どうぞよろしくお願い致します．末永幸平 -- Kohei Suenaga (末永幸平), Ph.D Associate professor (准教授) Graduate School of Informatics, Kyoto University (京都大学情報学研究科) ksuenaga(a)gmail.com http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 20 Jul '16

20 Jul '16

皆様ルートヴィヒ・マクシミリアン大学ミュンヘンのHelmut Schwichtenberg先生の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学系 e-mail: ishihara(a)jaist.ac.jp ----------------------------------------------- * JAIST Logic Seminar Series * * The seminar below 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/) Date: Thursday 25 August, 2016, 13:30-15:10 Place: JAIST, Lecture room I2 (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Helmut Schwichtenberg (Ludwig-Maximilians-Universität München) Title: Invariance axioms for realizability Abstract: Kolmogorov (1932) proposed to consider mathematical formulas as problems asking for solutions. Following this idea it seems reasonable to extend arithmetical theories by adding invariance axioms, which state that every formula is equivalent to the (internal) formula stating that it has a realizer. We sketch such a theory, which in addition allows to fine-tune the computational content of proofs by decorations of the logical connectives. A soundness theorem holds.

1 0

Kobe Colloquium: July 26, 2016, Bakhadyr Khoussainov
by Makoto Kikuchi 20 Jul '16

20 Jul '16

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。 Date: 2016/7/26 (Tue) 3.00pm - 4.30pm Place: Room 421 Speaker: Bakhadyr Khoussainov (Auckland/Kyoto) Title: Algorithmically random infinite structures Abstract: Over the last two decades a significant progress has been made in the study of algorithmic random infinite strings. The main concepts of algorithmic randomness on infinite strings are based on the natural measure on the Cantor space. In spite of much work, research on algorithmic randomness has excluded the investigation of randomness for infinite structures such as graph, trees, algebras. The reason is that it was unclear how one introduces a meaningful measures into these classes of structures that would be pivotal in defining algorithmic randomness. We provide a solution to this problem. We present an axiomatic approach that introduces measure, and hence algorithmic randomness into various classes of structures. We prove the existence of algorithmically random structures with various computability-theoretic properties. We show that any nontrivial variety of algebras has an effective measure 0. This, for instance, implies that no finitely presented algebra in a variety is algorithmically random. We also prove a counter-intuitive result that there are algorithmically random yet computable structures. This establishes a connection between algorithmic randomness and computable model theory. 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/guid/access/rokko/rokkodai-dai2.html 連絡先：菊池誠　mkikuchi(a)kobe-u.ac.jp

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 19 Jul '16

19 Jul '16

皆様インスブリア大学のMarco Benini先生の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学系 e-mail: ishihara(a)jaist.ac.jp ----------------------------------------------- * JAIST Logic Seminar Series * * The seminar below 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/) Date: Monday 8 August, 2016, 13:30-15:10 Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Marco Benini (University of Insubria) Title: Variations on the Higman's Lemma Abstract: The Higman's Lemma says that if A is a well-quasi-order, so is the set of finite sequences over A with the order induced by embedding. By considering the structure of the categories of well-founded quasi-orders and well-quasi-orders, another proof of the Lemma will be derived, along with a number of variants, which may be of some interest.

1 0

Talk by Liang-ting Chen, 19 Tue Jul
by Takumi Akazaki 16 Jul '16

16 Jul '16

Dear colleagues, Dr. Liang-Ting Chen, postdoc. in University of Hawaii at Manoa will visit us next Tuesday. He is working mainly on categorical-algebraic automata theory, and the topic of the talk is Schutzenberger Products. His talk is scheduled on 19 Jul (Tuesday). You're all invited. Thanks, and see you, Takumi Akazaki http://www-mmm.is.s.u-tokyo.ac.jp/seminars.html ----------- Tue 19 July 2016, 13:00–15:00 理学部7号館102 Room 102, School of Science Bldg. No. 7 Liang-Ting Chen <https://de.linkedin.com/in/liang-ting-chen-b5a74988> (Dept. of Info. and Comp. Sci., University of Hawaii), Schutzenberger Products in a Category The Sch\"utzenberger product of monoids is a key tool for the algebraic treatment of language concatenation. In this paper we generalize the Sch\"utzenberger product to the level of monoids in an algebraic category 𝒟, leading to a uniform view of the corresponding constructions for monoids (Sch\"utzenberger), ordered monoids (Pin), idempotent semirings (Kl\'ima and Pol\'ak) and algebras over a field (Reutenauer). In addition, assuming that 𝒟 is part of a Stone-type duality, we derive a characterization of the languages recognized by Sch\"utzenberger products. -- /_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/ 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

Nagoya Set Theory Seminar
by 吉信康夫 12 Jul '16

12 Jul '16

名古屋集合論セミナーのご案内：日時：2016年7月15日(金) 午後3時30分より場所：名古屋大学大学院情報科学研究科2階206号室講演者：渕野昌(神戸大学) 題目：Pre-Hilbert spaces without orthonormal bases 概要：Halmos proved in 1970's that there are pre-Hilbert spaces without orthonormal bases. His example of such pre-Hilbert space was so that its dimension (size of maximal orthonormal system in the space) is strictly less than the density of the space. We show that there are also pre-Hilbert spaces X without orthonormal bases such that dim(X)=d(X). We also show that Shelah Singular Compactness Theorem holds for non-existence of orthonormal bases holds and a natural reflection statement of non-existence of orthonormal bases is equivalent to the Fodor-type Reflection Principle. 多数のご参加をお待ちしております。名古屋大学大学院情報科学研究科吉信康夫

1 0

JAIST Logic Seminar Series (Thursday, 7th July 2016, 15:30-17:00, Ren-June Wang)
by Katsuhiko Sano 05 Jul '16

05 Jul '16

皆様台湾 National Chung Cheng University のRen-June Wangさんの講演会のお知らせです。どうぞふるってご参加ください。問合せ先：佐野勝彦北陸先端科学技術大学院大学情報科学系 e-mail: v-sano(a)jaist.ac.jp ----------------------------------------------------------------- * JAIST Logic Seminar Series * Date: Thursday, 7th July 2016, 15:30-17:00 Place: JAIST, IS school collaboration room 7, 5F (Access: http://www.jaist.ac.jp/english/top/access/index.html) Speaker: Ren-June Wang (Department of Philosophy, National Chung Cheng University) Title: Logical Omniscience and Deductive Rationality Abstract: Epistemic logic as an important tool for reasoning about an intellectual agent’s epistemic states has long suffered from the so-called logical omniscience problem since the beginning of its introduction. The problem indicates an idealized assumption on the part of the agent presented by a formalism of such kind. Although alternative epistemic formalisms have been proposed for dealing with the problem, there is no sight of that the problem is settled. Thus in this talk I will try my hand firstly to give an analysis of the problem, hopefully to pin down the source of the problem, and accordingly provide an advice as to what is the right direction of solving the problem. At the end of the talk I will suggest that what we need is not a formalism with a machinery that can limit what is known by the agent, but one with more powerful expressivity such that the resource that an agent will consume in the course of his/her reasoning, such as the temporal duration, can be explicitly stated. -- Katsuhiko Sano School of Information Science Japan Advanced Institute of Science and Technology IS building No.1 7F, 1-1 Asahidai, Nomi, Ishikawa, 923-1292, Japan

2 1

[TACL 2017] First announcement
by 小野寛晰 04 Jul '16

04 Jul '16

[Apologies for multiple copies] ======================================================= TOPOLOGY, ALGEBRA AND CATEGORIES IN LOGIC (TACL 2017) ======================================================= Conference: June 26 -- 30, 2017 (Prague) School: June 20 -- 24, 2017 (Olomouc) http://www.cs.cas.cz/tacl2017 <http://www.cs.cas.cz/tacl2017> The Eighth International Conference on Topology, Algebra and Categories in Logic organized by Institute of Computer Science, Czech Academy of Sciences Faculty of Arts, Charles University in Prague & & & & & & & & & & & & & & & & & & & & & & & The Third Summer School organized by Faculty of Science, Palacký University Olomouc Studying logics via semantics is a well-established and very active branch of mathematical logic, with many applications, in computer science and elsewhere. The area is characterized by results, tools and techniques stemming from various fields, including universal algebra, topology, category theory, order, and model theory. The programme of the conference TACL 2017 will focus on three interconnecting mathematical themes central to the semantical study of logics and their applications: algebraic, categorical, and topological methods. This is the eighth conference in the series Topology, Algebra and Categories in Logic (TACL, formerly TANCL). Earlier instalments of this conference have been organized in Tbilisi (2003), Barcelona (2005), Oxford (2007), Amsterdam (2009), Marseille (2011), Nashville (2013) and Ischia (2015). Starting from 2013, the conference is preceded by a summer school. Featured topics ------------------ Contributed talks can be on with any topic involving the use of algebraic, categorical or topological methods in either logic or computer science. This includes, but is not limited to, the following areas: * Algebraic structures in CS * Algebraic logic * Coalgebra * Categorical methods in logic * Domain theory * Lattice theory * Lattices with operators * Many-valued and fuzzy logics * Modal logics * Non-classical logics * Ordered topological spaces * Ordered algebraic structures * Pointfree topology * Proofs and Types * Residuated structures * Semantics * Stone-type dualities * Substructural logics * Topological semantics of modal logic Venues ------ The conference will be held at the campus of the Faculty of Arts, Charles University in Prague. The school will be held at the campus of the Faculty of Science, Palacký University Olomouc. (The two cities are two hours train trip apart.) Important dates ----------------- June 20 - June 24, 2017: School (Olomouc) June 26 - June 30, 2017: Conference (Prague) Programme Committee Chairs -------------------------- John Harding, New Mexico State University Rosalie Iemhoff, Utrecht University Steering Committee -------------------- Guram Bezhanishvili, New Mexico State University Mai Gehrke, University of Paris Diderot Rob Goldblatt, Victoria University, Wellington Ramón Jansana, University of Barcelona Achim Jung, University of Birmingham Hiroakira Ono, Japan Advanced Institute of Science and Technology Yde Venema, University of Amsterdam Michael Zakharyaschev, University of London Organizing Committees --------------------- Conference: Marta Bílková (chair), Faculty of Arts, Charles University in Prague Petr Cintula (chair), Institute of Computer Science, CAS Zuzana Haniková Rostislav Horčík Tomáš Lávička Ondrej Majer Tommaso Moraschini Carles Noguera Adam Přenosil Igor Sedlár Amanda Vidal Wandelmer School: Radomír Halaš (chair), Faculty of Science, Palacký University Olomouc Martin Broušek Jan Kuhr More Information ---------------- TACL 2017 web site: http://www.cs.cas.cz/tacl2017 <http://www.cs.cas.cz/tacl2017> Conference email: tacl2017(a)cs.cas.cz <mailto:[email protected]> School email: school2017(a)upol.cz <mailto:[email protected]>

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml July 2016