Skip to main content
PRL Project

Formal Models for Nuprl Evaluator

by Aleksey Nogin

In this talk I am going to describe the explicit substitution and explicit sharing calculi as described in Explicit Substitution Survey by Kristoffer Roze and talk about the ideas to use them in improving and formalizing the Nuprl evaluator. (