Kisoron-ml

1 participants
589 discussions

ラムダ計算と論理の早春セミナー3/12--3/16
by Fujita Kenetsu 22 Feb '13

22 Feb '13

『ラムダ計算と論理の早春セミナー』のご案内日程：2013年3月12日(火) 午後5時から3月16日(土) 正午まで場所：国立大学草津セミナーハウス　　　〒377-1711 群馬県吾妻郡草津町大字草津字白根737 詳細：http://komoriyuichi.web.fc2.com/symposium/KusatsuSeminar2008/2013/ 興味をお持ちのみなさまのご参加をお待ちしております． ----------- 群馬大学　藤田憲悦

1 0

Prof. Helmut Schwichtenberg Lecture at NII Logic Seminar
by Makoto Tatsuta 08 Feb '13

08 Feb '13

Prof. Helmut Schwichtenberg Lecture at NII Logic Seminar Date: February 21, 2013, 14:00--16:00 Place: National Institute of Informatics, Lecture Room 1208 (12th floor) 場所: 国立情報学研究所 12階 1208室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Helmut Schwichtenberg (Ludwig Maximilian University of Munich) Title: Proofs and computations with infinite data Abstract: Ulrich Berger and Monika Seisenberger recently studied extraction from proofs involving (only) abstract reals. They considered a proof using coinduction of the proposition that any two reals in [-1,1] have their average in the same interval, and informally extract a Haskell program working with stream representations of reals. We report on a formalization of this proof, and a machine-extraction of its computational content, in the Minlog proof assistant. This required an extension of this system to also take coinduction into account. The underlying formal system is a theory TCF of computable functionals. It is similar to Heyting arithmetic in all finite types, but with the Scott/Ershov partial continuous functionals as the domain of quantifiers. TCF has free type, predicate and function variables, to allow for abstract developments (groups, fields, real analysis). The underlying inference machinery is minimal logic (implication, universal quantification plus inductively and coinductively defined predicates). Computable functionals (of finite type, with free algebras at ground types) are given by their defining equations. Since the logic is constructive, program extraction by means of a realizability interpretation is possible and a soundness theorem holds. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

Dr. Sam Sanders Lecture at NII Logic Seminar
by Makoto Tatsuta 08 Feb '13

08 Feb '13

Dr. Sam Sanders Lecture at NII Logic Seminar Date: February 13, 2013, 13:30--15:30 Place: National Institute of Informatics, Lecture Room 1904 (19th floor) 場所: 国立情報学研究所 19階 1904室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Dr. Sam Sanders (University of Ghent) Title: Reuniting the antipodes: Bringing together Nonstandard Analysis and Constructive Analysis Abstract: Constructive Analysis (aka BISH) was introduced by Errett Bishop as a redevelopment of Mathematics with a focus on computational content. As such, BISH is based on the BHK (Brouwer-Heyting-Kolmogorov) interpretation of logic, where the notions of `proof' and `algorithm' are central. Constructive Reverse Mathematics (CRM) is a spin-off from Harvey Friedman's `Reverse Mathematics' program where the base theory is based on BISH. In this talk, we introduce an interpretation of BISH in classical Nonstandard Analysis. The role of `proof' in this interpretation is played by the Transfer Principle of Nonstandard Analysis. The role of `algorithm' is played by `$\Omega$-invariance'. Intuitively, an object is $\Omega$-invariant if it does not depend on the *choice* of infinitesimal used in its definition. Using this new interpretation, we obtain many of the well-known results form CRM. In particular, all non-constructive principles (like LPO, LLPO, MP, etc) are interpreted as Transfer Principles, which are not available in our nonstandard base theory. Finally, the interpretation preserves the property that not all $\Delta_1$-formulas are decidable in BISH. We discuss applications in (Homotopy) Type Theory. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp

1 0

Prof. Yue Yang Lecture at NII Logic Seminar
by Makoto Tatsuta 08 Feb '13

08 Feb '13

Prof. Yue Yang Lecture at NII Logic Seminar Date: February 12, 2013, 14:00--16:00 Place: National Institute of Informatics, Lecture Room 1210 (12th floor) 場所: 国立情報学研究所 12階 1210室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Yue Yang (National University of Singapore) Title: The strength of Ramsey Theorem for Pairs Abstract: Ramsey Theorem is a well-known theorem in combinatorics. However, a special weak form of it (Ramsey Theorem for Pairs) has been a hot topic in Recursion Theory and Reverse Mathematics. In this talk I will give a survey on some recent progresses related to combinatoric principles weaker than Ramsey's Theorem for Pairs. In particular, I will speak about some results obtained by Chitat Chong, Ted Slaman and me on the first order and second order arithmetical consequences of Ramsey Theorem for Pairs. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

仙台ロジックスクール
by Tanaka Kazuyuki 05 Feb '13

05 Feb '13

仙台ロジックスクール SLS2013 （日本ベルギー合同勉強会）すでにご案内申し上げておりますCTFM研究集会(２月１８日〜２１日，東工大) http://sendailogic.math.tohoku.ac.jp/CTFM/ のサテライトとして，仙台にて学生・若手のための勉強会を下記の通り行います。【日程】　２月２２日（金）・２３日（土）9:00 開場【場所】　仙台国際センター　小会議室８【講師】　S. Simpson，Yang Yue，Wu Guohua 　　　　　照井一成，宮部賢志，秋吉亮太（敬称略） ※詳細は，下記ウェブ・ページをご覧ください。 http://sendailogic.math.tohoku.ac.jp/SLS/ 　――――――――――――――――――――――― 参加費は無料ですが，会場準備の都合上，参加される方は事前申し込みをお願いします。【申し込み期限】　2月11日（祝）【申し込み・問い合わせ先】　sendailogic(a)gmail.com 　(担当：朴) 下の申込書をカット＆ペーストして必要事項を記入のうえ，上のアドレス（朴）までお送りください。２２日の夜に懇親会（参加費３千円程度）を予定しておりますので、出欠を併せてお知らせください。 ※　宿泊については，近くのホテルの部屋をいくつかおさえてありますので，必要な方はお問い合わせください。幹事：田中一之，山崎武（東北大学・理学研究科）　――――――――――――――――――――――― 仙台ロジックスクール SLS2013　申込書　お名前　所属・身分　ご連絡先　講演会参加　　22日（　）　23日（　）　懇親会参加　　22日（　）　―――――――――――――――――――――――

1 0

重要なご連絡ーアブストラクトの公開について（訂正）
by Masahiro Kumabe 02 Feb '13

02 Feb '13

皆様複数受け取られた場合はご容赦ください。こんにちは。日本数学会の数学基礎論及び歴史分科会の連絡評議委員の隈部です。先日、学会発表におけるアブストラクトの公開についてのご連絡を、メールにてお知らせしましたが、訂正があります。重要な内容ですので、是非ご一読お願い致します。＊学会における一般講演のアブストラクトについて２０１３年度年会から、数学会として、一般講演のアブストラクトをPDFファイルとして、学会開催前に、数学会のホームペジにて公開することをご連絡しましたが、これは、数学基礎論及び歴史分科会においては、学会会員内だけの公開です。昨年９月の分科会総会でそのように決まっていました。ここにお詫びして訂正致します。申し訳ありませんでした。従いまして、学会会員でない方は、アブストラクトの冊子を学会会場で購入してご覧になれます。以上の件、お間違いのないようにご理解ください。隈部

1 0

Eighth NII Type Theory Workshop
by Makoto Tatsuta 01 Feb '13

01 Feb '13

Eighth NII Type Theory Workshop Date: February 6, 2013, 10:40--16:50 Place: National Institute of Informatics, Room 1904 (19th floor) 場所: 国立情報学研究所 19階 1904室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Program: 10:40--11:20 Toshihiko Uchida (The Graduate University for Advanced Studies) Title: A Partial Translation from lambda U to lambda 2 11:20--12:00 Daisuke Kimura (National Institute of Informatics) Title: Linear Pure Type Systems 12:00--14:00 Lunch Break 14:00--14:40 Kazuyuki ASADA (National Institute of Informatics) Title: Curry-Howard Correspondence between Dialectica Interpretation and Bidirectional Transformation 14:40--15:20 Makoto Tatsuta (National Institute of Informatics) Title: Dual Calculus with Inductive and Coinductive Types 15:20--15:50 Tea Break 15:50--16:50 Stefano Berardi (Torino University) Title: A Curry-Howard result for various subclassical logics Abstracts: ---------------------------------------------------------------------- Toshihiko Uchida (The Graduate University for Advanced Studies) Title: A Partial Translation from lambda U to lambda 2 Abstract: Girard showed that every type of sort * (i.e., proposition) is inhabited in lambda U. Barendregt state without proof that every type of sort Box (i.e., domain) is also inhabited in the system. In this talk, we show that the second statement is not the case by giving a partial translation from lambda U to lambda 2. ---------------------------------------------------------------------- Daisuke Kimura (National Institute of Informatics) Title: Linear Pure Type Systems Abstract: This talk proposes a linear variant of Pure Type Systems (PTSs), called linear pure type systems (LPTSs). It is a general framework, which provides a uniform way to treat various linear type systems that have the features of linear logic. We first introduce a subframework of LPTSs, called multiplicative linear pure type systems (MLPTSs), in which only variables that linearly occur are abstracted. All MLPTSs are consistent and satisfy strong normalization. However their expressive power is rather weak. We then give LPTSs by extending MLPTSs with exponentials. Each PTS can be embedded into a LPTS. We also show the equivalence of strong normalizability of PTSs and LPTSs by giving mutual translations between them. ---------------------------------------------------------------------- Kazuyuki ASADA (National Institute of Informatics) Title: Curry-Howard Correspondence between Dialectica Interpretation and Bidirectional Transformation Abstract: We give Curry-Howard style correspondence between (propositional logic part of) Dialectica interpretation and bidirectional transformation. Dialectica interpretation was introduced by Godel to show relative consistency of Heyting Arithmetic to System T. Independently, bidirectional transformation arose in database community for automatic view-update problem, and recently have been studied in programming language community to formulate languages for bidirectional transformations. A bidirectional transformation consists of a pair of forward ("usual") transformation and a backward ("inverse") transformation, and we usually assume that they satisfy some standard axioms called GetPut law and PutGet law. We show GetPut law naturally fits the above correspondence to Dialectica interpretation, and this gives a way of extending a language for bidirectional transformations with GetPut law. Then we modify the above scheme for PutGet law and the combination of GetPut and PutGet laws. We also show that Paiva's variant of Dialectica model, GC, corresponds to the category for inverse computation. Then for the result by Paiva that the original Dialectica category is the coKleisli category of some comonad on GC, we give similar result for PutGet law, and we utilize this to investigate further categorical structures of these models. Also we see that a kind of Diller-Nahm variant of Dialectica interpretation corresponds to backward-partial bidirectional transformation. ---------------------------------------------------------------------- Makoto Tatsuta (National Institute of Informatics) Title: Dual Calculus with Inductive and Coinductive Types Abstract: This talk gives an extension of Dual Calculus by introducing inductive types and coinductive types. The same duality as Dual Calculus is shown to hold in the new system, that is, this talk presents its involution for the new system and proves that it preserves both typing and reduction. The duality between inductive types and coinductive types is shown by the existence of the involution that maps an inductive type and a coinductive type to each other. The strong normalization in this system is also proved. First, strong normalization in second-order Dual Calculus is shown by translating it into second-order symmetric lambda calculus. Next, strong normalization in Dual Calculus with inductive and coinductive types is proved by translating it into second-order Dual Calculus. This is a joint work with Daisuke Kimura. ---------------------------------------------------------------------- Stefano Berardi (Torino University) Title: A Curry-Howard result for various subclassical logics Abstract: We introduce games with Sequential Backtracking as a model for various sub-classical logic that have implication as a primitive connective. We define a one-sided version of the logical systems, whose proofs have a tree isomorphism (a kind of ``Curry Howard'' isomorphism) with respect to the winning strategies of the game semantics. We use this correspondence to interpret various classical proofs as learning algorithms. ---------------------------------------------------------------------- 問合せ先　龍田 (tatsuta(a)nii.ac.jp)

1 0

数学基礎論及び歴史分科会からの重要なお知らせ
by Masahiro Kumabe 31 Jan '13

31 Jan '13

皆様複数受け取られた場合はご容赦ください。こんにちは。日本数学会の数学基礎論及び歴史分科会の連絡評議委員の隈部です。学会に関して、以下の通りお知らせします。重要な内容ですので、是非ご一読お願い致します。（１）学会における一般講演のアブストラクトについて２０１３年度年会から、数学会として、一般講演のアブストラクトをPDFファイルとして、学会開催前に、数学会のホームペジにて公開することになりました。公開する時期は、学会が開催される２週間前までには公開する予定でいますが、詳しい内容については、学会のホームページにアクセスして、その都度ご確認ください。なおアブストラクトは、学会の会員外の方もダウンロードできるようにする予定です。これにより、アブストラクトを事前に各個人がプリントアウトし、それを持参して、学会に臨むことができるようになります。（２）（１）の対応に関連して、学会会場にて販売されていたアブストラクトの冊子の販売については、分科会として、以下の通りとすることになりました。アブストラクトの冊子での販売は、上記変更による混乱を避けるため、２０１３年度年会においては、続けます。ただし販売部数が減少することが予想されるため、用意する部数を減らします。アブストラクトの冊子の購入を希望される方は、この点ご了解ください。また出来る限り、事前にアブストラクトをプリントアウトあるいはダンロードして、学会に臨まれることをお願いします。当分科会のアブストラクトは、会員外の方もダウンロードできますので、できるだけそのようにお願いします。アブストラクトの冊子での販売は、赤字が予想されますので、なるべく早い時期に廃止する方向で考えています。そのためにもスムーズな移行ができるよう、ご協力お願いします。（３）２０１３年度年会は京都で行われますが、開催期間の京都のホテルが既に混み合っていると数学会から連絡を受けました。ですから、至急ホテルの予約をしていただきますようお願いいたします。以上です。連絡評議委員隈部正博

1 0

Cristian S. Calude氏、Elena Calude氏講演会のお知らせ（中央大学研究開発機構）
by Kohtaro Tadaki 11 Jan '13

11 Jan '13

＜重複してお受け取りの方はご容赦ください＞皆様：中央大学の只木と申します。中央大学研究開発機構では、来週19日土曜日、ニュージーランド研究者Cristian S. Calude氏（オークランド大学）およびElena Calude氏（マッセイ大学）をお招きし、下記要領で講演会を開催します。皆様、奮ってご参加下さい。 ---------------------------------- 只木孝太郎 (Kohtaro Tadaki) 中央大学研究開発機構〒112-8551 東京都文京区春日1-13-27 E-mail: tadaki(a)kc.chuo-u.ac.jp WWW: http://www2.odn.ne.jp/tadaki/ ---------------------------------------------------------- Cristian S. Calude氏、Elena Calude氏講演会 ◆日時： 2013年1月19日（土）15時00分〜 17時30分 ◆場所：中央大学後楽園キャンパス 5号館1階 5138号室（下記参照） ◆参加申込：不要 ---------------------------------------------------------- [ 講演内容 ] ◆15時00分〜16時00分講演題目：The complexity of mathematical problems 講演者：Cristian S. Calude (University of Auckland, NZ) and Elena Calude (Massey University, NZ) 講演要旨： Evaluating (or even guessing) the degree of complexity of an open problem, conjecture or mathematically proven statement is not an easy task not only for beginners, but also for the most experienced mathematicians. Is there a (uniform) method to evaluate, in some objective way, the difficulty of a mathematical statement or problem? The question is not trivial because mathematical problems can be so diverse. But, is there any indication that all, or most, or even a large part of mathematical problems have a kind of "commonality" allowing a uniform evaluation of their complexity? How could one compare a problem in number theory with a problem in complex analysis, a problem in algebraic topology or a theorem in dynamical systems? Surprisingly enough, such "commonalities" do exist for many mathematical problems. One of them is based on the possibility of expressing the problem in terms of (very) simple programs reducible to a (natural) question in theoretical computer science, the so-called "halting problem". A more general "commonality" can be discovered using the inductive type of computation, a computation more general the Turing computability. As a consequence, uniform approaches for evaluating the complexity of a large class of mathematical problems/conjectures/statements can be, and have been, developed. This talks reviews current progress and some open problems. ◆16時30分〜17時30分講演題目： The Kochen-Specker theorem and quantum randomness 講演者： Cristian S. Calude (University of Auckland, NZ) 講演要旨： The Kochen-Specker theorem shows the impossibility for a hidden variable theory to consistently assign values to certain (finite) sets of observables in a way that is noncontextual and consistent with quantum mechanics. If we require noncontextuality, the consequence is that many observables must not have pre-existing definite values. However, the Kochen-Specker theorem does not allow one to determine which observables must be value indefinite. In this talk we present an improvement on the Kochen-Specker theorem which allows one to actually locate observables which are provably value indefinite. Various technical and subtle aspects relating to this formal proof and its connection to quantum mechanics are discussed. This result is then utilized for the proposal and certification of a dichotomic quantum random number generator operating in a three-dimensional Hilbert space. ------------------------------------------------------------ 会場への道順： [中央大学後楽園キャンパスへのアクセスガイド] http://www.chuo-u.ac.jp/chuo-u/access/index_j.html http://www.chuo-u.ac.jp/chuo-u/access/access_korakuen_j.html [中央大学後楽園キャンパスマップ] http://www.chuo-u.ac.jp/chuo-u/campusmap/korakuen_j.html ------------------------------------------------------------

1 0

First Announcement ― TACL 2013
by Hiroakira Ono 18 Dec '12

18 Dec '12

[Apologies for multiple copies] ====================================================== TOPOLOGY, ALGEBRA AND CATEGORIES IN LOGIC (TACL 2013) ====================================================== July 28 - August 1, 2013 Department of Mathematics, Vanderbilt University Nashville, Tennessee USA http://www.math.vanderbilt.edu/~tacl2013/ The Sixth International Conference on Topology, Algebra and Categories in conjunction with the 28th Annual Shanks Lecture Series Scope --------- 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 program of the conference TACL 2013 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 sixth conference in the series Topology, Algebra and Categories in Logic (TACL, formerly TANCL). Earlier installments of this conference have been organized in Tbilisi (2003), Barcelona (2005), Oxford (2007), Amsterdam (2009), Marseilles (2011). Confirmed invited speakers ------------------------------------- Vladimir Voevodsky, Institute for Advanced Studies, USA (Shanks Lecturer) Nick Bezhanishvili, Utrecht University, The Netherlands Leo Cabrer, University of Oxford, UK Silvio Ghilardi, University of Milan, Italy George Metcalfe, University of Bern, Switzerland Alex Simpson, University of Edinburgh, UK Featured topics --------------------- Contributed talks can deal with any topic dealing with 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 Submissions ----------------- Contributed presentations will be of two types: o 20 minutes long presentations in parallel sessions and o featured, 30 minutes long, plenary presentations. The submission of an abstract will be required to be selected for a contributed presentation of either kind. While preference will be given to new work, results that have already been published or presented elsewhere will also be considered. More information on the submission procedure, as well as a link to the EasyChair system, can be found at the conference web site. Important dates ---------------------- April 1, 2013: Abstract submission deadline May 1, 2013: Notification to authors July 28-August 1, 2013: Conference Program Committee --------------------------- Steve Awodey, Carnegie Mellon University Guram Bezhanishvili, New Mexico State University David Gabelaia, Razmadze Mathematical Institute, Tbilisi Nick Galatos (co-chair), University of Denver Mai Gehrke, LIAFA, University of Paris Diderot Rob Goldblatt, Victoria University, Wellington John Harding, New Mexico State University Ramon Jansana, University of Barcelona Peter Jipsen, Chapman University Achim Jung, University of Birmingham Alexander Kurz (co-chair), University of Leicester Vincenzo Marra, University of Milan Hiroakira Ono, Japan Advanced Institute of Science and Technology Alessandra Palmigiano, University of Amsterdam Hilary Priestley, St Anne's College, Oxford James Raftery, University of KwaZulu-Natal, Durban Thomas Streicher, Technical University of Darmstadt Kazushige Terui, Kyoto University Constantine Tsinakis, Vanderbilt University Yde Venema, University of Amsterdam Michael Zakharyaschev, Birkbeck College, University of London Organizing Committee ------------------------------- Chris Conidis, Vanderbilt University Lianzhen Liu, Jiangnan University, China Warren McGovern, Florida Atlantic University Francesco Paoli, University of Cagliari Rebecca Steiner, Vanderbilt University Constantine Tsinakis (chair), Vanderbilt University William Young, Vanderbilt University Expression of interest ------------------------------ We would greatly appreciate your taking two minutes to express your level of interest in the conference by filling out a simple form on the conference web site under "Express Interest". This will help the Organizing Committee with their planning. You can also opt-out from receiving future announcements by clicking the link at the bottom of this email. More Information ----------------------- TACL 2013 web site: http://www.math.vanderbilt.edu/~tacl2013/ Use this site for local information, including hotel accommodations, for travel information and registration, and for submitting a request for financial support. Any queries for the Program Committee (such as usage of the EasyChair conference system, abstract submission guidelines, conference program, etc.) should be sent to tacl2013(a)gmail.com. Queries for the local Organizing Committee (registration, hotel accommodations, financial support and reimbursements, technology infrastructure, etc.) should be sent to tacl2013oc(a)vanderbilt.edu.

1 0

← Newer
1
...
47
48
49
50
51
52
53
...
59
Older →

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Kisoron-ml