The Coq mailing list

[Jean Goubault-Larrecq <goubault AT lsv.ens-cachan.fr>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Le 09/01/2014 10:22, Frédéric Blanqui a écrit :
> 
> 
> Le 08/01/2014 18:49, Jean Goubault-Larrecq a écrit : I'm no Coq
> expert, but wasn't this idea of translating pattern-matching to
> eliminators (recursors) already the core of Cristina Cornes' PhD
> thesis, back in the time where Coq only had recursors and no
> pattern-matching? I seem to recall she had already realized the
> difficulty of the task, and the importance of axiom K, at least.
> 
> All the best,
> 
> -- Jean.
> 
> 
> 
> Hello Jean.
> 
> You are right. Unfortunately, her PhD is in French and I know no 
> electronic copy of it. In the credits for Coq 6.1, 
> http://coq.inria.fr/distrib/current/refman/Reference-Manual002.html#sec5
>
> 
, it is written: "Cristina Cornes designed an extension of the Coq
> syntax to allow definition of terms using a powerful
> pattern-matching analysis in the style of ML programs." You can
> find the table of contents of her PhD on 
> https://who.rocq.inria.fr/Frederic.Blanqui/divers/cornes97phd-toc.pdf
>
> 
(messages on coq-club are limited to 39 Ko...).

Thanks a lot Frédéric.  Of course that was off the top
of my head, and I do not have a copy of Cristina's PhD
thesis at hand.  I don't remember what the relation to
Eduardo Gimenez' seminal paper was, either...
All the best,

- -- Jean.

-----BEGIN PGP SIGNATURE-----
Version: GnuPG/MacGPG2 v2.0.18 (Darwin)
Comment: GPGTools - http://gpgtools.org
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

iQEcBAEBAgAGBQJSzm52AAoJEBO3J6HB7Rh1MJUH/2N5Zju1zLGFxc8xPxI+XinM
MKBXQ2zT5UmnYRQzIs6CZcQPDeMscItwWx96ZX1p7AiMRNypHv6ylbNtSZlteSO7
TPk3mNjd0xyb1AX3hIrVNMqW2EeikHLhd2wcJWBJWZjnjPRQlhb1qvOzvlh4ZhuH
HxJxnOp+3qfYmtqgwDn85gjzAt02ypqi8sw99dqawwjlRx8byXLt6cJaYLy2E8+I
Snd0WLvVj2uD8I4sO/nXtmVtbiEy0UorI5p5tK0s7ZieczNm+w+njEU/va9W+FdO
mvMEwSu9HAgEUtlcUrtQ+R12LZK9XhFAZ65neFDvThJQ5/H7pHhBHnyFxFoFodo=
=203p
-----END PGP SIGNATURE-----