coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Nonstandard analysis in Coq?

From: Kohei SUENAGA <ksuenaga AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Nonstandard analysis in Coq?
Date: Tue, 20 Sep 2016 07:50:15 +0900
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ksuenaga AT gmail.com; spf=Pass smtp.mailfrom=ksuenaga AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f175.google.com
Ironport-phdr: 9a23:q+PXKBZdD5sEB4lQtQCd7Zz/LSx+4OfEezUN459isYplN5qZpsu6bnLW6fgltlLVR4KTs6sC0LuP9fC9EjVRqdbZ6TZZL8wKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2a3IyL0LW5/ISWaAFVjhK8Z6lzJVO4t1b/rM4T1KhlKqswgiD0j11hVM0ekWBzOF+Vlhn1zsi19Z9ntS9XvqRypIZ7TazmcvFgHvRjBzM8PjVt6Q==

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