In a functional program, a function may take an argument that is itself... a function. When it comes to model-checking, that implies that the tree of (potential) execution traces of a program is not regular in general: it can not be represented as the unfolding of a finite graph. However, it can be represented as the result of the (infinite) evaluation of a higher-order recursion scheme (HORS). If one wants to verify monadic second-order logic (MSO) formulas over such trace trees, it means that they have to be somehow lifted to the HORS. This is possible and leads to a decidable verification problem (Ong 2006).

Now HORS are equivalent to simply-typed lambda-terms with recursion. And this lamba-calculus admits semantics and type systems. Kobayashi and Ong (2009) used a type system to reprove Ong's result. In 2015-2016, Grellois and Melliès obtained another proof using semantics, in parallel with Salvati and Walukiewicz. The complexity measure was refined in 2018 by Clairambault, Grellois and Murawski.

We will in a first time explain this type-theoretic and semantic approach for the deterministic case, and which contemporary research lines it paves the way for.

The next challenge is to extend this deterministic case to the probabilistic case. We will quickly show results about termination:
- how to extend the lambda-calculus to a constrained probabilistic setting, and to obtain a decidable soundness result using companion one-counter Markov decision processes (OC-MDPs) (Dal Lago-Grellois 2017, 2019)
- how to extend HORS to a probabilistic setting, and what we can get of it (Kobayashi-Dal Lago-Grellois 2019, 2020)

The talk will not require any prerequiste on lambda-calculi, type systems or semantics.