coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Nonstandard analysis in Coq?

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Nonstandard analysis in Coq?
Date: Tue, 20 Sep 2016 10:33:47 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f43.google.com
Ironport-phdr: 9a23:sLskmh/oV31l8P9uRHKM819IXTAuvvDOBiVQ1KB90+IcTK2v8tzYMVDF4r011RmSDNydu6wP07Ge8/i5HzdfsdDZ6DFKWacPfiFGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJdb974EY/Kjsmxy/v6u9iKO10J13KBZuZZKwz+hgHMvIFCiox7b6011xHho31Seu0Qy3k+dnyJmBOpzM6rtKV78jhMtug6v5pKF6y8YOIjVb1EEDk8KEg64cTqsV/ISg7ZtShUaXkfjhcdW1uN1xr9RJqk93Ki7uc=

There is work by Maguad and Fuchs and coworkers, in Coq:
http://link.springer.com/article/10.1007/s10472-014-9434-6

Sam Sanders and Chuangjie Xu are working on an implementation in agda.
https://arxiv.org/abs/1606.06386

Both groups should be able to give you more information.

On Tue, Sep 20, 2016 at 12:50 AM, Kohei SUENAGA <ksuenaga AT gmail.com> wrote:

Hi,

I'm looking for a Coq implementation of nonstandard analysis by Robinson.
Does anyone know some project to looking at?

Sincerely,

Kohei

--
Kohei Suenaga (末永幸平), Ph.D
Associate professor (准教授)
Graduate School of Informatics, Kyoto University
(京都大学情報学研究科)
ksuenaga AT gmail.com
http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/

[Coq-Club] Nonstandard analysis in Coq?, Kohei SUENAGA, 09/20/2016
- Re: [Coq-Club] Nonstandard analysis in Coq?, Bas Spitters, 09/20/2016
  - Re: [Coq-Club] Nonstandard analysis in Coq?, Kohei SUENAGA, 09/21/2016
  - Re: [Coq-Club] Nonstandard analysis in Coq?, Bas Spitters, 09/21/2016