The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Erik Palmgren has an overview:
http://www2.math.uu.se/~palmgren/biblio/nonstd.html

His work on sheaf models should be interesting given the recent interest in forcing extensions of type theory (and Coq).

I seem to recall he has also implemented something, but I don't recall whether it was in mathematica, agda or in Coq.

Related to the work by Per Martin-L"of, there is also the work by Wallet on non-standard models of type theory, e.g.:
https://hal.archives-ouvertes.fr/hal-01320619/

On Tue, Sep 20, 2016 at 10:33 AM, Bas Spitters <b.a.w.spitters AT gmail.com> wrote:

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/