[logic-ml] JAIST Logic Seminar Series

[Hajime Ishihara]

皆様

スワンジー大学のAnton Setzer先生の講演のお知らせです。
どうぞふるってご参加ください。

問合せ先：
石原　哉
北陸先端科学技術大学院大学 情報科学研究科
e-mail: ishihara at jaist.ac.jp

-----------------------------------------------
* 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.