Recent years have seen a significant renewed interest into functional programming. This approach focuses on a more declarative style of programming, as opposed to the imperative view, which focuses on describing computation steps. Therefore, it sits at a higher abstraction level, particularly useful to describe complex modular applications, such as mobile and web user interfaces. Unfortunately, existing formalisms, tools and techniques to model computer systems are ill-suited to describe highly-functional applications. In a effort to tackle this issue, we propose a new formalism, based on high-level Petri nets, that allows to manipulate functions as first-class objects, directly within the model. We present our motivation, introduce our formalism by the means of examples and discuss potential ways to carry out software verification.