Logic of plotkin continuous domain

Abstract

This paper extend the Abramsky approach to domain logic, in the sense, that we are considering Plotkin continuous domains instead of Scott domain or SFP-domain. Thus, we study the logical aspects of domains as used in the denotational semantics of non-deterministic programming languages with directed application in scientific computation. Using the alternative description of information system (Plotkin continuous), we give a concrete language for types, we eliminate some restrictions of the Abramsky approach, we increment new axioms and rules to the proof system, and we determinate the meaning of the atomical formulae.