joint work with Sylvain Salvati

Speaker(s)

Igor Walukiewicz

Affiliation

CNRS and Bordeaux University

Date

Jan. 7, 2015, 2:15 p.m.

Room

room 5870

Title in Polish

A semantic model for verification of higher-order programs

Seminar

Seminar Automata Theory

---

We consider simply typed lambda-calculus with fixpoints as a
non-interpreted functional programming language: the result of the
execution of a program is its normal form that can be seen as a,
potentially infinite, tree of calls to built-in operations.  Properties
of such trees are properties of executions of programs and Monadic
second-order logic (MSOL) is well suited to express them.

For a given MSOL property we show how to construct a model recognizing it.
In other words, the value of a lambda-term in the model determines if the tree that is the result of the execution of the term satisfies the
property.  This construction allows to infer many results about
verification in this framework.

---