[kisoron-ml] Prof. Helmut Schwichtenberg Lecture at NII Logic Seminar

[Makoto Tatsuta]

	 Prof. Helmut Schwichtenberg Lecture at NII Logic Seminar

Date: February 21, 2013, 14:00--16:00

Place: National Institute of Informatics, Lecture Room 1208 (12th floor)
場所: 国立情報学研究所 12階 1208室
    (半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分)
    (地図 http://www.nii.ac.jp/about/access/)

Speaker: Prof. Helmut Schwichtenberg (Ludwig Maximilian University of Munich)

Title: Proofs and computations with infinite data

Abstract: 
Ulrich Berger and Monika Seisenberger recently studied extraction from
proofs involving (only) abstract reals.  They considered a proof using
coinduction of the proposition that any two reals in [-1,1] have their
average in the same interval, and informally extract a Haskell program
working with stream representations of reals.  We report on a
formalization of this proof, and a machine-extraction of its
computational content, in the Minlog proof assistant.  This required
an extension of this system to also take coinduction into account.
The underlying formal system is a theory TCF of computable
functionals.  It is similar to Heyting arithmetic in all finite types,
but with the Scott/Ershov partial continuous functionals as the domain
of quantifiers.  TCF has free type, predicate and function variables,
to allow for abstract developments (groups, fields, real analysis).
The underlying inference machinery is minimal logic (implication,
universal quantification plus inductively and coinductively defined
predicates).  Computable functionals (of finite type, with free
algebras at ground types) are given by their defining equations.
Since the logic is constructive, program extraction by means of a
realizability interpretation is possible and a soundness theorem
holds.

問合せ先:
龍田 真 (国立情報学研究所)
e-mail: tatsuta at nii.ac.jp
http://research.nii.ac.jp/~tatsuta