みなさま
今週木曜に京都大学にてUlrich Bergerさんによるご講演があります。
詳細は下記の通りです。よろしければご参加ください。
京都大学数理解析研究所
照井一成
==========
Time: 11:00-12:00, 17th January, 2019
Place: Rm 478, Research Building 2, Main Campus, Kyoto University
京都大学 本部構内 総合研究2号館 4階478号室
http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34)
Speaker: Ulrich Berger (Swansea University)
Title: Extracting the Fan Functional
Abstract: Consider a continuous functional F : (N -> B) -> N where N is the
type
of natural numbers and B is the type of Booleans, both endowed with
the discrete topology, and the function space N -> B carries the
pointwise topology. By a compactness argument (Koenig's Lemma or Fan
Theorem), F is uniformly continuous. Therefore, there exists a least
modulus of uniform continuity for F, that is, a least natural number m
such that F equates any two arguments that coincide below m. The
mapping F |-> m is called Fan Functional. Gandy showed that the Fan
Functional is computable. Later it was shown that it is computable
even in the restricted sense of Kleene's schemata (S1-S9), or,
equivalently, PCF. In this talk we show that the Fan Functional is
the computational content of a constructive proof of the uniform
continuity of F.
**************************************************************************
Call for papers — ENTROPY 2019
ENabling TRust through Os Proofs … and beYond
Second International workshop on the use of theorem provers for modelling
and verification at the hardware-software interface
Co-located with EuroS&P'19, KTH, Stockholm, June 2019
**************************************************************************
AIM AND SCOPE
Low level software such as kernels and drivers, along with the hardware
this software runs on, is critical for application security. In contrast
with user applications, OS kernel software runs in privileged CPU mode
and is thus highly critical. Large projects such as seL4, VeriSoft,
CertiKoS and Prosper have invested considerable resources in developing
formally verified systems such as hypervisors and microkernels, supplying
proofs that they satisfy critical properties. Such proofs are delicate in
terms of the scale and complexity of real systems, the models used in
performing the proof search, and the relations between the two, which
recent vulnerabilities such as Spectre and Meltdown have shown to be a
highly non-trivial issue.
The purpose of this workshop is to share, compare and disseminate best
practices, tools and methodologies to verify OS kernels, also setting the
stage for future steps in the direction of fully verified systems,
dealing with issues related to modelling, model validation, and large
proof maintenance through system evolution. On one hand, we need to make
low-level proofs more scalable, modular and cost-effective. On the other
hand, once certified systems are available, preservation and maintenance
of their proofs of validity become key questions.
The goal of the ENTROPY workshop is to provide a forum for researchers
and practitioners in this space, linking operating systems, formal
methods, and hardware architecture, interested in system design as well
as machine verified mathematical proofs using proof assistants such as
Coq, Isabelle and HOL4.
This will be the second edition of the ENTROPY workshop series. The
first workshop was organised by the Pip Development Team at University
of Lille in 2018.
TOPICS OF INTEREST
Specific topics include, but are not limited to:
* Verified kernels and hypervisors
* Verified security architectures and models
* Tools and frameworks for hardware security analysis
* Tools and frameworks for security analysis
* Formal hardware models and model validation techniques
* Theorem prover based tools and frameworks for verification
of low level code
* Combinations of static analysis and theorem proving
* Theories and techniques for compositional security analysis
* Case studies and industrial experience reports
* Proof maintenance techniques and problems
* Compositional models and verification techniques
* Proof oriented design
The aim of the workshop is to stimulate innovation and active exchange
of ideas, so position papers, work-in-progress and industrial
experience submissions are welcome.
INVITED SPEAKERS (to be extended)
Frank Piessens, KU Leuven
Peter Sewell, Univ. Cambridge
IMPORTANT DATES
Paper submission: March 11 2019
Author notification: April 10, 2019
Camera-ready versions: April 22, 2019 (strict)
Workshop: 16 June 2019
SUBMISSION AND PUBLICATION
There are two categories of submissions:
1. Regular papers describing fully developed work and complete results
(8 pages, references included, IEEE format)
2. Short papers, position papers, industry experience reports,
work-in-progress submissions: (4 pages, references included, IEEE
format)
All papers should be in English and describe original work that has not
been published or submitted elsewhere. The submission category should
be clearly indicated. All submissions will be fully reviewed by members
of the Programme Committee. Papers will appear in IEEE Xplore in a
companion volume to the regular EuroS&P proceedings. For formatting and
submission instructions see https://entropy2019.sciencesconf.org.
PROGRAM CHAIRS
Mads Dam, KTH Royal Institute of Technology
David Nowak, CNRS and University of Lille
PROGRAM COMMITTEE
Christoph Baumann, Ericsson AB
Gustavo Betarte, Univ. de la República, Uruguay
David Cock, ETH Zurich
Mads Dam, KTH Royal Institute of Technology (chair)
Anthony Fox, ARM
Deepak Garg, MPI Saarbrucken
Ronghui Gu, Columbia University
Samuel Hym, Univ. Lille
Thomas Jensen, INRIA and Univ. Rennes
Toby Murray, Univ. Melbourne
David Nowak, CNRS & Univ. Lille (chair)
Vicente Sanchez-Leighton, Orange Labs
Thomas Sewell, Chalmers
--
David Nowak
http://www.cristal.univ-lille.fr/~nowakd/
皆様
今年6月にドイツ・ドルトムントで開催されます、計算と演繹に関する
国際会議 FSCD の論文募集の最終案内をお送り致します。
是非、投稿をご検討下さい。
廣川 (JAIST)
---------------
Updated information: titles and abstracts of invited talks are now available
---------------
CALL FOR PAPERS
Fourth International Conference on
Formal Structures for Computation and Deduction (FSCD 2019)
24 -- 30 June 2019, Dortmund, Germany
http://easyconferences.eu/fscd2019/
IMPORTANT DATES
---------------
All deadlines are midnight anywhere-on-earth (AoE); late
submissions will not be considered.
Titles and Short Abstracts: 8 February 2019
Full Papers: 11 February 2019
Rebuttal period: 28 March -- 1 April 2019
Authors Notification: 8 April 2019
Final version for proceedings: 22 April 2019
FSCD covers all aspects of formal structures for computation and
deduction from theoretical foundations to applications. Building on
two communities, RTA (Rewriting Techniques and Applications) and TLCA
(Typed Lambda Calculi and Applications), FSCD embraces their core
topics and broadens their scope to closely related areas in logics,
models of computation (e.g. quantum computing, probabilistic
computing, homotopy type theory), semantics and verification in new
challenging areas (e.g. blockchain protocols or deep learning
algorithms).
Suggested, but not exclusive, list of topics for submission are:
1. Calculi:
Rewriting systems, Lambda calculus, Concurrent calculi, Logics,
Type theory, Homotopy type theory, Logical frameworks, Quantum
calculi
2. Methods in Computation and Deduction:
Type systems; Induction and coinduction; Matching, unification,
completion and orderings; Strategies; Tree automata; Model
checking; Proof search and theorem proving; Constraint solving and
decision procedures
3. Semantics:
Operational semantics; Abstract machines; Game Semantics; Domain
theory; Categorical models; Quantitative models
4. Algorithmic Analysis and Transformations of Formal Systems:
Type inference and type checking; Abstract interpretation;
Complexity analysis and implicit computational complexity; Checking
termination, confluence, derivational complexity and related
properties; Symbolic computation
5. Tools and Applications:
Programming and proof environments; Verification tools; Proof
assistants and interactive theorem provers; Applications in
industry (e.g. design and verification of critical systems);
Applications in other sciences (e.g. biology)
6. Semantics and verification in new challenging areas:
Certification; Security; Blockchain protocols; Data bases; Deep
learning and machine learning algorithms; Planning
INVITED SPEAKERS
-----------
Titles and abstracts available at
http://easyconferences.eu/fscd2019/invited-speakers/
* Beniamino Accattoli (INRIA, Paris, France)
https://sites.google.com/site/beniaminoaccattoli/
* Amy Felty (University of Ottawa, Canada)
http://www.site.uottawa.ca/~afelty/
* Sarah Winkler (University of Innsbruck, Austria)
http://cl-informatik.uibk.ac.at/users/swinkler/
* Hongseok Yang (KAIST, Korea)
https://sites.google.com/view/hongseokyang/
PUBLICATION
-----------
The proceedings will be published as an electronic volume in the
Leibniz International Proceedings in Informatics (LIPIcs) of Schloss
Dagstuhl. All LIPIcs proceedings are open access.
SUBMISSION GUIDELINES
---------------------
Submissions can be made in two categories. Regular research papers
are limited to 15 pages (including references, with the possibility to
add an annex for technical details, e.g.\ proofs) and must present
original research which is unpublished and not submitted
elsewhere. System descriptions are limited to 15 pages (including
references) and must present new software tools in which FSCD topics
play an important role, or significantly new versions of such
tools. Submissions must be formatted using the LIPIcs style files and
submitted via EasyChair. Complete instructions on submitting a paper
can be found on the conference web site:
http://easyconferences.eu/fscd2019/
BEST PAPER AWARD BY JUNIOR RESEARCHERS
--------------------------------------
The program committee will consider declaring this award to a paper in
which at least one author is a junior researcher, i.e. either a
student or whose PhD award date is less than three years from the
first day of the meeting. Other authors should declare to the PC Chair
that at least 50% of contribution is made by the junior
researcher(s).
SPECIAL ISSUE
-------------
Authors of selected papers will be invited to submit an extended
version for a special issue of Logical Methods in Computer Science.
PROGRAM COMMITTEE
-----------------
H. Geuvers, Radboud U. Nijmegen (Chair)
Z. Ariola, U. of Oregon
M. Ayala Rincón, U. of Brasilia
A. Bauer, U. of Ljubljana
F. Bonchi, U. of Pisa
S. Broda, U. of Porto
U. Dal Lago, U. of Bologna & Inria
U. De'Liguoro, U. of Torino
D. Kapur, U. of New Mexico
P. Dybjer, Chalmers U. of Technology
M. Fernandez, King's College London
J. Giesl, RWTH Aachen
N. Hirokawa, JAIST
S. Lucas, U. Politecnica de Valencia
A. Middeldorp, U. of Innsbruck
F. Pfenning, Carnegie Mellon U.
B. Pientka, McGill U.
J. van de Pol, Aarhus U. & U. of Twente
F. van Raamsdonk, VU Amsterdam
C. Schürmann, ITU Copenhagen
P. Severi, U. of Leicester
A. Silva, U. College London
S. Staton, Oxford U.
T. Streicher, TU Darmstadt
A. Stump, U. of Iowa
N. Tabareau, Inria
S. Tison, U. of Lille
A. Tiu, Australian National U.
T. Tsukada, U. of Tokyo
J. Urban, CTU Prague
P. Urzyczyn, U. of Warsaw
J. Waldmann, Leipzig U. of Applied Sciences
CONFERENCE CHAIR
----------------
Jakob Rehof, TU Dortmund
LOCAL WORKSHOP CHAIR
--------------------
Boris Düdder, U. of Copenhagen
STEERING COMMITTEE WORKSHOP CHAIR
--------------------------------
J. Vicary, Oxford U.
PUBLICITY CHAIR
---------------
Sandra Alves , Porto U.
FSCD STEERING COMMITTEE
-----------------------
S. Alves (Porto U.),
M. Ayala-Rincón (Brasilia U.)
C. Fuhs (Birkbeck, London U.)
D. Kesner (Chair, Paris U.)
H. Kirchner (Inria)
N. Kobayashi (U. Tokyo)
C. Kop (Radboud U. Nijmegen)
D. Miller (Inria)
L. Ong (Chair, Oxford U.)
B. Pientka (McGill U.)
S. Staton (Oxford U.)
Dear all (English translation follows below),
皆様、
お茶の水女子大学の叢です。
第29回 Agda Implementors' Meeting (AIM XXIX) を
3月13日(水)から
3月19日(火)まで
の予定で、お茶の水女子大学にて開催します。
このミーティングでは、定理証明支援系 Agda のユーザと開発者が
言語の理論や応用、拡張などについて議論します。
参加者に期待されるのは、
- 発表セッションへの貢献(任意・進行中の仕事も歓迎)
- code sprints への参加
の2つです。
ミーティングに関する情報は、以下のページに追加していく予定です:
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXXIX
参加者と発表の概数を把握したいので、参加をご希望の方は、
3月1日(金)までにメール最下部のフォームを
so.yuyu(a)is.ocha.ac.jp 宛にお送りください。
多数のご参加をお待ちしております。
どうぞよろしくお願いいたします。
叢 悠悠
We are happy to announce that the 29th Agda Implementors' Meeting
(AIM XXIX) will be held at Ochanomizu University
from March 13 (Wednesday)
to March 19 (Tuesday).
AIM provides an opportunity for the users and implementors of
the Agda proof assistant to discuss the theory, applications,
and extensions of the language. Participants are expected to
present their work in the talk session and take part in one or more
projects in the code sprint session.
More information about the meeting can be found at:
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXXIX
If you are interested in joining the meeting, please fill out the form
below and send it to so.yuyu(a)is.ocha.ac.jp by March 1 (Friday).
We look forward to your participation and contribution!
Best regards,
Youyou
-------8<--------------------------------------------------
Name:
Title and abstract (if you want to give a talk or lead a discussion; optional):
Suggestions for code sprints (optional):
Additional comments (optional):
直前ですが、次のワークショップの案内を流させていただきます。岡田光弘 慶應義塾大学
Workshop “Norm, Rule and Disagreement” Keio University Jan.11th, 2019
ワークショップ”Norm, Rule and Disagreemtnt”のお知らせ(慶応義塾大1月11日)
------------------------------------------------------------------------------------------------------------------
次のようなワークショップを予定しています。参加自由、事前登録無しです。パリ第1大学哲学科及び同大学IHPST論理の哲学グループと共同企画し、毎年1月に開催しているワークショップシリーズの5回目に当たります。The following Workshop is organized as the 5th one of the workshop series co-organized with the philosophy of logic group of University of Paris-1 (of Department of Philosophy and of IHPST).
For updated information, see Workshop URL
https://abelard.flet.keio.ac.jp/seminar/norm-rule-disagreement-2018
***ABSTRACTS are posted on the above page.* **
Time: Jan. 11th. Fri., 2019, 10:00-17:00, 1月11日金曜日
Place: 6th Floor, G-Lab, East Building (Higashi-Kan), Mita Campus of Keio University,
慶應義塾大学三田キャンパス東館6階G-Lab
Seven (7) minutes walking distance from JR-Tamachi, Subway-Mita or Subway-Akabanebashi.
JR田町駅、地下鉄三田駅、赤羽橋駅から徒歩7分
The South Building is #3 on Mita-Campus Map below:
https: (in Japanese and in English)
//www.keio.ac.jp/ja/maps/mita.html
//www.keio.ac.jp/en/maps/
PROGRAM
10:00 introductory remark
10:10 Pierre Wagner (Department of Philosophy and IHPST, University of Paris-1)
"How to disagree in logic and mathematics?"
11:10 Presentations from the collaborative project members on Philosophy of Mathematics and Logic (tentative),
including
1, Yuta Takahashi (Nagoya University),
2. Ryota Akiyoshi (Waseda University)
titles to be announced
11:50-13:00 Lunch Break
13:00-13:40 Florencia Di Rocco (Keio University (and University of Paris-1))
"Disagreement" and "language games"
13:40-14:00 Discussion and Pause
14:00 Yuichiro Hosokawa (Tokyo Metropolitan University)
"Belief, Knowledge and Possibility - Through Analysis of Gettier Problem by Modal Logic for Multiple Regions"
14:40-15:00 Discussion and Pause
15:00 Fleur Jongepier (Department of Ethics, Faculty of Philosophy, Theology and Religious Studies, Radboud University Nijmegen, the neitherlands)
"Algorithmic authority versus First-person authority"
15:40-16:00 Discussion and Pause
16:00 Mitsuhiro Okada (Department of Philosophy, Keio University)
Discussion on ”Formalism for Algorithmic Ethics” and
"Norm. Rule and Disagreement"
16:40 Closing Discussion Session
17:00 Closing
----------------------------------------------------------------
Workshop organizer, Sponsor,
Global Research Center for Logic and Sensitivity, Keio University
Email of the Workshop Office:[email protected]
主催及び問い合わせ先
慶應義塾大学 論理と感性のグローバル研究センター
logic(a)abelard.flet.keio.ac.jo
メーリングリストの皆様
九大の河村と申します。来年7月にクロアチアのザグレブで行われる「解析学と
計算理論」の国際会議CCA 2019の御案内をお送りいたします。
______________________________________________________________
First Call for Papers
Sixteenth International Conference on
Computability and Complexity in Analysis (CCA 2019)
http://cca-net.de/cca2019/
July 8-11, 2019, Zagreb, Croatia
Submission deadline: March 13, 2019
______________________________________________________________
The conference CCA 2019 is followed by the conference
Computability in Europe (CiE 2019) that takes place in
Durham, UK, from July 15-19, 2019.
Topics
- Computable analysis
- Complexity on real numbers
- Constructive analysis
- Domain theory and analysis
- Effective descriptive set theory
- Theory of representations
- Computable numbers, subsets and functions
- Randomness and computable measure theory
- Models of computability on real numbers
- Realizability theory and analysis
- Reverse analysis
- Weihrauch complexity
- Real number algorithms
- Implementation of exact real number arithmetic
Invited Speakers
- Douglas Cenzer (Gainesville, USA)
- Hannes Diener (Christchurch, New Zealand)
- Jacques Duparc (Lausanne, Switzerland)
- Hugo Férée (Kent, UK)
- Guido Gherardi (Bologna, Italy)
- Bruce Kapron (Victoria, Canada)
- Joël Ouaknine (Saarbrücken, Germany)
- Svetlana Selivanova (Novosibirsk, Russia)
Scientific Programme Committee
- Verónica Becher (Buenos Aires, Argentina)
- Vasco Brattka, chair (Munich, Germany)
- Akitoshi Kawamura, co-chair (Fukuoka, Japan)
- Neil Lutz (Pennsylvania, USA)
- Alberto Marcone (Udine, Italy)
- André Nies (Auckland, New Zealand)
- Peter Schuster (Verona, Italy)
- Dieter Spreen (Siegen, Germany)
- Florian Steinberg (Saclay, France)
- Sebastiaan Terwijn (Nijmegen, The Netherlands)
Organising Committee
- Konrad Burnik (Amsterdam, The Netherlands)
- Marko Horvat (Zagreb, Croatia)
- Zvonko Iljazović, chair (Zagreb, Croatia)
- Matea Kalinić (Split, Croatia)
- Bojan Pažek (Zagreb, Croatia)
Submissions
Authors are invited to submit 1-2 pages abstracts in PDF format,
including references via the following web page:
https://easychair.org/conferences/?conf=cca2019
If full versions of papers are already available as technical report
or arXiv version, then corresponding links should be added to the
reference list. Final versions of abstracts might be distributed to
participants in hard copy and/or in electronic form.
Dates
- Submission deadline: March 13, 2019
- Notification of authors: April 15, 2019
- Final version: May 6, 2019
- Registration deadline: May 20, 2019
--
河村彰星
九州大学システム情報科学研究院情報学部門
〒819-0395 福岡市西区元岡744
092-802-3806
http://www.fc.inf.kyushu-u.ac.jp/~kawamura/
kawamura(a)inf.kyushu-u.ac.jp
皆様
来年1月10日(木)に北陸先端科学技術大学院大学で行われます
Arnold Beckmann 教授の講演のお知らせです。皆様、どうぞ奮って
ご参加ください。
廣川 直 (JAIST)
-----------------------------------------------------------------------
* JAIST Logic Seminar Series *
Date: Thursday 10 January, 2019 (Thu) 13:30 - 15:00
Place: I-56 (Collaboration Room 7) at JAIST
(Access: http://www.jaist.ac.jp/english/location/access.html)
Speaker: Prof. Arnold Beckmann (Swansea University)
Title: Blockchain for Asset Reuse
Abstract:
We will consider how physical asset assemblies can be traced from
cradle to grave via security tags linked to a blockchain system.
The vision is that such blockchain enhanced asset systems will be
important to enable a circular economy, in which all kind of goods,
ranging from washing machines to cars, are being disassembled and
reassembled, with increased asset reuse and material recycling.
We will explain the basic principles behind this vision, and describe
a blockchain demonstrator that realises a part of it.
This is joint work with Michael Breach from Oyster Bay Systems,
a Swansea based FinTech company.
-----------------------------------------------------------------------