LMF PhD Seminars

Programming languages are designed with different goals. They are often complimentary, and can each be efficient for their own subset of problems. In practice, we would like to be able to mix them together. To do so, languages have to expose a way to communicate to each other, called FFI (Foreign Function Interface). Languages often have different memory models. To guarantee safety, very strict rules have to be enforced. We focus on interoperability between OCaml and C, and how formal methods can be used to guarantee the correct use of its rules.

Systems engineering requires to use many commercial modeling tools for which semantics is not always formally defined, if defined at all. Engineers have to adapt to the many different conceptions, and the relationships between the various models they develop are difficult to keep consistent over time. This work presents the simplified approach based on inductive type theory which is much simpler to deploy. We propose a Metamodel definition language based on small and effective formal basis, allowing to describe different models. With deep and shallow embedding in Coq we show how translation between Domain Specific Language (DSL) and formal description can be performed.

Computation can be introduced into proof systems using rewrite rules. It is convenient, as parts of the proofs are directly managed by the system. But do rewrite rules also add expresiveness? In other words, can we prove the same results with axioms instead of rewrite rules? We focus on the λΠ-calculus modulo theory, an extension of simply typed λ-calculus with dependent types and user-defined rewrite rules. We show that it is possible to replace the rewrite rules of a theory of the λΠ-calculus modulo theory by equational axioms, when this theory features the notions of proposition and proof. To do so, we introduce a heterogeneous equality in the target theory, and we build a translation that replaces each use of the conversion rule by the insertion of a transport.

We often divide programming languages into two categories: those that are strongly-typed but rigid, and those that are more flexible but untyped (or dynamically typed). While static typing offers formal guarantees about the soudness of programs ("well-typed programs cannot go wrong") and can be used for the documentation and the tooling (auto-completion, etc), this often comes at the expense of flexibility, making programs more secure but prototyping more tedious. In this presentation, we study a formal system to statically type dynamic languages such as Python or Javascript, offering a compromise between safety and flexibility.

The static typing of dynamic languages raises new challenges. In particular, in dynamic languages, functions can be overloaded: they can express multiple behaviors that cannot be resolved statically, but instead are selected at runtime (dynamic dispatch). Some work aims to extend these languages with static typing (e.g. Typescript for Javascript), but lacks a formalization and an algorithm for infering type without needing annotations from the programmer.

To address this issue, we present a type system that combines, in a controlled way, first-order polymorphism with intersection types, union types, and subtyping. This yields a type discipline in which unannotated functions are given polymorphic types (thanks to Hindley-Milner) that can capture the overloaded behavior of the functions they type (thanks to the intersection types) and that are deduced by applying advanced techniques of type narrowing (thanks to union types). This makes the system a prime candidate to type dynamic languages.

<abstract>

We present a low-level language suitable for writing basic algorithms of computer algebra (e.g. algorithms from the GMP or BLAS libraries). Such algorithms primarily use arrays to represent most mathematical objects. Our language therefore focuses on arrays. We present the semantics of our language, which was formalized in Coq. This semantics is safe, that is, well-typed programs cannot run into an undefined behavior. Another goal for this semantics is simplifying proof of programs. In particular, it does not manipulates any memory, nor pointers, and aliases of mutable arrays are forbidden. Finally, we present the formally verified compiler for our language. To achieve this, the compiler translates programs written in our language to the C#minor intermediate language of CompCert and we formally proved that the semantics is preserved by this translation.

Dependent type theory is the logical foundation of many popular proof assistants, such as Coq, Agda and Lean. However, when presented in its most primitive form, the syntax of type theory suffers from a serious usability problem: every type annotation must be explicitly spelled out, rendering it unusable in practice. In order to solve this, usual presentations of type theory omit the majority of these annotations, but this has a cost. Because knowing them is still important when typing terms, it becomes unclear how to do this algorithmically.

A solution to this problem is provided by bidirectional typing, a discipline in which the typing judgment is decomposed explicitly into inference and checking modes, allowing to control the flow of type information in typing rules and to specify algorithmically how they should be used. Bidirectional typing has been fruitfully studied and bidirectional systems have been developed for many type theories. However, the formal development of bidirectional typing has until now been kept confined to specific theories, with general guidelines remaining informal.

In this talk I will give a generic account of bidirectional typing for a general class of dependent type theories. This is done by first giving a general definition of type theories (or equivalently, a logical framework), for which I define declarative and bidirectional type systems. I then show, in a theory-independent fashion, that the two systems are equivalent. This equivalence is then explored to establish the decidability of typing for weak normalizing theories, yielding a generic type-checking algorithm that has been implemented in a prototype and used in practice with various theories.