The Coq mailing list

[Kohei SUENAGA <ksuenaga AT gmail.com>]

Thanks Bas.  Yes, I should have come up with Sam's work first!
I didn't know the work of Maguad et al.  I will take a look.

Kohei

2016-09-20 17:33 GMT+09:00 Bas Spitters 
<b.a.w.spitters AT gmail.com>:
> 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/
>
>



-- 
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/