Towards an arithmetic for partial computable functionals

The thesis concerns itself with nonflat Scott information systems
as an appropriate denotational semantics for the proposed theory
TCF+, a constructive theory of higher-type partial computable
functionals and approximations. We prove a definability theorem for
type systems with at most unary constructors via atomic-coherent
information systems, and give a simple proof for the density
property for arbitrary finitary type systems using coherent
information systems. We introduce the notions of token matrices and
eigen-neighborhoods, and use them to locate normal forms of
neighborhoods, as well as to demonstrate that even nonatomic
information systems feature implicit atomicity. We then establish
connections between coherent information systems and various
pointfree structures. Finally, we introduce a fragment of TCF+ and
show that extensionality can be eliminated.