LMF PhD Seminars

The PhD seminar is a monthly lab event open to any non-permanent member of the LMF. PhD students, interns, post-docs, and engineers are all welcome to attend the presentation and lunch.

The next edition is planned on the 18th of June and we will listen to Andrei Samokish!

Please register before Monday 3rd of June!

Past editions

Thomas Traversié 2024/05/28
Replacing Rewrite Rules by Equational Axioms in the LambdaPi-Calculus Modulo Theory (📽️ slides)
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.
Mickaël Laurent 2024/05/07
Polymorphic Type Inference for Dynamic Languages (📽️ slides)

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.

David Hamelin 2024/04/02
Cool Inductive Constructions (📽️ slides)
Josué Moreau 2024/01/30
A safe language for computer algebra and its formally verified compiler (📽️ slides)
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.
Thiago Felicissimo 2023/11/30
Generic Bidirectional Typing for Dependent Type Theories (📽️ slides)

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.