Using models to model-check recursive schemes

Sylvain Salvati, Igor Walukiewicz

We propose a model-based approach to the model checking problem for recursive schemes. Since simply typed lambda calculus with the fixpoint operator, lambda-Y-calculus, is equivale…