Logic-ml March 2015

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

12 participants
15 discussions

講演会 (Nadia Polikarpova氏)
by Atsushi Igarashi 06 Mar '15

06 Mar '15

皆様，京都大学の五十嵐です．以下の要領で MIT の Nadia Polikarpova さんの講演会を実施いたしますので，ふるってご参加ください．当日夕方には，簡単な懇親会も考えておりますので，興味のある方は五十嵐までご連絡ください．どうぞよろしくお願いいたします -- 五十嵐淳 (IGARASHI Atsushi) E-mail: igarashi(a)kuis.kyoto-u.ac.jp url: http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/ ---------------------------------------------------------------------- 日時: ３月１２日(木) 14:00〜15:00 場所: 京都大学吉田キャンパス総合研究７号館(旧工学部１０号館)１階１３１号室(セミナー室２) Title: A Fully Verified Container Library and Synthesis from Liquid Types Abstract: In this talk I will discuss two approaches to constructing provably correct programs: one is based on automated deductive verification, and the other one combines program synthesis and refinement types. The first part of my talk will present AutoProof: an automated deductive verifier for heap-manipulating object-oriented programs, as well as our experience using AutoProof to prove full functional correctness of a realistic general-purpose container library. While the comprehensive functionality and flexible design of container libraries pose nontrivial challenges to formal verification, our results indicate that verifying a realistic library (135 public methods, 8,400 LOC) is possible with moderate annotation overhead (1.4 lines of specification per LOC) and good performance (0.2 seconds per method on average). The second part of my talk builds upon the Liquid Types framework, which has been successfully used to verify a wide range of properties of functional programs with very little human interaction. The secret to this success is the encoding of program invariants using a combination of types and predicates from an SMT-decidable logic. I will discuss some ideas on how Liquid Type inference could be extended to infer program components, and ultimately synthesize programs that are correct by construction. Bio: Nadia Polikarpova is a postdoctoral researcher at MIT, where she works with Armando Solar-Lezama. She obtained her PhD at ETH Zurich in 2014. Her research interests are in program verification and synthesis.

1 0

Talk by G. Sambin and M. Maietti [13 Mar 15:30-]
by Shinya Katsumata 06 Mar '15

06 Mar '15

京都大学数理解析研究所の勝股です。 3月13日15:30から、University of PadovaのGiovanni Sambin氏とMaria Emilia Maietti氏に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 15:30-17:30, 13 Mar, 2015 Place: Rm 478, Research Building 2, Main Campus, Kyoto University http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (See 34) 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speaker: Giovanni Sambin and Maria Emilia Maietti (University of Padova) Title: 1 A new foundation of constructive mathematics 50 years after Bishop's FCA 2 Why developing mathematics in a two-level foundation Abstract: --- 1. Giovanni Sambin --- A new foundation of constructive mathematics 50 years after Bishop's FCA Bishop's book Foundations of constructive analysis, 1967, briefly CFA, showed that constructive mathematics can be emancipated from the subjective views of its founder Brouwer. That single book started the process turning constructive mathematics into a rich and lively research field and community, as it is today. While standing on the shoulders of such giants, after almost fifty years it is our task to see further. Some epochal changes which took place after 1967 provide motivations and support. Outside mathematics: 1. Evolutionary thought has expanded its range of application and is now commonly accepted in science, except in mathematics. The main challenge awaiting us is to pass from a static, transcendent view of mathematics to a dynamic, human one. 2. The power of computers and other tools has enormously increased. Their active role in mathematical research will certainly also increase. This requires fully detailed formal systems for the foundation of mathematics. 3. Diffusion of information technology makes our world intensely connected. One feels the need of a framework which allows for a plurality of different world views. Moreover, inside mathematics: 1. new branches have been created, 2. other branches besides analysis have been constructivized, such as algebra and topology. The talk will give a preliminary view on a new foundational system inspired by these facts, first introduced in 2005 and later developed by M. E. Maietti and myself and called the Minimalist Foundation, shortly MF. Aims of MF include: 1. to permit the development of constructive mathematics, including topology, in agreement with a dynamic view (different levels of abstractions, real and ideal entities,...), 2. to provide a framework in which virtually all foundations of mathematics can be expressed by adding some assumptions (hence the adjective minimalist) and hence in particular a good setting for reverse mathematics, 3. to allow formalization of mathematics in a computer language, 4. to express the computational content of mathematics. More specifically MF keeps: 1. an effective notion of set different from an ideal notion of collection 2. the notions of operation (with instructions) distinct from that of function (without instructions), 3. a positive notion of existence We wish to know that MF is consistent by a proof, not by faith or feelings. One can prove much more than consistency for MF, namely a normalization theorem, a realizability interpretation, implementation in a proof-assistant. We conclude the talk by showing that one needs a theory with two levels of abstraction, thus providing a good introduction to Maietti's talk. --- 2. Maria Emilia Maietti --- Why developing mathematics in a two-level foundation We provide motivations for developing mathematics in a two-level formal system following the ideas put forward in joint work with G. Sambin in [MS05]. There we introduced the notion of two-level system to found constructive mathematics but it turned out that the same notion can be accomodated to develop mathematics in general with computer-aided formalization of its proofs. A main motivating example of such foundations is the Minimalist Foundation for constructive mathematics which was ideated in [MS05] and completed into two levels in [M09]. Its peculiarity is that it is compatible with most relevant constructive and classical foundations at the "right level". Another perculiarity is that its design makes use of different languages: mostly that of type theory, but also that of category theory and axiomatic set theory. [MS05] M.E. Maietti and G. Sambin "Toward a minimalist foundation for constructive mathematics" in L. Crosilla and P. Schuster eds., ''From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics", Oxford University Press, 2005 [M09] M.E. Maietti "A minimalist two-level foundation for constructive mathematics" Annals of Pure and Applied Logic 160(2009):319-354

1 0

教員公募（名古屋大学情報科学研究科・准教授）
by Jacques Garrigue 05 Mar '15

05 Mar '15

PPLおよびlogic-mlの皆様、名古屋大学のGarrigueです。名古屋大学の結縁先生のご依頼で、教員公募（名古屋大学情報科学研究科・准教授）をお送りします。 ====================================== （重複してお受け取りの場合はご容赦ください。）名古屋大学の結縁です。メーリングリストをお借りして公募情報をお送りいたします。名古屋大学情報科学研究科情報システム学専攻准教授　１名応募期限　4/28(消印有効) ------------------------------------------- 平成 27 年 2 月 4 日関係各位名古屋大学大学院情報科学研究科研究科長　坂部俊樹教員の公募について（依頼）謹啓　時下ますますご清祥のことお慶び申し上げます．さて，この度当研究科では，下記の要領により，教員を公募いたします．つきましては，貴学（機関）関係者にご周知いただければ幸いです．謹白記 1. 公募対象：准教授 1 名（名古屋大学大学院情報科学研究科情報システム学専攻ソフトウェア論講座） 2. 専門分野：ソフトウェア科学 (プログラムの検証理論，検証技術など) 3. 担当科目：情報科学研究科情報システム学専攻の講義および大学院学生の指導，工学部電気電子・情報工学科の講義および学生の指導，全学教育の講義 4. 応募資格：博士の学位を有する方 5. 任期：なし 6. 着任時期：2015 年 10 月 1 日以降のできるだけ早い時期 7. 提出書類： (1) 履歴書（写真付き） (2) 研究業績リスト（著書，学術論文誌，国際会議などを区分して記述） (3) 主要論文別刷（主要なもの 3 編以内，コピーも可） (4) これまでの研究概要（A4 用紙 2 枚程度） (5) 今後の研究計画および教育についての抱負（A4 用紙 1 枚程度） (6) その他選考に役立つ情報（教育実績，学会および社会活動，獲得した外部資金，受賞，特許，ソフトウェア開発実績など） (7) 応募者の業績について問い合わせることのできる方 2 名の氏名と連絡先 8. 応募期限：2015 年 4 月 28 日（火）(郵送の場合，当日消印有効) 9. 書類提出先および問い合わせ先：〒 464-8603 名古屋市千種区不老町 C3-1（631）名古屋大学大学院情報科学研究科平成 26 年度情報システム学専攻長　高田広章 TEL: 052-789-5887 Email: hiro ＠ is.nagoya-u.ac.jp ★封筒に「情報システム学専攻教員応募書類在中」と朱書し，持参または書留で郵送して下さい． 10. 備考： (1) 応募書類は原則として返却しません． (2) 応募書類は本選考のみに使用し，他の目的には使用しません． (3) 選考の過程でプレゼンテーションをお願いすることがあります． (4) 本学では採用に際して男女共同参画に配慮しております． -- Shoji Yuen, Graduate School of Information Science, Nagoya Univ., Japan 結縁祥治　名古屋大学大学院情報科学研究科 +81-52-789-3649

1 0

情報処理学会全国大会企画「計算に潜む数理，計算としての数理 --- 証明はプログラミング！」のご案内
by Kazutaka Matsuda 03 Mar '15

03 Mar '15

logic-ml関係者の皆様，東京大学の松田です．複数受け取られた場合はご容赦ください．この場をお借りして，情報処理学会全国大会の企画の一つとして 3/17の13:00〜15:30より京都大学吉田キャンバス吉田南総合館 2F 共北26で開催される「計算に潜む数理，計算としての数理 --- 証明はプログラミング！」 http://www.gakkai-web.net/gakkai/ipsj/77program/html/event/A-6.html のご案内をさせていただきたく存じます．情報処理学会全国大会は当日のご参加も受けつけており，企画セッションのみの聴講は無料です．詳しくは以下をご欄下さい． http://www.ipsj.or.jp/event/taikai/77/on_site_registration.html 本セッションでは，論理と計算に関する以下の3件の講演を企画しております． # 田中一之（東北大学大学院理学研究科教授）「決定問題の相転移について」 1920年代にヒルベルト学派が数理論理学の中心テーマとして掲げた「決定問題」は，狭義には1階論理における真偽を判定する手続きを求める問題である．これはゲーデルやチューリングによってすぐに否定的に解かれたが，その後も様々な角度から類似の問題が提起され，肯定的にも否定的にも豊富な結果と解決手法が生れた．肯定的な手法としては，オートマトンの強化がしばしば有効であるが，それをさらに非決定性にすると顕著に決定不能な結果が得られることがある．たとえば，決定性ω文脈自由言語のゲームは（計算的に）決定可能だが，非決定性の場合は通常の集合論で決定できない．本講演では，決定問題の大きな流れを振り返りつつ，決定可能性と不可能性の相転移現象についていくつかの例をもとに考察する．文献：田中一之『チューリングとメタパズル』東京大学出版会2013．田中一之『無限ゲームとオートマトン』数学セミナー2014年11月号． # 佐藤雅彦（京都大学名誉教授）「計算と論理」プログラミングという行為の背景にある計算と論理について解説する．特に，「プログラム」，「計算」，「論理」という3つの概念に共通するキーワードである「証明」に焦点を合せて，これら3概念の共通点，相異点を明きらかにし，プログラミングという行為の本質に迫ることを目標とする．直観主義的型理論において発見された「カリー・ハワード同型対応」は，命題と型の同型性に基づき，（命題の）「証明」と（型の要素としての）「プログラム」を同一視するという「証明」の見方を与えた．これは確かに有力な「ものの見方」であり，型を持つプログラミング言語や型理論に基づく Coq 等の証明支援系の理論的基盤を与えている．本講演では，このような「カリー・ハワード同型対応」によるプログラム観を紹介し，その有用性と同時にそれが抱える問題点を指摘する．上の型理論的証明観の問題点を理解するために，型理論誕生の動機となった18世紀末から19世紀初頭にかけての，「数学の危機」とよばれた数学の基礎付けをめぐる問題とその解決策が何であったかを説明する．これにより型理論を絶対視することなく，より広い観点からプログラミングという行為の本質に迫りたい． # AFFELDT　Reynald （産業技術総合研究所セキュアシステム研究部門・高信頼ソフトウェア研究グループ主任研究員）「定理証明支援系Coqによる形式検証」ソフトウェアや数学の証明に誤りのないことを保証するのは重要な研究課題である．1970年代からカリー＝ハワード同型対応に基づく形式体系の研究が継続的に行われてきた．その形式体系が定理証明支援系という形式検証ツールとして実現された結果，厳密で現実的な形式検証が可能となった．例えば，クリティカルな基盤ソフトウェア（コンパイラやオペレーティングシステム等）と大規模な数学の証明（四色定理やケプラー予想等）の形式検証が近年相次いで成功し，IT業界でも形式検証はスマートカードの厳密な安全性評価に応用されている．本発表では，ソフトウェアと数学の形式検証の実例を通じて，定理証明支援系による形式検証の基本を説明する．特に，ACMによる受賞を契機に注目を集めているフランス国立情報学自動制御研究所（INRIA）で開発されているCoqという定理証明支援系を紹介する．どうぞご参加を検討いただけますと幸いです．

1 0

Workshop on secure quantum computing
by NISHIMURA Harumichi 02 Mar '15

02 Mar '15

logic-mlの皆様，名古屋大学の西村です．群馬大学の森前先生に代わって secure quantum computingのワークショップのご案内を以下に投稿させていただきます．参加費無料，レジストレーション不要です．ご興味のある皆様の参加をお待ちしております．名古屋大学大学院情報科学研究科西村治道 ---------------------------------------- メーリングリストの皆様、群馬大の森前と申します。３月１９，２０日に東大本郷キャンパスで行われるWorkshop on secure quantum computingについてご案内させて頂きます。 http://tomoyukimorimae.web.fc2.com/Workshop_on_secure_quantum_computing.html 宜しくお願いします。森前 -------------------------------------

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml March 2015