Efficient Evaluation with Controlled Definition Unfolding - WITS'24

Explore a conference talk from ACM SIGPLAN's WITS'24 that delves into efficient evaluation techniques with controlled definition unfolding in polymorphic and dependently typed languages. Examine the tension between efficient conversion checking and preserving definition unfoldings, crucial for user interaction and unification processes. Learn about a design for efficient open evaluation that maintains unfoldings, with a focus on distinguishing between top-level and local definitions. Discover how this approach can benefit conversion checking, scope checking, and metavariable solutions in unification. Consider the potential for preserving arbitrary unfoldings with moderate complexity increases, as presented by András Kovács in this 29-minute presentation.