Search


Volume

Author

Year

  • < Previous
  • 1
  • Next >
2 results

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 equivalent to schemes, we propose the use of a model of lambda-Y-calculus to discriminate the terms that satisfy a given&nbsp;[&hellip;]
Published on June 11, 2015

Typing weak MSOL properties

Sylvain Salvati ; Igor Walukiewicz.
We consider lambda-Y-calculus as a non-interpreted functional programming language: the result of the execution of a program is its normal form that can be seen as the tree of calls to built-in operations. Weak monadic second-order logic (wMSOL) is well suited to express properties of such trees. We&nbsp;[&hellip;]
Published on March 23, 2017

  • < Previous
  • 1
  • Next >