[Agda] the joys and sorrows of abstraction.

[Matthieu Sozeau]

Hi,

I know in Coq and Matita for example, equipping the core term
representation with general explicit substitutions was tried and found to
be a performance bottleneck, for conversion in particular, and not the
converse, sadly. But Coq does still use some explicit/delayed substitution
representation in its “efficient” reduction abstract machine.

Best,
— Matthieu
Le jeu. 17 mai 2018 à 00:52, Martin Escardo <m.escardo at cs.bham.ac.uk> a
écrit :

>
>
> On 16/05/18 23:52, hancock at fastmail.fm wrote:
> > Or is there some reason why solid foundations and practical
> implementations
> > should not coincide?
>
> This is the right question.
>
> Martin
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180517/a9665588/attachment.html>