皆様
ストックホルム大学のErik Palmgren先生の連続講義のお知らせです。
ふるってご参加ください。
問合せ先：
石原 哉
北陸先端科学技術大学院大学 情報科学研究科
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 project CORCON (http://corcon.net/).
Date:
Lecture 1. Monday 9 March, 2015, 15:10-16:40
Lecture 2. Tuesday 10 March, 2015, 15:10-16:40
Lecture 3. Wednesday 11 March, 2015, 15:10-16:40
Place: JAIST, Lecture room I3-I4
(Access: http://www.jaist.ac.jp/english/location/access.html)
Speaker: Professor Erik Palmgren
(Department of Mathematics, Stockholm University)
Title: Lectures on type theory with a view towards formalizing
Bishop-style mathematics
Abstract:
In this series of three lectures we give an introduction to Martin-Lof
type theory and the tools it provides for formalizing Bishop-style
constructive mathematics.
The first lecture will cover basic principles of type theory and give an
introduction to its manifestation in the well-known proof assistant Coq.
In the second lecture we consider "Bishop's set theory" (Bishop and
Bridges 1985) from the point of view of type theory, which will involve
a development the theory of setoids and subsetoids.
The third lecture will cover models constructive set theory (CZF) in
type theory, and how it can be used to solve the problem of universes of
setoids and development of category theory.
Throughout the lectures we provide examples and suggestions how you can
yourself experiment with the Coq system in the formalization of
constructive mathematics.
References
E. Bishop and D.S. Bridges. Constructive Analysis. Springer 1985.
E. Palmgren. Lecture notes on Type Theory. Stockholm 2014. URL:
http://kurser.math.su.se/course/view.php?id=48
E. Palmgren and O. Wilander. Constructing categories and setoids of
setoids in type theory. Logical Methods in Computer Science. 10(2014),
Issue 3, paper 25.
Prof. Georg Moser at NII Logic Seminar
Date: February 13, 2015, 14:00--16:00
Place: National Institute of Informatics, Room 1208 (12th floor)
場所: 国立情報学研究所 12階 1208室
(半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分)
(地図 http://www.nii.ac.jp/about/access/)
Speaker: Prof. Georg Moser (University of Innsbruck)
Title: Amortised Cost Analysis and Term Rewrite Systems
Abstract:
I will present a univariate resource analysis for typed term rewrite
systems based on a potential-based type system. This type system gives
rise to polynomial bounds on the innermost runtime complexity. The
thus obtained amortised resource analysis relates to polynomial
interpretations and we obtain the perhaps surprising result that
whenever a rewrite system can be well-typed, then there exists a
polynomial interpretation that orients the system. If time permits
I'll speak about very recent generalisations to a multivariate
analysis. This is a joint work with Martin Hofmann.
問合せ先:
龍田 真 (国立情報学研究所)
e-mail: tatsuta(a)nii.ac.jp
http://research.nii.ac.jp/~tatsuta
皆様
来年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)
