Type inference can be considered a form of partial evaluation that only evaluates a program with respect to its type annotations. Building on this key observation, this dissertation presents a uniform framework for expressing computation, its dynamic properties and corresponding static type information. By using a unified approach, the static phase divide between values and types is lifted. Instead, computations and properties can be freely assigned to the static or dynamic phase of computation. Even more, moving a property from one world to the other does not require any program modifications. This thesis builds a bridge between two worlds: That of statically typed languages and the dynamically typed world. The former is wanted for the offered static guarantees and detection of a range of defects. With the increasing power of type systems available, the kinds of errors that can be statically detected is growing, nearing the goal of proving overall program correctness from the program’s source code alone. However, such power does come for a price: Type systems are becoming more complex, restrictive and invasive, to the point where specifying type annotations becomes as complex as specifying the algorithm itself. Untyped languages, in contrast, may provide less static safety but they have simpler semantics and offer a higher flexibility. They allow programmers to express their ideas without worrying about provable correctness. Not surprisingly, untyped languages have a strong following when it comes to prototyping and rapid application development. Using the framework presented in this thesis, the programmer can have both: Prototyping applications using a dynamically typed approach and gradual refinement of prototypes into programs with static guarantees. Technically, this flexibility is achieved with the novel concept of auxiliary computations. Auxiliary computation are additional streams of computation. They model, next to the data’s computation, the computation of property of data. These streams thereby may depend on the actual data that is computed, as well as on further auxiliary computations. This expressiveness brings auxiliary computations into the domain of dependent types. Partial evaluation of auxiliary computations is used to infer static knowledge from auxiliary computations. Due to the interdependencies between auxiliary computations, evaluating only those parts of a program that contribute to a property is non trivial. A further contribution of this work is the use of demands on computations to narrow the extent of partial evaluation to a single property. An algorithm for demand inference is presented and the correctness of the inferred demands is shown.

We live in a time where computing devices power essential systems of our society: our automobiles, our airplanes and even our medical services. In these safety-critical systems, bugs do not just cost money to fix; they have a potential to cause harm, even death. Therefore, software correctness is of paramount importance. Existing mainstream programming languages do not support software verification as part of their design, but rely on testing, and thus cannot completely rule out the possibility of bugs during software development. To fix this problem we must reshape the very foundation on which programming languages are based. Programming languages must support the ability to verify the correctness of the software developed in them, and this software verification must be possible using the same language the software is developed in. In the first half of this dissertation we introduce three new programming languages: Freedom of Speech, Separation of Proof from Program, and Dualized Type Theory. The Freedom of Speech language separates a logical fragment from of a general recursive programming language, but still allowing for the types of the logical fragment to depend on general recursive programs while maintaining logical consistency. Thus, obtaining the ability to verify properties of general recursion programs. Separation of Proof from Program builds on the Freedom of Speech languageby relieving several restrictions, and adding a number of extensions. Finally, Dualized Type Theory is a terminating functional programming language rich in constructive duality, and shows promise of being a logical foundation of induction and coninduction. These languages have the ability to verify properties of software, but how can we trust this verification? To be able to put our trust in these languages requires that the language be rigorously and mathematically defined so that the programming language itself can be studied as a mathematical object. Then we must show one very important property, logical consistency of the fragment of the programming language used to verify mathematical properties of the software. In the second half of this dissertation we introduce a well-known proof technique for showing logical consistency called hereditary substitution. Hereditary substitution shows promise of being less complex than existing proof techniques like the Tait-Girard Reducibility method. However, we are unsure which programming languages can be proved terminating using hereditary substitution. Our contribution to this line of work is the application of the hereditary substitution technique to predicative polymorphic programming languages, and the first proof of termination using hereditary substitution for a classical type theory.

This thesis consists of four papers on type theory and a formalisation of certain results from the two first papers in the Agda language. We cover topics such as models of multisets and sets in Homotopy Type Theory, and explore ideas of using type theory as a language for databases and different ways of expressing dependencies between terms. The two first papers build on work by Aczel 1978. We establish that the underlying type of Aczel’s model of set theory in type theory can be seen as a type of multisets from the perspective of Homotopy Type Theory, and we identify a suitable subtype which becomes a model of set theory in which equality of sets is the identity type. The third paper is joint work with Henrik Forssell and David I .Spivak and explores a certain model of type theory, consisting of simplicial complexes, from the perspective of database theory. In the fourth and final paper, we consider two approaches to unraveling the dependency structures between terms in dependent type theory, and formulate a few conjectures about how these two approaches relate.

Satisfiability (SAT) and satisfiability modulo theories (SMT) solvers are high-performance automated propositional and first-order theorem provers, used as underlying tools in many formal verification and artificial intelligence systems. Theoretic and engineering advancement of solver technologies improved the performance of modern solvers; however, the increased complexity of those solvers calls for formal verification of those tools themselves. This thesis discusses two methods to formally certify SAT/SMT solvers. The first method is generating proofs from solvers and certifying those proofs. Because new theories are constantly added to SMT solvers, a flexible framework to safely add new inference rules is necessary. The proposal is to use a meta-language called LFSC, which is based on Edinburgh Logical Framework. SAT/SMT logics have been encoded in LFSC, and the encoding can be easily and modularly extended for new logics. It is shown that an optimized LFSC checker can certify SMT proofs efficiently. The second method is using a verified programming language to implement a SAT solver and verify the code statically. Guru is a pure functional programming language with support for dependent types and theorem proving; Guru also allows for efficient code generation by means of resource typing. A modern SAT solver, called versat, has been implemented and verified to be correct in Guru. The performance of versat is shown to be comparable with that of the current proof checking technology.

Type checking is widely used in mainstream programming languages to detect programming errors at compile time. Model checking is gaining popularity as an automated technique for systematically analyzing behaviors of systems. My research focuses on combining these two software verification techniques synergically into one platform for the creation of correct models for software designs. This thesis describes two modeling languages ATS/PML and ATS/Veri that inherit the advanced type system from an existing programming language ATS, in which both dependent types of Dependent ML style and linear types are supported. A detailed discussion is given for the usage of advanced types to detect modeling errors at the stage of model construction. Going further, various modeling primitives with well-designed types are introduced into my modeling languages to facilitate a synergic combination of type checking with model checking. The semantics of ATS/PML is designed to be directly rooted in a well-known modeling language PROMELA. Rules for translation from ATS/PML to PROMELA are designed and a compiler is developed accordingly so that the SPIN model checker can be readily employed to perform checking on models constructed in ATS/PML. ATS/Veri is designed to be a modeling language, which allows a programmer to construct models for real-world multi-threaded software applications in the same way as writing a functional program with support for synchronization, communication, and scheduling among threads. Semantics of ATS/Veri is formally defined for the development of corresponding model checkers and a compiler is built to translate ATS/Veri into CSP# and exploit the state-of-the-art verification platform PAT for model checking ATS/Veri models. The correctness of such a transformational approach is illustrated based on the semantics of ATS/Veri and CSP#. In summary, the primary contribution of this thesis lies in the creation of a family of modeling languages with highly expressive types for modeling concurrent software systems as well as the related platform supporting verification via model checking. As such, we can combine type checking and model checking synergically to ensure software correctness with high confidence.

In programming languages, record types give a universe of discourse (via so-called Σ-types); parameterised record types fix parts of that universe ahead of time (via Π-types), and algebraic datatypes give us first-class syntax (via W-types), which can then be used to program, e.g., evaluators and optimisers. A frequently-encountered issue in library design for statically-typed languages is that, for example, the algebraic datatype implementing the first-class view of the language induced by a record declaration cannot be defined by simple reference to the record type declaration, nor to any common “source”. This leads to unwelcome repetition, and to maintenance burdens. Similarly, the “unbundling problem” concerns similar repetition that arises for variants of record types where some fields are turned into parameters. The goal of this thesis is to show how, in dependently-typed languages (DTLs), algebraic datatypes and parameterised record types can be obtained from a single pragmatic declaration within the dependently-typed language itself, without using a separate “module language”. Besides this practical shared declaration interface, which is extensible in the language, we also find that common data structures correspond to simple theories. Put simply, the thesis is about making tedious and inexpressible patterns of programming in DTLs (dependently typed languages) become mechanical and expressible. The situations described above occur frequently when working in a dependently-typed language, and it is reasonable enough to have the computer handle them. We develop a notion of contexts that serve as common source for definitions of algebraic datatype and of parameterised record types, and demonstrate a “language” of “package operations” that enables us to avoid the above-mentioned replication that pervades current library developments. On the one hand, we demonstrate an implementation of that language as integrated editor functionality — this makes it possible to directly emulate the different solutions that are employed in current library developments, and refactor these into a shape that uses single declaration of contexts, thus avoiding the usual repetition that is otherwise required for provision of record types at different levels of parameterisation and of algebraic datatypes. On the other hand, we will demonstrate that the power of dependently-typed languages is sufficient to implement such package operations in a statically-typed manner within the language; using this approach will require adapting to the accordingly-changed library interfaces. Although our development uses the dependently-typed programming language Agda throughout, we emphasise that the idea is sufficiently generic to be implemented in other DTLs. / Thesis / Doctor of Philosophy (PhD) / There are things we want to use from various perspectives, our tools show that this is possible without any duplication and in a practical and efficient fashion.

Dans ce mémoire, je présente une technique pour combiner du code de bas niveau à un langage purement fonctionnel avec types dépendants. Par code de bas niveau, je veux dire n’importe quel programme écrit dans un langage qui permet le contrôle direct des ressources de la machine. En particulier, ce texte s’intéresse à la gestion de la mémoire. Plus concrètement, un programmeur C contrôle l’endroit et le moment où un bloc de mémoire est alloué, ainsi que la façon dont l’objet est initialisé. Par exemple, on peut allouer de l’espace sur la pile pour immédiatement l’initialiser avec un memcpy. Alternativement, on peut allouer un bloc sur le tas et l’initialiser champ par champ plus tard. Pour certaines applications où la mémoire est limitée ou la performance importante, ce choix est important. Un tel niveau de contrôle n’est pas disponible dans les langages de haut niveau, sauf pour quelques exceptions. Les langages fonctionnels comme OCaml ou Haskell découragent ou même interdisent de modifier les champs d’un objet. C’est encore plus vrai pour les langages à types dépendants où la mutation est l’éléphant dans le magasin de porcelaine de la cohérence. C’est un choix de design intentionnel. Un programme pur est plus facile à comprendre et analyser, mais comment séparer l’initialisation de l’allocation quand un objet ne peut pas changer ? Ce mémoire essaie de démontrer que ce n’est pas parce que c’est impossible, mais parce que ces langages ne sont pas habituellement utilisés dans un contexte où c’est nécessaire. Par contre, ce n’est pas facile non plus. Pour garantir la sécurité et la cohérence, il faut modéliser l’état d’un objet partiellement initialisé au niveau des types, ce que la plupart des langages ont de la peine à faire. La combinaison du manque de nécessité et de la lourdeur syntaxique et conceptuelle est la raison pour laquelle cette fonctionnalité est souvent absente. Pour y parvenir, nous prenons un langage à types dépendants, Typer, et nous y ajoutons le nécessaire pour récupérer une partie du contrôle abandonné dans le design original. Nous permettons au programmeur d’allouer des blocs de mémoire et de les initialiser graduellement plus tard, sans compromettre les propriétés de sécurité du programme. Concrètement, nous utilisons les monades, un concept de la théorie des catégories déjà utilisé pour la modélisation d’effets de bord, pour limiter les mutations aux endroits sécuritaires. / In this thesis, I will demonstrate how to combine low-level code with dependent types. By low-level code, I mean any program authored in a language that allows direct control of computer resources. In particular, this text will focus on memory management. Specifically, a C programmer has control over the location and time when a block of memory is allocated, as well as how it is initialized. For instance, it is possible to allocate stack space to immediately initialize it with an invocation of memcpy. Alternatively, one can allocate heap spate and initialize it field by field later. For some applications where memory is constrained or performance is important, this choice can matter. This level of control is not available in high-level languages, barring a few exceptions. Functional languages such as OCaml or Haskell discourage or simply forbid the mutation of objects. This is especially the case in dependently typed languages where mutation is the bull in the china shop of consistency. This is a deliberate choice as a pure program is easier to understand and reason about. However, having allocation and initialization done in two distinct steps seems impossible in this situation. This thesis shows that this is not impossible, it is simply done this way because these kinds of languages are seldom used in a context where such control is necessary. This does not mean though that adding this feature is easy. If we are to guarantee both safety and consistency, we need to keep track of the initialization state at the type level. Most languages struggle to do this. Language designers simply forgo this feature because it is not useful to them in addition to being difficult to use. To achieve it, we start with a dependently typed language, Typer, and add back the mechanisms necessary to recover the control relinquished in the original design. We let the programmer allocate blocks of memory to initialize later, without compromising the safety properties of the program. Specifically, we use monads, a concept from category theory, a know technique to model side effects, to limit mutation to situations where it is safe.

Les structures avec des lieurs sont très communes en informatique. Les langages de programmation et les systèmes logiques sont des exemples de structures avec des lieurs. La manipulation de lieurs est délicate, de sorte que l’écriture de programmes qui ma- nipulent ces structures tirerait profit d’un soutien spécifique pour les lieurs. L’environ- nement de programmation Beluga est un exemple d’un tel système. Nous développons et présentons ici un compilateur pour ce système. Parmi les programmes pour lesquels Beluga est spécialement bien adapté, plusieurs peuvent bénéficier d’un compilateur. Par exemple, les programmes pour valider les types (les "type-checkers"), les compilateurs et les interpréteurs tirent profit du soutien spécifique des lieurs et des types dépendants présents dans le langage. Ils nécessitent tous également une exécution efficace, que l’on propose d’obtenir par le biais d’un compilateur. Le but de ce travail est de présenter un nouveau compilateur pour Beluga, qui emploie une représentation interne polyvalente et permet de partager du code entre plusieurs back-ends. Une contribution notable est la compilation du filtrage de Beluga, qui est particulièrement puissante dans ce langage. / In computer science, structures with variable binders are very common. Program- ming languages and logical frameworks are examples of structures with binders. Thus writing programs that deal with these kinds of data benefits with explicit support for data binding. The Beluga programming environment is an example of such a system. In this work we develop and present a compiler for the system. Many of the programs that Beluga is specially well suited for writing can benefit from a compiler. For example, some of the kinds programs that would benefit more are type-checkers, compilers and interpreters that take advantage of the binder support and dependent types present in the language, and also require a reasonably fast run-time. Our goal in this work, is to present a compiler for the Beluga system, that uses a very versatile internal representation that helps with the development of the system, and allows a sharing of code between several back-ends. Furthermore, we present a way of compiling the uniquely powerful pattern language supported by Beluga.

Les structures avec des lieurs sont très communes en informatique. Les langages de programmation et les systèmes logiques sont des exemples de structures avec des lieurs. La manipulation de lieurs est délicate, de sorte que l’écriture de programmes qui ma- nipulent ces structures tirerait profit d’un soutien spécifique pour les lieurs. L’environ- nement de programmation Beluga est un exemple d’un tel système. Nous développons et présentons ici un compilateur pour ce système. Parmi les programmes pour lesquels Beluga est spécialement bien adapté, plusieurs peuvent bénéficier d’un compilateur. Par exemple, les programmes pour valider les types (les "type-checkers"), les compilateurs et les interpréteurs tirent profit du soutien spécifique des lieurs et des types dépendants présents dans le langage. Ils nécessitent tous également une exécution efficace, que l’on propose d’obtenir par le biais d’un compilateur. Le but de ce travail est de présenter un nouveau compilateur pour Beluga, qui emploie une représentation interne polyvalente et permet de partager du code entre plusieurs back-ends. Une contribution notable est la compilation du filtrage de Beluga, qui est particulièrement puissante dans ce langage. / In computer science, structures with variable binders are very common. Program- ming languages and logical frameworks are examples of structures with binders. Thus writing programs that deal with these kinds of data benefits with explicit support for data binding. The Beluga programming environment is an example of such a system. In this work we develop and present a compiler for the system. Many of the programs that Beluga is specially well suited for writing can benefit from a compiler. For example, some of the kinds programs that would benefit more are type-checkers, compilers and interpreters that take advantage of the binder support and dependent types present in the language, and also require a reasonably fast run-time. Our goal in this work, is to present a compiler for the Beluga system, that uses a very versatile internal representation that helps with the development of the system, and allows a sharing of code between several back-ends. Furthermore, we present a way of compiling the uniquely powerful pattern language supported by Beluga.

Řada programovacích jazyků byla schopna zvýšit svoji rychlost výměnou běhových systémů stavěných na míru za obecné platformy, které pro optimalizaci používají just-in-time překlad, jako jsou GraalVM nebo RPython. V této práci vyhodnocuji, zda je použití takovýchto platforem vhodné i pro jazyky se závislymi typy nebo důkazovými systémy. Tato práce představuje koncepty -kalkulu a teorie typů potřebné pro úvod do závislých typů s relevantními algoritmy, specifikuje malý závisle typovaný jazyk založený na $\lambda\Pi$ kalkulu, a prezentuje dva interpretery tohoto jazyka. Tyto interpretery jsou psané v jazyce Kotlin, první je jednoduchý, psaný ve funkcionálním stylu a druhý používá platformu GraalVM a Truffle. GraalVM je platforma založená na virtuálním stroji Javy (JVM), která přidává just-in-time překladač založený na částečném vyhodnocení (partial evaluation) a Truffle je knihovna pro tvorbu programovacích jazyků využívající tento překladač. Závěr práce vyhodnocuje běhové charakteristiky těchto interpreterů na různých zátěžových testech.Závěry práce jsou ale silně negativní. Vliv JIT překladu není znatelný ani přes snahu optimalizovat běžné algoritmy z teorie typů, které jsou zjevně nevhodné pro platformu JVM. Práce končí návrhy několika navazujících projektů, které by lépe využily možnosti Truffle a které by byly vhodnější pro implementaci závisle typovaných jazyků.