Re: [Brillant-devel] Difference between shallow and deep embedding?

Hello

David,  is your question about what is  deep embedding vs. a shallow embedding? 
or the consequence in a COQ formalization of the B theory?

Regards,
Simão 

A 2009/12/08, às 12:44, David MENTRE escreveu:

> Hello,
> 
> I re-read Samuel's announcement of BiCoax[1] recently. It is written:
> "BiCoax is a shallow embedding and BiCoq is a deep embedding."
> 
> What is the difference between a shallow and a deep embedding on B in Coq?
> 
> Regards,
> david
> 
> [1] http://download.gna.org/brillant/snapshots/BiCoax-announce
> 
> _______________________________________________
> Brillant-devel mailing list
> [EMAIL PROTECTED]
> https://mail.gna.org/listinfo/brillant-devel

------------------------------------------------------------------------
Simão Melo de Sousa            | PhD
     RELEASE - RELiablE And SEcure computation Group
             http://www.di.ubi.pt/~release
   * -> ., # -> @ => email Simão -> desousa#di*ubi*pt
Departamento de Informática    | http://www.di.ubi.pt/~desousa
Universidade da Beira Interior | Tel: +351 275 319 891
Rua Marquês d'Âvila e Bolama   | Fax: +351 275 319 899
6200-001 Covilhã, PORTUGAL.
------------------------------------------------------------------------



_______________________________________________
Brillant-devel mailing list
[EMAIL PROTECTED]
https://mail.gna.org/listinfo/brillant-devel