Dependent type systems allow types to depend on values, enabling the encoding of rich semantic properties directly in types. Currently, dependently typed systems are not widely used for general-purpose programming, but they are commonly used in proof assistants. Agda, Idris, Lean, and Rocq all support dependent types.

The expressiveness of the type system comes with a cost: type checking is expensive. This thesis explores co-contextual type checking as an alternative foundation for dependent type systems. Co-contextual type checking inverts the ‘traditional’ flow of information, enabling type checking to proceed without immediate access to a complete typing environment.

This work explores a co-contextual formulation of a dependent type system and its accompanying type-checking algorithm. Both incremental and parallel variants of the algorithm are implemented for the dependently typed lambda calculus Elara, based on LambdaPi (Löh, McBride, and Swierstra, 2010). The research primarily focuses on the feasibility of such a type checker.

Apart from providing the first co-contextual implementation of a dependent type system, its performance is compared to LambdaPi’s contextual bidirectional type-checking algorithm for reference. In the end, it is found that the implemented co-contextual type checker generally performs worse than the contextual reference implementation. Its performance is of the same order of magnitude, with plenty of opportunity for improvement discussed in this work. In particular, co-contextual incremental type checking has significant potential through the reuse of evaluation, which is not fully leveraged in the conservative approach taken in this work.

The Maven Central Repository hosts over 11 million packages. As Maven itself is a build tool for Java, the majority of these packages are Java archives.
This research aims to analyze these packages and look into various build aspects of these projects (the research questions): are Java modules used, what Java versions are used and how is the compiler configured? This is done by downloading a subset of these packages and looking at both the final artifact and the attached Project Object Model (Maven configuration). Specifically, one version is randomly selected from each distinct package hosted on Maven Central and then analyzed.
This research helps inform Java language developers and library maintainers. It captures parts of the build system evolution over a span of more than a decade. Precisely, version adoption, reproducibility and desirable build features are all important metrics for project maintainers in any software ecosystem. In the end, 473352 packages were analyzed. Firstly, it was found that Java modules are rare: only 6919 (1.69% of the artifacts with an archive) of the packages use Java modules. Secondly, the most common Java version used is Java SE 8 (182476 packages) representing almost half of all analyzed packages. All long-term support versions (Java SE 8, 11, 17 and 21) make up roughly half of the available packages. Thirdly, only 54.98% of artifacts configure the Maven compiler plugin with the most used parameters being the source and target Java versions. The most common additional compiler flags are verbosity settings, providing more feedback and code analysis from both the linter and compiler.