Workshop on Reverse Mathematics and Type Theory
25(Mon) ~ 29(Fri) March, 2013
Hoam Faculty House, Seoul, Korea
About this workshop
This workshop is part of a Korea-France research project on Reverse Mathematics in Coq. The main goal of the research is to develop and implement formal systems that support doing “reverse mathematics” in the proof assistant Coq. This workshop aims at bringing together all participants of the project. Some external experts who could be interested by this line of research are invited.Schedule and talks
- 25 March, 2013
- 13:00~14:30 Hajime Ishihara, Constructive reverse mathematics
- 14:30~15:30 Hugo Herbelin, On the type-theoretic presentation of PRA
- 15:30~16:00 Coffee break
- 16:00~17:00 Danko Ilic, Applications and meta-mathematical implications of double-negation shift
- 17:00~18:00 Alexander Kreuzer, Non-principal ultrafilters, program extraction and higher order reverse mathematics
- 26 March, 2013
- 09:30~10:30 Takeshi Yamazaki, Filters and Reverse mathematics
- 10:30~11:00 Coffee break
- 11:00~12:00 Takayuki Kihara, WKL for infinite trees with few infinite paths
- 12:00~13:30 Lunch break
- 13:30~14:30 Takako Nemoto, Determinacy in classical and intuitionistic reverse mathematics
- 14:30~15:30 Gyesik Lee, Constructive formulation of the big five subsystems of second-order arithmetic
- 15:30~16:00 Coffee break
- 16:00~17:00 Keiko Nakata, Are streamless sets Noetherian?
- 17:00~18:00 Paul Shafer, A DNR(k) function that computes no DNR(2) function
- 27 March, 2013: free talks and discussions
- Objectives of doing rev. math. in relation with type theory (Takeshi)
- strength of Sigma01-IND vs. (IND + pr. rec. functions) (Gyesik)
- Is intuitionistically provable that DNR(4) implies DNR(2)? (Paul)
- 28 March, 2013: free talks and discussions
- Another view of zoo like RT22, DNR, etc. (Ludovic)
- Coquand-Hofmann translation (Hugo)
- 29 March, 2013: free talks and discussions
- Variants of choice axioms (Hugo)
- Presentation of 2nd-order arithmetic with sets or
functions (Takako)
- WKL strictly weaker than KL. Why?
Participation & registration
Everyone who is seriously interested in the subject of the workshop is welcome to the meeting. Registration is required although there is no registration fee. If you intend to attend the workshop, please send an email to the local organizer including full name, position, and affiliation.Venue
The Hoam Faculty House is located on the campus of Seoul National University in Seoul, Korea. The place is easily reachable by public transportation.Travel Information
- First, consult the following web page.
http://www.hoam.ac.kr/eng/hoamHotel/contact_us.php - Second, if you come from the Incheon Airport, take the limousine
bus No. 6017.
(See the time table.)
The Hoam Faculty House is the final stop. (approx. 70min) - Third, if you come from the city, take a subway, line number 2
(green line),
and get off at Nakseongdae station.
(See the map.)
Go to the exit number 4 and take bus number 02, and get off at the Hoam Faculty House. (approx. 10min)
Participants
- Shahin Amini (PPS, University of Paris 7, France)
- Laurent Bienvenu (LIAFA, University of Paris 7, France)
- Hugo Herbelin (INRIA, France)
- Danko Ilik (Macedonia)
- Hajime Ishihara (JAIST, Japan)
- Takayuki Kihara (JAIST, Japan)
- Alexander Kreuzer (ENS-Lyon, France)
- Gyesik Lee (Hankyong National University, Korea)
- Keiko Nakata (Tallinn University of Technology, Estonia)
- Takako Nemoto (JAIST, Japan)
- Ludovic Patey (ENS, France)
- Paul Shafer (Université Paris Diderot, France)
- Antoine Taveneaux (LIAFA, France)
- Takeshi Yamazaki (Tohoku University, Japan)
Organizers
Local organizers
Sponsors
