Type-Theoretic Functional Semantics

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 by the authors and others 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 ...

• Type: Conference
• Year: 2002
• Where: TPHOL
• Authors: Yves Bertot, Venanzio Capretta, Kuntal Das Barman
• Keywords: Automated Reasoning, General Recursive Functions, Nested Recursive Functions, Recursive Functions, TPHOL 2002