今後の開催予定
- 第4回
- 日時: 未定
- 場所: 未定
- 講演者：未定
- 講演タイトル：未定
- 概要：未定
過去の開催履歴
クリックすると詳細が表示されます．
第3回：2025年2月27日 | 佐藤 哲也 | 差分プライバシーの検証と形式化
- 日時：2025年2月27日 (木) 16:30 開始
- 場所：東京科学大学 大岡山キャンパス 西8号館 W1008号室
- 講演者：佐藤 哲也
- 所属：東京科学大学 (南出研 助教)
- 講演タイトル：差分プライバシーの検証と形式化
- 講演資料
- 概要：本講演では、差分プライバシーの概要と、圏論的特徴づけの研究、最近行っているIsabelle/HOLによる形式化について紹介する。差分プライバシーとは、データベースの統計的なプライバシー基準とそれを実現する為のノイズ付加手法を指す。多くの応用が存在し、iOS の入力候補の推定や、Google Maps の混雑状況の算出、アメリカの国勢調査などにおける匿名化などに用いられている。こうした差分プライバシーを検証するためのシステムの数学的基礎として、講演者は関係持ち上げによる圏論的特徴づけの研究を行い、差分プライバシーの元となる統計的距離の圏論的性質を調べた。Isabelle/HOLによる形式化・検証については、基本的な部分が組みあがったところで、Future Workがいくつかあるのでそれも紹介したい。
第2回：2024年12月19日 | 松下 祐介 | 量子、並列、所有権
- 日時：2024年12月19日 (木) 16:00 開始 (開場予定 15:30)
- 場所：国立情報学研究所(NII) 1208・1210会議室
- 講演者：松下 祐介
- 所属：京都大学 (五十嵐・末永研 特別研究員(PD))
- 講演タイトル：量子、並列、所有権
- 講演資料
- 概要：この講演では、私・平田賢吾氏・脇坂遼氏の現在進行中の共同研究である、細粒度の並列化のための並行量子分離論理について発表します。 私たちの論理では、細粒度の並列化で性能を上げた量子プログラムをモジュラーに検証できます。特に、同じ量子ビットを操作するが意味論的にはデータ競合がない並列プロセスについて推論できます。また、ある種の完全性も満たします。そのための鍵となる仕組みは、柔軟な共有を可能にする、量子メモリに対する新しい形の所有権です。
第1回：2024年11月6日 | 酒寄 健 | Semantics of circuit description language with dependent type-and-effect systems
- 日時：2024年11月6日 (水) 17:00 開始
- 場所：東京大学理学部７号館 214教室
- 講演者：酒寄 健
- 所属：東京大学 (小林研 助教)
- 講演タイトル：Semantics of circuit description language with dependent type-and-effect systems
- 概要：Circuit description languages, such as Proto-Quipper, are high-level languages used to describe and generate circuits, a quintessential example being the quantum circuit. To statically estimate the resources used in a circuit generated by Proto-Quipper, a dependent type-and-effect system was recently developed.
In this talk, I will discuss the denotational side of this story in a step-by-step manner.
First, the categorical semantics for a variant of the simply typed Proto-Quipper will be given using an indexed (aka parameterized) monad that handles the effect of circuit generations. Then, ideas to extend this semantics for dependent types and effect systems will be presented independently. Finally, I’ll explain my attempts to unify these extensions (which I still haven’t succeeded in). If time allows, I would also like to discuss with the audience whether this concrete semantic model for circuits can be generalized and applied in other contexts. This is a joint ongoing work with Andrea Colledan and Ugo Dal Lago.
発起人