Logic-ml January 2015

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

14 participants
18 discussions

CFP: PPL2015 サーベイ・チュートリアル、ポスター発表募集
by Makoto Hamana 13 Jan '15

13 Jan '15

皆様、群馬大学の浜名です。来年3月に愛媛県松山市道後温泉で開催される第17回プログラミングおよびプログラミング言語ワークショップ PPL'15 2015年3月4日(水)〜3月6日(金) http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ のサーベイ・チュートリアル、ポスター発表申込みの案内をさせていただきます。 * サーベイ・チュートリアル発表 (カテゴリ4）は、今年のPPLからの試みで、プログラミング言語分野の学生、研究者に役立つようなサーベイ・チュートリアル発表を広く募集します。プログラミング言語理論も実装も歴史が深くなってきて、自分の特定専門分野の事は知っていても、なかなか他の小分野の事はよく知らないという事が多くなってきました。そこでプログラミング言語に関わる様々な理論、応用の小分野間の相互理解と全体の底上げとなる事を目指し、設置しました。既発表・未発表の別を問いません(申込みは簡単なアウトラインの提出のみ)。既存発表の解説論文、教科書、セミナーや講義での資料、経験などお持ちの方はそれを用いていただくのも便利かと思います。 - ある専門分野の事を皆にもっと知ってもらいたい！ - 難しい分野と言われているがアイデアはそんなことないから解説したい。 - 現在隆盛を誇っている分野はこんな風に発展してきた。あまり知られていないが自分の専門性から解説したい。 - 解説論文を出版したけど、これを発表で話したことはないな… - 自分もやってる活発な〇〇分野の研究動向をまとめたいけどなかなかきっかけがない。これを機にまとめようか。などいろいろパターン、動機はあるかと思います。上記どれか当てはまるような方、もちろんそれに限らず、ぜひ申込みいただければと思います。通常発表と同様の30分での発表を予定していますが、採択件数によっては発表者との相談で少し時間延長もできるかもしれません。通常研究発表とは違い、ある程度確立した分野の話、専門家の方にお願いできればと思っております。PPLへの関連および関連研究への言及をもとに採録を判定いたします。 * ポスター・デモ発表 (カテゴリ3)は例年盛況な2時間程度のセッション内でのポスター発表またはデモ発表です。既発表・未発表の別を問いません。今年はポスター賞も設置しました。申込み多数の場合はプログラム委員会での選考により採否を決定します。締切はどちら(カテゴリ3,4)も、来週末 2015年1月23日(金) 17:00 (JST) ですので、ぜひ申込みをご検討ください。詳しい申込み方法などは http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ ご参照ください。 -- 浜名　誠群馬大学理工学府電子情報部門 http://www.cs.gunma-u.ac.jp/~hamana/

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

Logic, religion and science
by Kensaku GOMI 08 Jan '15

08 Jan '15

Dear Sirs and Madams, Regarding conflicts among religions and between religion and science, and regarding the 1st World Congress on Logic and Religion http://www.uni-log.org/logic-and-religion.html, I would inform you of the paper entitled ``MATHEMATICAL THEOLOGY: A Proscience Concept of God with a Mathematical Model'' http://homepage3.nifty.com/gomiken/english/mathpsy.htm. I believe that it contributes to promoting harmony among religions and reconciling religion and science toward omniscience. Would you support it by forwarding this mail to your acquaintances who would be interested? With kind regards, The original sender: Kensaku Gomi, a retired professor of the Graduate School of Mathematical Sciences, University of Tokyo.

1 0

NLCS '15 Call for Papers
by Makoto Kanazawa 05 Jan '15

05 Jan '15

Third Workshop on Natural Language and Computer Science NLCS '15 July 5, 2015 Kyoto, Japan http://www.indiana.edu/~iulg/nlcs.html A workshop affiliated with 42nd International Colloquium on Automata, Languages and Programming (ICALP 2015) and 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015) Endorsed by the Association for Computational Linguistics Special Interest Group on Computational Semantics Paper submission deadline: April 2, 2015 AIMS AND SCOPE Formal tools coming from logic and category theory are important in both natural language semantics and in computational semantics. Moreover, work on these tools borrows heavily from all areas of theoretical computer science. In the other direction, applications having to do with natural language has inspired developments on the formal side. The workshop invites papers on both topics. Specific topics includes, but are not limited to: • logic for semantics of lexical items, sentences, discourse and dialog • continuations in natural language semantics • formal tools in textual inference, such as logics for natural language inference • applications of category theory in semantics • linear logic in semantics • formal approaches to unifying data-driven and declarative approaches to semantics INVITED SPEAKERS Makoto Kanazawa, National Institute of Informatics Gerard de Melo, Tsinghua University PROGRAM COMMITTEE • Heather Burnett, Université de Toulouse 2 • Robin Cooper, University of Gothenburg • Valeria de Paiva, Nuance Communications • Tim Fernando, Trinity College • Nissim Francez, The Technion • Makoto Kanazawa, National Institute of Informatics • Larry Moss, Indiana University • Aarne Ranta, University of Gothenburg • Christian Retoré, Université de Montpellier PAPER SUBMISSIONS Extended abstracts of up to 10 pages may be submitted through Easychair: https://easychair.org/conferences/?conf=nlcs15 ORGANIZERS Valeria de Paiva Nuance.com Email: Valeria.dePaiva at nuance .com Makoto Kanazawa National Institute of Informatics Email: kanazawa at nii.ac.jp Larry Moss Indiana University Email: lsm at cs.indiana . edu IMPORTANT DATES Paper submission deadline: April 2, 2015 Author notification: May 1, 2015 Electronic versions of papers due: May 14, 2015 Workshop: July 5, 2015

1 0

『第２回山陰基礎論・解析学研究集会』の御案内
by Horihata Yoshihiro 05 Jan '15

05 Jan '15

皆様米子高専の堀畑です．米子（鳥取県）にて下記要領で『第２回山陰基礎論・解析学研究集会』を開催いたします．分野を超えて，基礎論，関数解析，微分幾何，偏微分方程式の研究者が集まり，ざっくばらんに意見交換できる場にしたいと思っています．現在，発表１２件，参加者２０人前後となっています．講演をご希望される方は，少し詳しいアブストラクト（Texソース）と共に，１月１３日（火）までに堀畑までご連絡頂ければ幸いです．聴講のみご希望の方は１６日（金）頃までにご一報いただければ助かります．【日時】　１日目：１月２４日（土）１０時～１７時　２日目：１月２５日（日）１０時～１３時（時間については予定です．終了時間は発表件数によって変わる可能性があります）【場所】国際ファミリープラザ３Ｆ稲盛ホール（米子駅から徒歩１０分程）ＨＰ→ http://familyplaza.net/conference2 ※２３日（金）夜と２４日（土）夜に懇親会を行います．詳細は堀畑まで．会の詳細は下記ホームページで更新していきます： https://sites.google.com/site/yonagonctmath/slas2015 以上です．よろしくお願い申し上げます．堀畑佳宏 -- 米子工業高等専門学校教養教育科・数学〒683-8502 鳥取県米子市彦名町4448 E-mail: horihata(a)yonago-k.ac.jp

1 0

FW: UNILOG'2015 in Istanbul and 10th PLS in Samos Island
by Kensaku GOMI 05 Jan '15

05 Jan '15

From: jean-yves beziau [mailto:jyb.logician@gmail.com] Sent: Monday, January 5, 2015 3:44 AM To: Kensaku GOMI Forwarded to: Logic-ml Subject: UNILOG'2015 in Istanbul and 10th PLS in Samos Island Hope to see you at the 5th UNILOG - World Congress and School on Universal Logic to happen in Istanbul, June 20-30, 2015 http://www.uni-log.org/enter-istanbul As indicated in our website: The event is organized in combination with the 10th Panhellenic Logic Symposium that will happen June 11-15, 2015 in Samos Island, where Pythagoras was born. https://samosweb.aegean.gr/pls10/ A travel by bus from the nearby port of Kusadasi in Turkey up to Istanbul will be organized with stops on famous historical sites: Ephesus, Troy, etc. Special arrangements will exist for participants who wish to attend both conferences. I am sending you attached the posters for UNILOG'2015 and the related contest "The Future of Logic". I would be glad if you can print them (colour A3) and post them at your university /institute or if you prefer I can send them to you by post (then send me your exact mailing address) I wish you a happy new year 2015 Jean-Yves >----------------------------------------------------------------------> Jean-Yves Beziau Editor-in-Chief - Logica Universalis Latest Issue Scope of Logic Theorems - In Memoriam Adolf Lindenbaum http://link.springer.com/journal/11787/8/3/page/1

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml January 2015