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.

Creating photorealistic images is one of the ultimate goals of computer graphics. Previous work has shown that a material's microstructure plays a crucial role when trying to achieve photorealism. This is because a material's appearance depends on the roughness of its microstructure. Due to this dependence, effects such as masking and shadowing have to be taken into account, as these are capable of altering the effective reflectance of a material. Render engines typically use a mathematical expression, known as a visibility function, that aims to calculate the impact of these effects. However, even the best visibility function known is still an approximation; an exact solution doesn't exist. In order to evaluate the accuracy of visibility functions, an algorithm can be created that computes the correct output, such that the output of a given visibility function can be compared against it. Such an algorithm can be one of two types: approximative or exact. In this paper, we show that approximative algorithms are very capable and come close to their exact counterparts. However, there is still a non-negligible difference between them, meaning they aren't suitable for applications that demand very high levels of accuracy.

This research proposes a new algorithm for mapping Normal Distribution Functions to Heightfields in order to answer its research question: ”Given an NDF, how can we generate a corresponding Heightfield using simple optimization algorithms?”. This research is important, as it helps us to gain a better understanding of how limited statistics-based representations of 3D surfaces are. To this end, we have produced an algorithm using the Simulated Annealing optimization technique, a technique that randomly explores possible solutions of a problem until it finds the optimal solution. The algorithm begins with a flat Heightfield (a 2D representation of a surface that shows the relative altitude of a discrete plane of points), iteratively changes points on the Heightfield and compares its measured NDF (Normal Distribution Function, a function to denote the area distribution along a given direction in a Heightfield) to the target NDF that we want to map. Once the target NDF is reached, or once the pre-determined number of iterations has been reached, the algorithm concludes and the NDF-to-Heightfield mapping has been completed. Three different variations are tried, one na¨ıve implementation which changes points on the Heightfield completely at random, another where the angle of the normal vector of a random surrounding facet of a chosen point is used as guidance for randomization, and finally one where this angle is guided using the relative position of the chosen point to the centre of the Heightfield. The conclusion the proposed algorithm provides is that, while possible, the process of mapping NDFs to Heightfields is a costly and complex operation, and leaves a lot of room for ambiguity. While the research cannot provide a case of an exact match of a target NDF and measured NDF of a Heightfield created through the algorithm, we do show it is without a doubt possible given time.

The micro detail on surfaces can have a profound effect on how rays bounce of it. In ray tracing, this micro-surface is normally approximated with statistical models. We wish to figure out what the effect of normal interpolation and Phong tessellation is on how rays reflect on the surface. This has been Done by creating a ray tracers from scratch, that uses height fields, with normal interpolation and Phong tessellation. This ray tracer has then been used to render 3 different micro-surfaces, which were compared in order to understand the difference. The conclusion of this research was that both smoothing techniques had little to no effect on the reflection of rays on micro-surfaces with a high triangle density. However on micro-surfaces with a low triangle density, there was a much more pronounced difference with the smoothing techniques. A second conclusion was made which was that rougher surfaces have a more spread out distribution of rays than smoother surfaces.

Bidirectional Reflectance Distribution Functions, BRDFs, describe the reflectance of light on a ma-terial, and are widely used in computer graphics to render materials. Acquiring a full measured BRDF can be costly and time consuming, so this research aims to answer the question ”How can we approx-imate a full BRDF from a single slice (in-plane BRDF)?”. Outlined in this paper is an algorithm that uses solids of revolution to approximate a full BRDF from a single slice. The algorithm finds sub-curves of the slice, creates solids of revolution for each, normalizes the data, and merges the solids while removing overlapping data. The resulting solid, described by a list of points using a Carte-sian coordinate system, represents the full, three-dimensional BRDF.

JSGLR2 is a modular Java implementation of the SGLR parsing algorithm that supports systematic benchmarking and improvement of its several parsing variants. By splitting the code into several components, they can be tested in isolation and thus optimized more effortlessly. The modular architecture, although beneficial for efficiently identifying and implementing optimizations, negatively impacts the performance of the parsing algorithm. This paper aims to measure the overhead introduced by the code architecture for one of the variants, more specifically the incremental variant, which combines incremental parsing with SGLR parsing. It does so by comparing the original implementation with a version with the modularity removed. The evaluation is done on programming languages used in practice: Java, WebDSL and SDF3. The results show that the inlined parser outperforms the previous one, achieving speedups of up to 16% in batch parsing and up to 10% in incremental parsing.

JSGLR2 is a java implementation of the Scannerless Generalized LR-parsing (SGLR) algorithm. It employs a modular architecture. This architecture comes with a performance overhead for letting multiple components interact with each other. This paper looks into the size of the performance overhead penalty for the recovery parser variant. It does so by creating an 'inlined' version of the recovery parser variant. The inlined recovery variant is a JSGLR2 implementation that ignores the modular architecture, and hard-codes the components. The performance of the inlined variant is measured with a pre-existing evaluation suite. The results show that there is a performance increase between the original, and the inlined variant.