- About dokuwiki
The specification of computation systems today is commonly given using operational semantics, supplanting the well-established but restrictive approach using denotational semantics. Operational semantics is generally given via inference rules using relations between different items of the computation, and for this reason, it is an example of a relational specification. Inference rules over relations are also used for specifying the static semantics for programming languages as well (type inference, for example).
The use of denotational style presentations of computational systems naturally leads to the use of functional programming-based executable specifications. Similarly, the use of inference systems for the presentation of operational semantics provides a natural setting for exploiting logic programming-based implementations.
The Parsifal project will exploit recent developments in proof search and logic programming to make the specification of operational semantics more expressive and declarative and will develop techniques and tools for reasoning directly on logic-based specifications.
More specifically, the Parsifal project will focus on the following goals.
Keywords: program specification, program correctness, proof search, type theory, operational semantics, model checking, proof theory
Theme: “Sym A : Symbolic systems: Reliability and safety of software”.