Résumé/Abstract:
We describe the operational and denotational semantics
of a small imperative language in type theory with inductive and
recursive definitions. The operational semantics is given by natural
inference rules, implemented as an inductive relation.
The realization of the denotational semantics is more delicate: The
nature of the language imposes a few difficulties on us. First, the
language is Turing-complete, and therefore the interpretation function
we consider is necessarily partial. Second, the language contains strict
sequential operators, and therefore the function necessarily exhibits
nested recursion.
Our solution combines and extends recent work on the treatment of
general recursive functions and partial and nested recursive
functions.The first new result is a technique to encode the approach of
Bove and Capretta for partial and nested recursive functions in type
theories that do not provide simultaneous induction-recursion.
A second result is a clear understanding of the characterization of the
definition domain for general recursive functions, a key aspect in the
approach by iteration of Balaa and Bertot.
In this respect, the work on operational semantics is a meaningful
example, but the applicability of the technique should extend to other
circumstances where complex recursive functions need to be described
formally.
Retour au sommaire / Back to schedule