With Virtual Reality, we can create and explore an infinite number of environments. These environments can have multiple applications, such as in education, training, or entertainment. However, we need a way to move through these environments. The most natural way is to walk, but we are limited by our physical space. A solution would be hyperbolic space. In this thesis, we explore navigational performance in hyperbolic space and its relation to the properties of hyperbolic geometry. By using the existing application Holonomy VR, we can use hyperbolic space and virtual reality to create an infinite world in a confined physical space. We let participants navigate in this virtual experience to study if they can navigate and learn about its properties. To achieve this, the performance of Holonomy VR is improved and new features are added that allow for a textured top view of the hyperbolic plane in the form of a 2D experience. Also, a new mode is added that requires users to find multiple landmarks in the environment. The beacon cue is developed to let users see targets outside of their current reach. A user study is conducted in collaboration with Leiden University to test the navigational performance and the understanding of the hyperbolic properties. The results show that some people can adapt to navigating in a confined hyperbolic space and that the 2D experience results in the fastest training time. However, it is found that training by exploring the environment and learning about the landmarks before the evaluation does not improve the navigational performance. This contradicts the findings about navigation in a Euclidean scene. It is also found that some hyperbolic properties can be learned and that the 2D experience made it easier to learn about the diverging paths property. Participants who grasped the concept found the experience fun and interesting, and some even indicated that they wanted to learn more about hyperbolic space. Overall, this study shows that people can navigate a confined hyperbolic environment and that they can learn about its properties.

Formal verification works better than testing, since the correctness of a program is proven. It is researched if it is possible and feasible to formally verify the Inductive Graph Library. The library is an abstract class in Haskell and is ported manually to Agda. Agda is a total and dependently typed language and thus can be used as a proof assistant. The functions are first converted to total functions and the preconditions the are proven. Verifying an abstract class is time consuming, since it requires an implemented instance of the abstract class. Stating the properties of the library is possible, but difficult since it requires generalised properties that need to be valid for all instances of the abstract class. The verification process is not completed yet, so no definitive conclusions are made, but the properties that are verified did not produce any issues. agda2hs is used to compile the Agda code to Haskell, this ensures that the verified Agda code is verified Haskell code. This requires the library to fall within the common subset of agda2hs.