皆様
スワンジー大学のAnton Setzer先生の講演のお知らせです。 どうぞふるってご参加ください。
問合せ先： 石原 哉 北陸先端科学技術大学院大学 情報科学研究科 e-mail: [email protected]
----------------------------------------------- * JAIST Logic Seminar Series *
* This seminar is held as a part of the EU FP7 Marie Curie Actions IRSES projects COMPUTAL (http://computal.uni-trier.de/) and CORCON (http://corcon.net/).
Date: Thursday 22 January, 2015, 15:10-16:40
Place: JAIST, Collaboration room 6 (I-57g) (Access: http://www.jaist.ac.jp/english/location/access.html)
Speaker: Anton Setzer (Swansea University)
Title: Extraction of programs from proofs using postulated axioms (joint work with Chi Ming Chuang)
Abstract: In this talk we discuss how to extract programs from proofs with postulated axioms in dependent type theory. Since type theory has constructive logic, it is easy to determine for every $\Pi_2$-statement a function $f$ which determines the witness from the input. However, in the presence of postulated axioms, this function applied to an argument doesn't reduce necessarily to constructor head normal form, which means it doesn't produce a value.
In this talk we discuss conditions which guarantee that the extracted function provide values in the presence of postulated axioms, and give a proof.
This methodology will be applied to the extraction of alogrithms for exact real number computations. For this purpose the signed digit reals are introduced as a coalgebraic data type, and it is shown that the signed digit reals are closed under average, multiplication and rational numbers. Proofs have been carried out in the theorem prover Agda and the resulting programs can be executed effectively in this language.