home search a-z help
University of Cambridge Logic and Semantics Seminar
29 September: Weng Kin Ho
Computer Laboratory > Research > TSG > Logic and Semantics Seminar > 29 September: Weng Kin Ho

Speaker: Weng Kin Ho, University of Birmingham
Title: An Operational Domain-Theoretic Treatment of Recursive Types
Time: 29 September, 14.00
Venue: William Gates Building, room FW11

An operational domain theory is developed for treating recursive types. The principal approach taken here deviates from classical domain theory in that we do not produce recursive types via inverse limit constructions - we have it for free by working directlly with the operational semantics of FPC. The important step taken in this work is to extend type expressions to legitimate $n$-ary functors on suitable `syntactic' categories. To achieve this, we rely on operational versions of the Plotkin's uniformity principle and the minimal invariance property. This provides a basis for us to introduce the operational notion of algebraic compactness. We then establish algebraic compactness results in this operational setting. In addition, a "pre-deflationary" structure is derived on closed FPC types and this is used to generalise the "Generic Approximation Lemma" recently developed by Huttons and Gibbons. This lemma provided a powerful tool for proving program equivalence by simple inductions, where previously various other more complex methods had been employed.