The Language Server Protocol (LSP) is a protocol that standardizes the way Integrated Development Environments (IDEs) and text editors communicate with language servers to provide language-specific features like autocompletion, go-to-definition, and diagnostics. While LSP has been widely adopted by mainstream programming languages, its adoption in dependently typed languages has been slower due to the unique challenges posed by their complex type systems and interactive theorem proving capabilities. This thesis explores the potential of LSP for enhancing the development of dependently typed programs, focusing on the Agda programming language. We present the implementation of a prototype LSP server for Agda that leverages scope checking to provide fast and responsive IDE features. We evaluate the performance of the prototype and compare its feature completeness with existing Agda development tools. Our findings demonstrate that scope checking can serve as a foundation for implementing efficient LSP features in Agda, offering a promising direction for improving the tooling and overall development experience for dependently typed languages.

We can see and we can hear through the internet, but not yet touch. Tactile Internet (TI) is the paradigm that will enable the transmission of tactile feedback through the internet. TI requires Ultra Low Latency (ULL) networking to prevent desynchronization. Reaching the ULL requirements for medium to long distances is not possible without breaking the known physical limits of the speed of light. We propose instead to bypass these requirements by running a physical simulation of the controlled environment to perform predictions before the information can arrive. To this end, efficient low-polygon 3D meshes from the objects in the environment are required for physical simulation. The focus of this work is on reconstructing these meshes from point cloud scanners. Through a combination of Marching Cubes mesh reconstruction and Hoppe's Mesh Simplification, point clouds with up to 20 mm Gaussian noise can be accurately reconstructed into compact low polygon meshes.