Kisoron-ml October 2013

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

6 participants
7 discussions

JAIST Logic Seminar Series
by Hajime Ishihara 26 Oct '13

26 Oct '13

皆様リュブリャナ大学のAndrej Bauer教授の講演のお知らせです。ふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学研究科 e-mail: ishihara(a)jaist.ac.jp -------------------------------------------------- * JAIST Logic Seminar Series * * This seminar is held as a part of the EU FP7 Marie Curie Actions IRSES project COMPUTAL (http://computal.uni-trier.de/). Date: Friday 20 September, 2013, 15:00-17:00 Place: JAIST, Collaboration room 6 (I-57g) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Professor Andrej Bauer (University of Ljubljana, Slovenia) Title: A higher inductive construction of the real numbers Abstract: Homotopy type theory [1] is a foundation of mathematics based on Martin-Löf type theory extended with the Univalence axiom and higher inductive types. The latter allow us to present mathematical objects as inductive types generated by point and path constructors. For instance, the circle is represented by a type with a point and a loop satisfying the "circle induction" principle. In the first part I shall review higher inductive types. In the second part of the talk I shall look at a higher inductive construction of real numbers. Ordinary higher inductive types do not seem to suffice -- instead we have to use a higher inductive-inductive definition which simultaneously constructs the reals and a proximity relation on them. We thus obtain a type of real numbers which satisfies a principle of "real induction". We can prove properties of reals by induction! From a logical point of view the construction is interesting because it avoids the axiom of choice, impredicativity (powersets), and excluded middle. Nevertheless, the resulting theory still allows us to develop the basics of real analysis as usual. The work described in the talk is joint work of the members of the Univalent foundations project [2]. References: [1] Univalent Foundations Project: "Homotopy type theory: Univalent foundations of Mathematics", http://homotopytypetheory.org/book/ [2] Univalent Foundations Project, Institute for Advanced Study, Princeton, http://www.math.ias.edu/sp/univalent -- Professor Hajime Ishihara School of Information Science Japan Advanced Institute of Science and Technology 1-1 Asahidai, Nomi, Ishikawa 923-1292, Japan Tel: +81-761-51-1206 Fax: +81-761-51-1149 ishihara(a)jaist.ac.jp http://www.jaist.ac.jp/~ishihara

1 2

JAIST Logic Seminar Series
by Takako Nemoto 22 Oct '13

22 Oct '13

皆様 JAIST Logic Seminar Seriesのお知らせです。ふるってご参加ください。問合せ先：根元多佳子北陸先端科学技術大学院大学情報科学研究科 e-mail: nemototakako(a)gmail.com ------------------------------ * JAIST Logic Seminar Series * Date: Tuesday 29 October, 2013, 15:30- Place: Collaboration room 6 (I-57g) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Prof. Martin Ziegler (Technische Universitaet Darmstadt) Title: Real Parameterized and Second-Order Complexity Theory: from Computability in Analysis to Numerical Practice Abstract: http://www.jaist.ac.jp/~t-nemoto/Ziegler_talk.pdf

1 0

[お知らせ] キャンパス停電のためのML休止
by Atsushi Igarashi 12 Oct '13

12 Oct '13

logic-ml, kisoron-ml, jssst-ppl 購読のみなさま，管理人の五十嵐です． 10/14(月)に予定されている京大キャンパス内の停電のため， MLを運用しているサーバを 10/12(金) 夕方〜 10/15(火) 午前まで落とします．やや長期間の休止でご不便をおかけいたしますが，よろしくお願いいたします． -- 五十嵐淳 (IGARASHI Atsushi) E-mail: igarashi(a)kuis.kyoto-u.ac.jp url: http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/

1 0

第48回 MLG 数理論理学研究集会のご案内
by Katsuhiko Sano 06 Oct '13

06 Oct '13

第48回 MLG 数理論理学研究集会のご案内 (重複してお受け取りの際はご容赦ください。) 北陸先端科学技術大学院大学の佐野勝彦です。2013年度MLG数理論理学研究集会（第48回）を下記の要領で開催いたします。多くの方のご講演・ご参加をお待ちしております。 ========================================= 第48回 MLG 数理論理学研究集会開催要領 ========================================= 期間: 2013 年 12 月 6 日(金) 〜 12 月 8 日(日) 場所: 山中温泉河鹿荘ロイヤルホテル（JR加賀温泉駅から車で約20分，加賀温泉駅から送迎あり）〒922-0126 石川県加賀市山中温泉河鹿町ホ100 URL : http://www.daiwaresort.jp/kajikasou/ 講演・宿泊申込締め切り: 2013 年 11 月 20 日（水）申し込みはこちらから --> https://docs.google.com/forms/d/1W0cfix5awVjPBI71Bn7dK-LT1E_an2dizQMcoK5LST… ホームページ：https://sites.google.com/site/mlg2013kaga/ 連絡先E-mail :mlg.logic.japan [at] gmail.com ============ 参加募集 ============ ・講演時間は原則40分を予定しています。・12月7日（土）の夜に懇親会を行います。・全日程参加の場合，参加費（宿泊代・食事代・会場代）は25000円前後になる予定です。・ご講演をなさらなくても参加いただけます。山中温泉河鹿荘ロイヤルホテルで宿泊および食事をなさらない場合にも参加費（会場代）2500円をいただきます。・講演申し込みは、https://docs.google.com/forms/d/1W0cfix5awVjPBI71Bn7dK-LT1E_an2dizQMcoK5LSTk/viewform の registration form からお願い致します。世話人佐野勝彦〒923-1292 石川県能美市旭台1-1 北陸先端科学技術大学院大学情報科学研究科 MLG2013に関するメールは，mlg.logic.japan [at] gmail.com まで。 -- Katsuhiko Sano School of Information Science Japan Advanced Institute for Science and Technology IS building No.1 7F, 1-1 Asahidai, Nomi, Ishikawa, 923-1292, Japan

1 0

Dr. Andreas Abel at NII Logic Seminar
by Makoto Tatsuta 04 Oct '13

04 Oct '13

Dr. Andreas Abel at NII Logic Seminar Date: October 11, 2013, 14:00--16:00 Place: National Institute of Informatics, Room 1210 (12th floor) 場所: 国立情報学研究所 12階 1210室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Dr. Andreas Abel (Chalmers and Gothenburg University) Title: Copatterns: Programming Infinite Structures by Observations Abstract: Inductive datatypes provide mechanisms to define finite data such as finite lists and trees via constructors and allow programmers to analyze and manipulate finite data via pattern matching. In this paper, we develop a dual approach for working with infinite data structures such as streams. Infinite data inhabits coinductive datatypes which denote greatest fixpoints. Unlike finite data which is defined by constructors we define infinite data by observations. Dual to pattern matching, a tool for analyzing finite data, we develop the concept of copattern matching, which allows us to synthesize infinite data. This leads to a symmetric language design where pattern matching on finite and infinite data can be mixed. We present a core language for programming with infinite structures by observations together with its operational semantics based on (co)pattern matching and describe coverage of copatterns. Our language naturally supports both call-by-name and call-by-value interpretations and can be seamlessly integrated into existing languages like Haskell and ML. We prove type soundness for our language and sketch how copatterns open new directions for solving problems in the interaction of coinductive and dependent types. This is joint work with Brigitte Pientka, McGill University, Montreal. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

配送回復のおしらせ
by Atsushi Igarashi 02 Oct '13

02 Oct '13

logic-ml, kisoron-ml, jssst-ppl を購読されているみなさま，管理人の五十嵐です．メイリングリストを管理しているソフトウェアが落ちていたことに気付かず， 9月の半ばから二週間程度配送が滞っていたことがわかりました．現在は通常の状態に戻っているのではないかと思います．この間に投稿をされた方におきましては大変ご迷惑をおかけいたしました．どのメイリングリストも毎日必ず投稿があるほどはアクティブではありませんので単に投稿がないのか，不具合が発生しているのか俄かにはわからないことがあります (^^; あれ，投稿が配送されていないかも？と思った場合はお気軽にお問い合わせください．今後ともどうぞよろしくお願いいたします． -- 五十嵐淳 (IGARASHI Atsushi) E-mail: igarashi(a)kuis.kyoto-u.ac.jp url: http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/

1 0

再送：数学基礎論若手の会（11月15日-11月17日）のご案内
by Yoshihito Tanaka 01 Oct '13

01 Oct '13

（重複して受け取られた場合はご容赦ください）再送：数学基礎論若手の会2013のご案内数学基礎論若手の会は，数学基礎論を専攻する学生および若手研究者の研究交流を目的とする合宿形式の研究集会です．講演はオリジナルの成果発表に限らず，研究の途中報告や研究内容の紹介など幅広く募集しています．また，これから数学基礎論を勉強したいと思っている方のご参加も歓迎します．多くの方のご参加・ご講演をお待ちしています．数学基礎論若手の会2013開催要領日時：2013年11月15日（金） - 2013年11月17日（日）講演会場：九州産業大学2号館2E406 宿泊：九州産業大学立花寮1階立花研修所幹事：田中義人（九州産業大学） E-mail：ytanaka(a)ip.kyusan-u.ac.jp 数学基礎論若手の会2013ホームページ： http://www.ip.kyusan-u.ac.jp/J/ms/event/wakate13/notice.html 九州産業大学立花研修所：宿泊料金：1人1泊2415円，1人2泊4725円食事料金：朝食1食250円，夕食1食400円宿泊設備（4人部屋×10室）：2人掛け机2台，椅子4脚，2段ベッド2組　　　　（1人部屋× 3室）：机1台，椅子1脚，ベッド，バス，トイレ共有スペース：シャワー室，トイレ，洗面所，コインランドリー門限 22:30，消灯 23:00 研修所内での飲酒・喫煙はご遠慮願います．退所の際は，宿泊室，シャワー室，トイレ，談話室等の清掃をお願いします． ※ 宿泊や食事を伴わない参加も歓迎します． ※ 親睦会等の会費は別途いただく予定です． ※ 部屋割りに関しては，幹事にご一任ください．参加申し込み：参加をご希望の方は，下記に必要事項をご記載の上，幹事宛に電子メールでお申し込みください．締切：2013年10月27日 ---------------------------------------------------------------- 数学基礎論若手の会参加申し込みフォーム氏名：所属機関：職名/学年：講演について：講演：する / しない講演題目：立花研修所の宿泊・食事について宿泊：要 / 不要宿泊を希望する場合： 15日 / 16日食事：要 / 不要食事を希望する場合： 15日（夕） / 16日（朝・夕） / 17日（朝） ---------------------------------------------------------------- ************************************* Yoshihito Tanaka Faculty of Economics, Kyushu Sangyo University (KSU) 2-3-1 Matsukadai, Higashi-ku, Fukuoka 813-8503, Japan e-mail ytanaka(a)ip.kyusan-u.ac.jp. tel +81-92-673-5216 *************************************

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Kisoron-ml October 2013