Kisoron-ml January 2015

4 participants
5 discussions

JAIST Logic Workshop Series 2015
by Hajime Ishihara 03 Feb '15

03 Feb '15

皆様来年3月に金沢で開催されるJAIST Logic Workshop Series 2015のお知らせです。ふるってご投稿・ご参加ください。問合せ先：石原　哉・木原貴行・根元多佳子・横山啓太北陸先端科学技術大学院大学情報科学研究科 e-mail: jlws2015(a)jaist.ac.jp -------------------------------------------------------- *Call for Abstracts* JAIST LOGIC WORKSHOP SERIES 2015 Constructivism and Computability 2 March 2015 – 6 March 2015 Shiinoki Cultural Complex, Kanazawa, Japan http://www.jaist.ac.jp/is/labs/ishihara-lab/jlws2015/ -------------------------------------------------------- IMPORTANT DATES November 30 - deadline for abstract submissions December 25 - notification of accepted contributions February 15 - deadline for registrations March 2-6 - Constructivism and Computability workshop TUTORIALS * Giovanni Sambin (University of Padova) * Hideki Tsuiki (Kyoto University) * Stanley Wainer (University of Leeds) INVITED SPEAKERS * Ulrich Berger (Swansea University) * Takayuki Kihara (JAIST) * Graham Leigh (Vienna University of Technology) * Michael Rathjen (University of Leeds) * Masahiko Sato (Kyoto University) * Makoto Tatsuta (National Institute of Informatics) PROGRAM COMMITTEE * Toshiyasu Arai (Chiba University) * Andrej Bauer (University of Ljubljana) * Ulrich Berger (Swansea University) * Hajime Ishihara (co-chair, JAIST) * Masahiro Kumabe (Open University of Japan) * Erik Palmgren (Stockholm University) * Peter Schuster (University of Leeds) * Helmut Schwichtenberg (co-chair, LMU Munich) * Dieter Spreen (University of Siegen, UNISA Pretoria) * Kazuyuki Tanaka (Tohoku University) SUBMISSIONS Submissions of short abstracts (1 page in PDF format) are accepted through easychair.org, see https://easychair.org/conferences/?conf=jlws2015 DESCRIPTION JAIST Logic Workshop Series is a workshop series bringing together researchers from mathematical logic and its application, especially to artificial intelligence and software science. Each workshop has its own focus on a specific area of research in mathematical logic and its application. Previous workshops have been held in Kanazawa 2013, 2014 and 2014: http://www.jaist.ac.jp/~hirokawa/pr2013/ http://www.jaist.ac.jp/~preining/wpp/ http://www.jaist.ac.jp/~v-sano/jw2014/index.html In 2015, JAIST Logic Workshop Series focuses on “Constructivism and Computability” aiming at interaction and knowledge transfer between constructive mathematics and computability theory. The workshop is held being affiliated with EU FP7 Marie Curie Actions IRSES projects COMPUTAL (http://computal.uni-trier.de/) and CORCON (http://corcon.net/), but is open to all researchers in the areas. SCOPE Constructive mathematics and computability, and related areas including but not limited to: intuitionistic logic and type theory, proof theory, constructive analysis and topology, program extraction from proofs, recursion theory, computable analysis and topology, classical/constructive reverse mathematics, algorithmic randomness, real number computation etc. LOCAL ORGANIZERS * Hajime Ishihara (JAIST) * Takayuki Kihara (JAIST) * Takako Nemoto (JAIST) * Keita Yokoyama (JAIST) The workshop is supported by: * Japan Advanced Institute of Science and Technology (JAIST) CO-LOCATED WORKSHOP * JSPS-NUS Joint Workshop in Mathematica Logic and Foundations of Mathematics (6-7 March 2015, at the same venue)

1 2

JSPS-NUS Joint Workshop in Logic
by Tanaka Kazuyuki 25 Jan '15

25 Jan '15

JSPS-NUS二国間共同研究のロジック・ワークショップのご案内シンガポールとの二国間交流事業（代表：田中、Chong）の一環として下記の研究会を開催致します。 Workshop in Mathematical Logic and Foundations of Mathematics 日程：2015年3月6日(金) から3月8日(日) まで場所：金沢しいのき迎賓館および金沢東急ホテルこのワークショップは主に共同研究のメンバーによって行われるものですが、ご関心のある方は一般からもご参加いただけます。但し、会場準備の都合上事前登録者に限りますので参加希望の方は SendaiLogic[at]math.tohoku.ac.jp （締切２月８日）までご連絡ください。下記のページで＜英語＞でもご案内しております。 http://www.math.tohoku.ac.jp/~tanaka/kanazawa2015.html よろしくお願いします。　東北大学　田中一之コンタクト：　SendaiLogic[at]math.tohoku.ac.jp

1 0

KusatsuSeminar3/16--20
by Fujita Kenetsu 13 Jan '15

13 Jan '15

皆様，『ラムダ計算と論理の早春セミナー』のご案内日程：2015年3月16日(月) 午後5時から3月20日(金) 正午まで場所：国立大学草津セミナーハウス　　　〒377-1711 群馬県吾妻郡草津町大字草津字白根737 詳細：http://www.cs.gunma-u.ac.jp/~fujita/2015.03LLSinKusatsu.htm 申込・質問などは藤田（群馬大学）までご連絡をお願いします．興味をお持ちのみなさまのご参加をお待ちしております． ----------- 群馬大学　藤田憲悦

1 0

Ninth NII Type Theory Workshop
by Makoto Tatsuta 11 Jan '15

11 Jan '15

Ninth NII Type Theory Workshop Date: January 15, 2015, 10:20--17:30 Place: National Institute of Informatics, Room 1208 (12th floor) 場所: 国立情報学研究所 12階 1208室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Program: 10:20--11:00 Daisuke Kimura (National Institute of Informatics) Title: A framework of models of functional PTSs 11:00--11:40 Josh Ko (National Institute of Informatics) Title: Relational algebraic ornamentation 11:40--13:10 Lunch Break 13:10--13:50 Makoto Fujiwara (Tohoku University) Title: On the strength of ¥Delta^0_1-LEM over Intuitionistic Analysis 13:50--14:30 Koji Nakazawa (Kyoto University) Title: Confluence of lambda-calculi with permutative conversion 14:30--14:50 Break 14:50--15:30 Mahmudul Faisal Al Ameen (The Graduate University for Advanced Studies) Title: Completeness of Separation Logic with Recursive Procedures 15:30--16:10 Makoto Tatsuta (National Institute of Informatics) Title: Decidability of Separation Logic with Monadic Inductive Definitions 16:10--16:30 Break 16:30--17:30 Stefano Berardi (Torino University) Title: Realizability and Strong Normalization for Heyting Arithmetic with EM1 Abstracts: ---------------------------------------------------------------------- Daisuke Kimura (National Institute of Informatics) Title: A framework of models of functional PTSs Abstract: This talk presents a framework of models of functional PTSs. The class of functional PTSs is a class of PTS which contains well-known type theories such as the simply typed lambda calculus, System F, lambda P (dependent type system), and Calculus of Constructions. This framework of models is obtained by using Cousineau and Dowek's embedding from a functional PTS into a lambda P modulo. As a result of this talk, a semantical condition for a functional PTS to be a strongly normalizing system is given. This result is expected to give a semantical approach to Barendregt-Geuvers-Klop conjecture. ---------------------------------------------------------------------- Josh Ko (National Institute of Informatics) Title: Relational algebraic ornamentation Abstract: Type theory makes it possible to treat programs and proofs uniformly as the same entities. Dependently typed programmers aim to design programs that carry their own correctness proofs, exploiting the coincidence of programs and proofs to the full extent. A generic construction that can help to achieve this is relational algebraic ornamentation, with which we can synthesise datatypes satisfying properties that can be expressed in terms of folds. In this talk I will show how relational algebraic ornamentation can help with designing a dependently typed program for solving the well-known minimum coin change problem. ---------------------------------------------------------------------- Makoto Fujiwara (Tohoku University) Title: On the strength of ¥Delta^0_1-LEM over Intuitionistic Analysis Abstract: Ishihara [2] showed over intuitionistic analysis EL that Markov’s principle MP is equivalent to WMP+¥Pi^0_1-DML(under the name of MP^v). On the other hand, Akama et al. [1] showed that ¥Delta^0_1-LEM is implied from both of MP(under the name of ¥Sigma^0_1-DNE) and ¥Sigma^0_1-DML(under the name of ¥Sigma^0_1-LLPO). In this talk, we show over EL that ¥Delta^0_1-LEM is implied from ¥Pi^0_1-DML and equivalent to ¥Delta^0_1 comprehension axiom, which is from reverse mathematics. In addition, some separation results are also presented. This is a joint work with Hajime Ishihara and Takako Nemoto. References: [1] Y. Akama, S. Berardi, S. Hayashi and U. Kohlenbach, An arithmetical hierarchy of the law of excluded middle and related principles. Proc. of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), pp. 192--201, IEEE Press (2004). [2] H. Ishihara, Markov's principle, Church's thesis and Lindel¥"of theorem, Indag. Math. (N.S.) 4 (1993), pp. 321--325. ---------------------------------------------------------------------- Koji Nakazawa (Kyoto University) Title: Confluence of lambda-calculi with permutative conversion Abstract: We give a new proof of confluence for the lambda and the lambda-mu calculi with permutative conversion for case branching. For such calculi, naive approaches with parallel reductions do not work, and we adopt a proof technique with generalized notions of complete development with the Z property, introduced by Dehornoy and van Oostrom. Our idea also gives a simpler proof for confluence of the first-order classical natural deduction, which has been proved by Ando with more complicated notions. ---------------------------------------------------------------------- Mahmudul Faisal Al Ameen (The Graduate University for Advanced Studies) Title: Completeness of Separation Logic with Recursive Procedures Abstract: This talk proves the completeness of Hoare's Logic extended by separation logic for verification of while programs with pointers and recursive procedures. ---------------------------------------------------------------------- Makoto Tatsuta (National Institute of Informatics) Title: Decidability of Separation Logic with Monadic Inductive Definitions Abstract: This talk shows the decidability of entailments of symbolic heaps in separation logic with monadic inductive definitions under certain conditions. ---------------------------------------------------------------------- Stefano Berardi (Torino University) Title: Realizability and Strong Normalization for Heyting Arithmetic with EM1 Abstract: We present a new Curry-Howard correspondence for HA+EM1, first order constructive Heyting Arithmetic with the excluded middle on Sigma-0-1-formulas. We add to the lambda calculus an operator k_a which represents, from the viewpoint of programming, an exception operator with a delimited scope, and from the viewpoint of logic, a restricted version of the excluded middle. We motivate the restriction of the excluded middle by its use in proof mining; we introduce new techniques to prove strong normalization for HA + EM1 and the witness property for simply existential statements. One may consider our results as an application of the ideas of Interactive realizability, which we have adapted to the new setting and used to prove our main theorems. This technique has been recently extended by F. Aschieri to the entire excluded middle for First Order Arithmetic. This is a joint work with F. Aschieri and G. Birolo. ---------------------------------------------------------------------- 問合せ先　龍田 (tatsuta(a)nii.ac.jp)

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 10 Jan '15

10 Jan '15

皆様スワンジー大学のAnton Setzer先生の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学研究科 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 projects COMPUTAL (http://computal.uni-trier.de/) and CORCON (http://corcon.net/). Date: Thursday 22 January, 2015, 15:10-16:40 Place: JAIST, Collaboration room 6 (I-57g) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Anton Setzer (Swansea University) Title: Extraction of programs from proofs using postulated axioms (joint work with Chi Ming Chuang) Abstract: In this talk we discuss how to extract programs from proofs with postulated axioms in dependent type theory. Since type theory has constructive logic, it is easy to determine for every $\Pi_2$-statement a function $f$ which determines the witness from the input. However, in the presence of postulated axioms, this function applied to an argument doesn't reduce necessarily to constructor head normal form, which means it doesn't produce a value. In this talk we discuss conditions which guarantee that the extracted function provide values in the presence of postulated axioms, and give a proof. This methodology will be applied to the extraction of alogrithms for exact real number computations. For this purpose the signed digit reals are introduced as a coalgebraic data type, and it is shown that the signed digit reals are closed under average, multiplication and rational numbers. Proofs have been carried out in the theorem prover Agda and the resulting programs can be executed effectively in this language.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Kisoron-ml January 2015