[Agda] Type-checker evaluator performance

[Nils Anders Danielsson]

On 2016-02-02 08:31, Jon Sterling wrote:
> I hope this isn't off-topic, but what's the state of the art for this?
> Krivine machines?

I don't know, I know very little about this topic.

Randy Pollack once informed me that LEGO uses the U-machine (due to
Pierre Lescanne) for strong reduction:

   λν, a calculus of explicit substitutions which preserves strong
   normalisation
   Zine-El-Abidine Benaissa, Daniel Briaud, Pierre Lescanne and Jocelyne
   Rouyer-Degli
   http://doi.org/10.1017/S0956796800001945

He also mentioned a machine due to Pierre Crégut:

   An abstract machine for Lambda-terms normalization
   Pierre Crégut
   http://doi.org/10.1145/91556.91681

An extended version of the paper above:

   Strongly reducing variants of the Krivine abstract machine
   Pierre Crégut
   http://doi.org/10.1007/s10990-007-9015-z

Is this the kind of thing you have in mind? Or maybe the following
machine?

   A Compiled Implementation of Strong Reduction
   Benjamin Grégoire and Xavier Leroy
   http://doi.org/10.1145/583852.581501

-- 
/NAD