25(Mon) ~ 29(Fri) March, 2013
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
- 26 March, 2013
- 27 March, 2013: free talks and discussions
- Objectives of doing rev. math. in relation with type
- strength of Sigma01-IND vs. (IND + pr. rec. functions)
- Is intuitionistically provable that DNR(4) implies DNR(2)?
- 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
- 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.
The Hoam Faculty House
is located on the campus of Seoul National University in Seoul, Korea.
The place is easily reachable by public transportation.
- First, consult the following web page.
- 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
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)
(PPS, University of Paris 7, France)
(LIAFA, University of Paris 7, France)
- Danko Ilik
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
Ludovic Patey (ENS, France)
Paul Shafer (Université Paris Diderot, France)
Antoine Taveneaux (LIAFA, France)
Takeshi Yamazaki (Tohoku University, Japan)