This library defines the Scott Topology, and shows that continuous functions are increasing and lub-preserving; and -- under point-wise ordering -- also form a Scott Topology. The main reason Computer Scientists are interested is that it constitutes a general foundation on which to build the fix point theory needed for the semantics of loops and recursive functions.
This library is mainly based on BA Davey and HA Priestly "Introduction to Lattices and Orders", CUP, 1990.
| Theorem | Location | PVS Name | Contributors |
|---|
- David Lester, Manchester University, UK
- César Muñoz, NASA, USA
- Mariano Moscato, NIA & NASA, USA
- Sam Owre, SRI, USA
- César Muñoz, NASA, USA
